Documentation

Mathlib.Algebra.Homology.ShortComplex.ShortExact

Short exact short complexes #

A short complex S : ShortComplex C is short exact (S.ShortExact) when it is exact, S.f is a mono and S.g is an epi.

structure CategoryTheory.ShortComplex.ShortExact {C : Type u_1} [] (S : ) :

A short complex S is short exact if it is exact, S.f is a mono and S.g is an epi.

• exact :
• mono_f :
• epi_g :
Instances For
theorem CategoryTheory.ShortComplex.shortExact_of_iso {C : Type u_1} [] {S₁ : } {S₂ : } (e : S₁ S₂) :
theorem CategoryTheory.ShortComplex.shortExact_iff_of_iso {C : Type u_1} [] {S₁ : } {S₂ : } (e : S₁ S₂) :
theorem CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃ {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) [] [] :
theorem CategoryTheory.ShortComplex.isIso₂_of_shortExact_of_isIso₁₃' {C : Type u_1} [] {S₁ : } {S₂ : } (φ : S₁ S₂) :
noncomputable def CategoryTheory.ShortComplex.ShortExact.fIsKernel {C : Type u_1} [] {S : } :

If S is a short exact short complex in a balanced category, then S.X₁ is the kernel of S.g.

Equations
• = let_fun this := (_ : );
Instances For
noncomputable def CategoryTheory.ShortComplex.ShortExact.gIsCokernel {C : Type u_1} [] {S : } :

If S is a short exact short complex in a balanced category, then S.X₃ is the cokernel of S.f.

Equations
• = let_fun this := (_ : );
Instances For

A split short complex is short exact.

noncomputable def CategoryTheory.ShortComplex.ShortExact.splittingOfInjective {C : Type u_1} [] {S : } [] :

A choice of splitting for a short exact short complex S in a balanced category such that S.X₁ is injective.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.ShortComplex.ShortExact.splittingOfProjective {C : Type u_1} [] {S : } [] :

A choice of splitting for a short exact short complex S in a balanced category such that S.X₃ is projective.

Equations
• One or more equations did not get rendered due to their size.
Instances For