# Short exact sequences, and splittings. #

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

short_exact f g is the proposition that 0 ⟶ A -f⟶ B -g⟶ C ⟶ 0 is an exact sequence.

We define when a short exact sequence is left-split, right-split, and split.

In algebra.homology.short_exact.abelian we show that in an abelian category a left-split short exact sequences admits a splitting.

structure category_theory.short_exact {𝒜 : Type u_1} {A B C : 𝒜} (f : A B) (g : B C)  :
Prop
• mono :
• epi :
• exact :

If f : A ⟶ B and g : B ⟶ C then short_exact f g is the proposition saying the resulting diagram 0 ⟶ A ⟶ B ⟶ C ⟶ 0 is an exact sequence.

structure category_theory.left_split {𝒜 : Type u_1} {A B C : 𝒜} (f : A B) (g : B C)  :
Prop

An exact sequence A -f⟶ B -g⟶ C is left split if there exists a morphism φ : B ⟶ A such that f ≫ φ = 𝟙 A and g is epi.

Such a sequence is automatically short exact (i.e., f is mono).

theorem category_theory.left_split.short_exact {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
structure category_theory.right_split {𝒜 : Type u_1} {A B C : 𝒜} (f : A B) (g : B C)  :
Prop

An exact sequence A -f⟶ B -g⟶ C is right split if there exists a morphism φ : C ⟶ B such that f ≫ φ = 𝟙 A and f is mono.

Such a sequence is automatically short exact (i.e., g is epi).

theorem category_theory.right_split.short_exact {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
structure category_theory.split {𝒜 : Type u_1} {A B C : 𝒜} (f : A B) (g : B C)  :
Prop

An exact sequence A -f⟶ B -g⟶ C is split if there exist φ : B ⟶ A and χ : C ⟶ B such that:

• f ≫ φ = 𝟙 A
• χ ≫ g = 𝟙 C
• f ≫ g = 0
• χ ≫ φ = 0
• φ ≫ f + g ≫ χ = 𝟙 B

Such a sequence is automatically short exact (i.e., f is mono and g is epi).

theorem category_theory.exact_of_split {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} {χ : C B} {φ : B A} (hfg : f g = 0) (H : φ f + g χ = 𝟙 B) :
theorem category_theory.split.exact {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
theorem category_theory.split.left_split {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
theorem category_theory.split.right_split {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
theorem category_theory.split.short_exact {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
theorem category_theory.split.map {𝒜 : Type u_1} {ℬ : Type u_2} (F : 𝒜 ℬ) [F.additive] {A B C : 𝒜} {f : A B} {g : B C} (h : g) :

The sequence A ⟶ A ⊞ B ⟶ B is exact.

The sequence B ⟶ A ⊞ B ⟶ A is exact.

@[nolint]
structure category_theory.splitting {𝒜 : Type u_1} {A B C : 𝒜} (f : A B) (g : B C)  :
Type u_2
• iso : B A C
• comp_iso_eq_inl :
• iso_comp_snd_eq :

A splitting of a sequence A -f⟶ B -g⟶ C is an isomorphism to the short exact sequence 0 ⟶ A ⟶ A ⊞ C ⟶ C ⟶ 0 such that the vertical maps on the left and the right are the identity.

Instances for category_theory.splitting
• category_theory.splitting.has_sizeof_inst
@[simp]
theorem category_theory.splitting.iso_comp_snd_eq_assoc {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (self : g) {X' : 𝒜} (f' : C X') :
= g f'
@[simp]
theorem category_theory.splitting.comp_iso_eq_inl_assoc {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (self : g) {X' : 𝒜} (f' : A C X') :
f self.iso.hom f' =
@[simp]
theorem category_theory.splitting.inl_comp_iso_eq {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
@[simp]
theorem category_theory.splitting.inl_comp_iso_eq_assoc {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) {X' : 𝒜} (f' : B X') :
= f f'
@[simp]
theorem category_theory.splitting.iso_comp_eq_snd_assoc {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) {X' : 𝒜} (f' : C X') :
h.iso.inv g f' =
@[simp]
theorem category_theory.splitting.iso_comp_eq_snd {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
noncomputable def category_theory.splitting.section {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
C B

If h is a splitting of A -f⟶ B -g⟶ C, then h.section : C ⟶ B is the morphism satisfying h.section ≫ g = 𝟙 C.

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

If h is a splitting of A -f⟶ B -g⟶ C, then h.retraction : B ⟶ A is the morphism satisfying f ≫ h.retraction = 𝟙 A.

Equations
Instances for category_theory.splitting.retraction
@[simp]
theorem category_theory.splitting.section_π_assoc {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) {X' : 𝒜} (f' : C X') :
h.section g f' = f'
@[simp]
theorem category_theory.splitting.section_π {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
@[simp]
theorem category_theory.splitting.ι_retraction_assoc {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) {X' : 𝒜} (f' : A X') :
f h.retraction f' = f'
@[simp]
theorem category_theory.splitting.ι_retraction {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
@[simp]
theorem category_theory.splitting.section_retraction_assoc {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) {X' : 𝒜} (f' : A X') :
@[simp]
theorem category_theory.splitting.section_retraction {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
= 0
@[protected]
noncomputable def category_theory.splitting.split_mono {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :

The retraction in a splitting is a split mono.

Equations
@[protected]
noncomputable def category_theory.splitting.split_epi {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :

The section in a splitting is a split epi.

Equations
@[simp]
theorem category_theory.splitting.inr_iso_inv {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
@[simp]
theorem category_theory.splitting.inr_iso_inv_assoc {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) {X' : 𝒜} (f' : B X') :
= h.section f'
@[simp]
theorem category_theory.splitting.iso_hom_fst_assoc {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) {X' : 𝒜} (f' : A X') :
@[simp]
theorem category_theory.splitting.iso_hom_fst {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
noncomputable def category_theory.splitting.splitting_of_is_iso_zero {𝒜 : Type u_1} {X Y Z : 𝒜} (f : X Y)  :

A short exact sequence of the form X -f⟶ Y -0⟶ Z where f is an iso and Z is zero has a splitting.

Equations
@[protected]
theorem category_theory.splitting.mono {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
@[protected]
theorem category_theory.splitting.epi {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
@[protected, instance]
def category_theory.splitting.section.category_theory.mono {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
@[protected, instance]
def category_theory.splitting.retraction.category_theory.epi {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
theorem category_theory.splitting.split_add {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
theorem category_theory.splitting.retraction_ι_eq_id_sub {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
theorem category_theory.splitting.retraction_ι_eq_id_sub_assoc {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) {X' : 𝒜} (f' : B X') :
h.retraction f f' = (𝟙 B - g h.section) f'
theorem category_theory.splitting.π_section_eq_id_sub_assoc {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) {X' : 𝒜} (f' : B X') :
g h.section f' = (𝟙 B - h.retraction f) f'
theorem category_theory.splitting.π_section_eq_id_sub {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
theorem category_theory.splitting.splittings_comm {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h h' : g) :
theorem category_theory.splitting.split {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
theorem category_theory.splitting.comp_eq_zero_assoc {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) {X' : 𝒜} (f' : C X') :
f g f' = 0 f'
theorem category_theory.splitting.comp_eq_zero {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g) :
f g = 0
@[protected]
theorem category_theory.splitting.exact {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g)  :
@[protected]
theorem category_theory.splitting.short_exact {𝒜 : Type u_1} {A B C : 𝒜} {f : A B} {g : B C} (h : g)  :