# Documentation

Mathlib.Algebra.Homology.ShortExact.Abelian

# Short exact sequences in abelian categories #

In an abelian category, a left-split or right-split short exact sequence admits a splitting.

theorem CategoryTheory.isIso_of_shortExact_of_isIso_of_isIso {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {A' : 𝒜} {B' : 𝒜} {C' : 𝒜} {f : A B} {g : B C} {f' : A' B'} {g' : B' C'} (h : ) (h' : ) (i₁ : A A') (i₂ : B B') (i₃ : C C') (comm₁ : ) (comm₂ : ) [] [] :
def CategoryTheory.Splitting.mk' {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) (i : B A C) (h1 : = CategoryTheory.Limits.biprod.inl) (h2 : CategoryTheory.CategoryStruct.comp i CategoryTheory.Limits.biprod.snd = g) :

To construct a splitting of A -f⟶ B -g⟶ C it suffices to supply a morphism i : B ⟶ A ⊞ C such that f ≫ i is the canonical map biprod.inl : A ⟶ A ⊞ C and i ≫ q = g, where q is the canonical map biprod.snd : A ⊞ C ⟶ C, together with proofs that f is mono and g is epi.

The morphism i is then automatically an isomorphism.

Instances For
def CategoryTheory.Splitting.mk'' {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) (i : A C B) (h1 : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl i = f) (h2 : = CategoryTheory.Limits.biprod.snd) :

To construct a splitting of A -f⟶ B -g⟶ C it suffices to supply a morphism i : A ⊞ C ⟶ B such that p ≫ i = f where p is the canonical map biprod.inl : A ⟶ A ⊞ C, and i ≫ g is the canonical map biprod.snd : A ⊞ C ⟶ C, together with proofs that f is mono and g is epi.

The morphism i is then automatically an isomorphism.

Instances For
def CategoryTheory.LeftSplit.splitting {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :

A short exact sequence that is left split admits a splitting.

Instances For
def CategoryTheory.RightSplit.splitting {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :

A short exact sequence that is right split admits a splitting.

Instances For