Short exact sequences, and splittings. #

CategoryTheory.ShortExact 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 Mathlib.Algebra.Homology.ShortExact.Abelian we show that in an abelian category a left-split short exact sequences admits a splitting.

structure CategoryTheory.ShortExact {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} (f : A B) (g : B C) :
• 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.

Instances For
structure CategoryTheory.LeftSplit {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} (f : A B) (g : B C) :
• left_split :
• epi :
• exact :

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

Instances For
theorem CategoryTheory.LeftSplit.shortExact {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
structure CategoryTheory.RightSplit {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} (f : A B) (g : B C) :
• right_split :
• mono :
• exact :

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

Instances For
theorem CategoryTheory.RightSplit.shortExact {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
structure CategoryTheory.Split {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} (f : A B) (g : B C) :

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

Instances For
theorem CategoryTheory.exact_of_split {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} {χ : C B} {φ : B A} (hfg : ) :
theorem CategoryTheory.Split.exact {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Split.leftSplit {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Split.rightSplit {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Split.shortExact {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Split.map {𝒜 : Type u_2} {ℬ : Type u_3} [] [] (F : ) {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
CategoryTheory.Split (F.map f) (F.map g)
theorem CategoryTheory.exact_inl_snd {𝒜 : Type u_1} [] (A : 𝒜) (B : 𝒜) :
CategoryTheory.Exact CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd

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

theorem CategoryTheory.exact_inr_fst {𝒜 : Type u_1} [] (A : 𝒜) (B : 𝒜) :
CategoryTheory.Exact CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.fst

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

structure CategoryTheory.Splitting {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} (f : A B) (g : B C) :
Type u_2

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
@[simp]
theorem CategoryTheory.Splitting.comp_iso_eq_inl_assoc {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (self : ) {Z : 𝒜} (h : A C Z) :
@[simp]
theorem CategoryTheory.Splitting.iso_comp_snd_eq_assoc {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (self : ) {Z : 𝒜} (h : C Z) :
CategoryTheory.CategoryStruct.comp self.iso.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) =
@[simp]
theorem CategoryTheory.Splitting.inl_comp_iso_eq_assoc {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) {Z : 𝒜} (h : B Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp h.iso.inv h) =
@[simp]
theorem CategoryTheory.Splitting.inl_comp_iso_eq {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h.iso.inv = f
@[simp]
theorem CategoryTheory.Splitting.iso_comp_eq_snd_assoc {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) {Z : 𝒜} (h : C Z) :
= CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h
@[simp]
theorem CategoryTheory.Splitting.iso_comp_eq_snd {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
CategoryTheory.CategoryStruct.comp h.iso.inv g = CategoryTheory.Limits.biprod.snd
def CategoryTheory.Splitting.section {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
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.

Instances For
def CategoryTheory.Splitting.retraction {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
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.

Instances For
@[simp]
theorem CategoryTheory.Splitting.section_π_assoc {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) {Z : 𝒜} (h : C Z) :
@[simp]
theorem CategoryTheory.Splitting.section_π {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
@[simp]
theorem CategoryTheory.Splitting.ι_retraction_assoc {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) {Z : 𝒜} (h : A Z) :
@[simp]
theorem CategoryTheory.Splitting.ι_retraction {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
@[simp]
theorem CategoryTheory.Splitting.section_retraction_assoc {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) {Z : 𝒜} (h : A Z) :
@[simp]
theorem CategoryTheory.Splitting.section_retraction {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
def CategoryTheory.Splitting.splitMono {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :

The retraction in a splitting is a split mono.

Instances For
def CategoryTheory.Splitting.splitEpi {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :

The section in a splitting is a split epi.

Instances For
@[simp]
theorem CategoryTheory.Splitting.inr_iso_inv_assoc {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) {Z : 𝒜} (h : B Z) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp h.iso.inv h) =
@[simp]
theorem CategoryTheory.Splitting.inr_iso_inv {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h.iso.inv =
@[simp]
theorem CategoryTheory.Splitting.iso_hom_fst_assoc {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) {Z : 𝒜} (h : A Z) :
CategoryTheory.CategoryStruct.comp h.iso.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) =
@[simp]
theorem CategoryTheory.Splitting.iso_hom_fst {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
CategoryTheory.CategoryStruct.comp h.iso.hom CategoryTheory.Limits.biprod.fst =
def CategoryTheory.Splitting.splittingOfIsIsoZero {𝒜 : Type u_1} [] {X : 𝒜} {Y : 𝒜} {Z : 𝒜} (f : X Y) (hZ : ) :

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

Instances For
theorem CategoryTheory.Splitting.mono {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Splitting.epi {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
instance CategoryTheory.Splitting.instMonoSection {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
instance CategoryTheory.Splitting.instEpiRetraction {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Splitting.split_add {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Splitting.retraction_ι_eq_id_sub_assoc {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) {Z : 𝒜} (h : B Z) :
theorem CategoryTheory.Splitting.retraction_ι_eq_id_sub {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Splitting.π_section_eq_id_sub_assoc {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) {Z : 𝒜} (h : B Z) :
theorem CategoryTheory.Splitting.π_section_eq_id_sub {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Splitting.splittings_comm {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) (h' : ) :
theorem CategoryTheory.Splitting.split {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Splitting.comp_eq_zero_assoc {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) {Z : 𝒜} (h : C Z) :
theorem CategoryTheory.Splitting.comp_eq_zero {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Splitting.exact {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :
theorem CategoryTheory.Splitting.shortExact {𝒜 : Type u_1} [] {A : 𝒜} {B : 𝒜} {C : 𝒜} {f : A B} {g : B C} (h : ) :