mathlib3 documentation

algebra.homology.short_exact.abelian

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₃] :
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