# mathlibdocumentation

algebra.homology.short_exact.abelian

# Short exact sequences in abelian categories #

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

theorem category_theory.is_iso_of_short_exact_of_is_iso_of_is_iso {𝒜 : Type u_1} {A B C A' B' C' : 𝒜} {f : A B} {g : B C} {f' : A' B'} {g' : B' C'} (h : g) (h' : g') (i₁ : A A') (i₂ : B B') (i₃ : C C') (comm₁ : i₁ f' = f i₂) (comm₂ : i₂ g' = g i₃)  :
noncomputable def category_theory.splitting.mk' {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) (i : B A C) (h1 : f i = category_theory.limits.biprod.inl) (h2 : = 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.

Equations
noncomputable def category_theory.splitting.mk'' {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) (i : A C B) (h1 : = f) (h2 : i g = category_theory.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.

Equations
noncomputable def category_theory.left_split.splitting {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :

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

Equations
noncomputable def category_theory.right_split.splitting {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :

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

Equations