# 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