Dimension Shifting #
@[reducible, inline]
noncomputable abbrev
ModuleCat.projectiveShortComplex
{R : Type u}
[CommRing R]
[Small.{v, u} R]
(M : ModuleCat R)
:
The standard short complex 0 → N → P → M → 0 with P= R^{⊕M} free.
Equations
Instances For
theorem
ModuleCat.shortExact_projectiveShortComplex
{R : Type u}
[CommRing R]
[Small.{v, u} R]
(M : ModuleCat R)
:
instance
instFreeCarrierX₂ModuleCatProjectiveShortComplex
{R : Type u}
[CommRing R]
[Small.{v, u} R]
(M : ModuleCat R)
:
theorem
precomp_extClass_surjective_of_projective_X₂
{R : Type u}
[CommRing R]
[Small.{v, u} R]
(M : ModuleCat R)
{S : CategoryTheory.ShortComplex (ModuleCat R)}
(h : S.ShortExact)
(n : ℕ)
[CategoryTheory.Projective S.X₂]
:
Function.Surjective ⇑(h.extClass.precomp M ⋯)
The connection maps in the contravariant long exact sequence of Ext are surjective if
the middle term of the short exact sequence is projective.
theorem
postcomp_extClass_surjective_of_projective_X₂
{R : Type u}
[CommRing R]
[Small.{v, u} R]
{S : CategoryTheory.ShortComplex (ModuleCat R)}
(h : S.ShortExact)
(M : ModuleCat R)
(n : ℕ)
[CategoryTheory.Injective S.X₂]
:
Function.Surjective ⇑(h.extClass.postcomp M ⋯)
The connection maps in the covariant long exact sequence of Ext are surjective if
the middle term of the short exact sequence is injective.