Dimension Shifting #
@[reducible, inline]
noncomputable abbrev ModuleCat.projectiveShortComplex {R : Type u} [Ring R] [Small.{v, u} R] (M : ModuleCat R) :
The standard short complex 0 → N → P → M → 0 with P= R^{⊕M} free.
Equations
- M.projectiveShortComplex = (({ repr := Finsupp.mapRange.linearEquiv (Shrink.linearEquiv R R) }.constr ℕ) id).shortComplexKer
Instances For
theorem ModuleCat.shortExact_projectiveShortComplex {R : Type u} [Ring R] [Small.{v, u} R] (M : ModuleCat R) :
instance instFreeCarrierX₂ModuleCatProjectiveShortComplex {R : Type u} [Ring R] [Small.{v, u} R] (M : ModuleCat R) :
theorem precomp_extClass_surjective_of_projective_X₂ {R : Type u} [Ring 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} [Ring 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.