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} [CategoryTheory.Category.{u_2, u_1} 𝒜] {A : 𝒜} {B : 𝒜} {C : 𝒜} {A' : 𝒜} {B' : 𝒜} {C' : 𝒜} {f : A ⟶ B} {g : B ⟶ C} {f' : A' ⟶ B'} {g' : B' ⟶ C'} [CategoryTheory.Abelian 𝒜] (h : CategoryTheory.ShortExact f g) (h' : CategoryTheory.ShortExact f' g') (i₁ : A ⟶ A') (i₂ : B ⟶ B') (i₃ : C ⟶ C') (comm₁ : autoParam (CategoryTheory.CategoryStruct.comp i₁ f' = CategoryTheory.CategoryStruct.comp f i₂) _auto✝) (comm₂ : autoParam (CategoryTheory.CategoryStruct.comp i₂ g' = CategoryTheory.CategoryStruct.comp g i₃) _auto✝) [CategoryTheory.IsIso i₁] [CategoryTheory.IsIso i₃] : CategoryTheory.IsIso i₂

def CategoryTheory.Splitting.mk' {𝒜 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒜] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [CategoryTheory.Abelian 𝒜] (h : CategoryTheory.ShortExact f g) (i : B ⟶ A ⊞ C) (h1 : CategoryTheory.CategoryStruct.comp f i = CategoryTheory.Limits.biprod.inl) (h2 : CategoryTheory.CategoryStruct.comp i CategoryTheory.Limits.biprod.snd = g) : CategoryTheory.Splitting f 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

• CategoryTheory.Splitting.mk' h i h1 h2 = let_fun this := (_ : CategoryTheory.IsIso i); { iso := CategoryTheory.asIso i, comp_iso_eq_inl := h1, iso_comp_snd_eq := h2 }

def CategoryTheory.Splitting.mk'' {𝒜 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒜] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [CategoryTheory.Abelian 𝒜] (h : CategoryTheory.ShortExact f g) (i : A ⊞ C ⟶ B) (h1 : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl i = f) (h2 : CategoryTheory.CategoryStruct.comp i g = CategoryTheory.Limits.biprod.snd) : CategoryTheory.Splitting f g

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

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

def CategoryTheory.LeftSplit.splitting {𝒜 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒜] {A : 𝒜} {B : 𝒜} {C : 𝒜} [CategoryTheory.Abelian 𝒜] {f : A ⟶ B} {g : B ⟶ C} (h : CategoryTheory.LeftSplit f g) : CategoryTheory.Splitting f g

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

Equations

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

def CategoryTheory.RightSplit.splitting {𝒜 : Type u_1} [CategoryTheory.Category.{u_2, u_1} 𝒜] {A : 𝒜} {B : 𝒜} {C : 𝒜} [CategoryTheory.Abelian 𝒜] {f : A ⟶ B} {g : B ⟶ C} (h : CategoryTheory.RightSplit f g) : CategoryTheory.Splitting f g

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

Equations

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