mathlib documentation

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} [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₃] :
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) :

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} [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) :

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} [category_theory.category 𝒜] {A B C : 𝒜} [category_theory.abelian 𝒜] {f : A ⟶ B} {g : B ⟶ C} (h : category_theory.left_split f g) :

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

Equations
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) :

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

Equations