Short exact sequences in abelian categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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} [category_theory.category 𝒜] {A B C A' B' C' : 𝒜} {f : A ⟶ B} {g : B ⟶ C} {f' : A' ⟶ B'} {g' : B' ⟶ C'} [category_theory.abelian 𝒜] (h : category_theory.short_exact f g) (h' : category_theory.short_exact f' g') (i₁ : A ⟶ A') (i₂ : B ⟶ B') (i₃ : C ⟶ C') (comm₁ : i₁ ≫ f' = f ≫ i₂) (comm₂ : i₂ ≫ g' = g ≫ i₃) [category_theory.is_iso i₁] [category_theory.is_iso i₃] :

category_theory.is_iso i₂

source

noncomputable def category_theory.splitting.mk' {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.abelian 𝒜] (h : category_theory.short_exact f g) (i : B ⟶ A ⊞ C) (h1 : f ≫ i = category_theory.limits.biprod.inl) (h2 : i ≫ category_theory.limits.biprod.snd = g) :

category_theory.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

category_theory.splitting.mk' h i h1 h2 = {iso := category_theory.as_iso i _, comp_iso_eq_inl := _, iso_comp_snd_eq := h2}

source

noncomputable def category_theory.splitting.mk'' {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.abelian 𝒜] (h : category_theory.short_exact f g) (i : A ⊞ C ⟶ B) (h1 : category_theory.limits.biprod.inl ≫ i = f) (h2 : i ≫ g = category_theory.limits.biprod.snd) :

category_theory.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

category_theory.splitting.mk'' h i h1 h2 = {iso := (category_theory.as_iso i).symm, comp_iso_eq_inl := _, iso_comp_snd_eq := _}

source

noncomputable def category_theory.left_split.splitting {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} [category_theory.abelian 𝒜] {f : A ⟶ B} {g : B ⟶ C} (h : category_theory.left_split f g) :

category_theory.splitting f g

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

Equations

h.splitting = category_theory.splitting.mk' _ (category_theory.limits.biprod.lift _.some g) _ _

source

noncomputable def category_theory.right_split.splitting {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} [category_theory.abelian 𝒜] {f : A ⟶ B} {g : B ⟶ C} (h : category_theory.right_split f g) :

category_theory.splitting f g

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

Equations

h.splitting = category_theory.splitting.mk'' _ (category_theory.limits.biprod.desc f _.some) _ _