algebra.homology.short_exact.preadditive

source

structure category_theory.short_exact {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} (f : A ⟶ B) (g : B ⟶ C) [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] :

Prop

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.

source

structure category_theory.left_split {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} (f : A ⟶ B) (g : B ⟶ C) [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] :

Prop

left_split : ∃ (φ : B ⟶ A), f ≫ φ = 𝟙 A
epi : category_theory.epi g
exact : category_theory.exact f g

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

source

theorem category_theory.left_split.short_exact {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] {f : A ⟶ B} {g : B ⟶ C} (h : category_theory.left_split f g) :

category_theory.short_exact f g

source

structure category_theory.right_split {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} (f : A ⟶ B) (g : B ⟶ C) [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] :

Prop

right_split : ∃ (χ : C ⟶ B), χ ≫ g = 𝟙 C
mono : category_theory.mono f
exact : category_theory.exact f g

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

source

theorem category_theory.right_split.short_exact {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] {f : A ⟶ B} {g : B ⟶ C} (h : category_theory.right_split f g) :

category_theory.short_exact f g

source

structure category_theory.split {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} (f : A ⟶ B) (g : B ⟶ C) [category_theory.preadditive 𝒜] :

Prop

split : ∃ (φ : B ⟶ A) (χ : C ⟶ B), f ≫ φ = 𝟙 A ∧ χ ≫ g = 𝟙 C ∧ f ≫ g = 0 ∧ χ ≫ φ = 0 ∧ φ ≫ f + g ≫ χ = 𝟙 B

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

source

theorem category_theory.exact_of_split {𝒜 : Type u_1} [category_theory.category 𝒜] [category_theory.preadditive 𝒜] [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} {χ : C ⟶ B} {φ : B ⟶ A} (hfg : f ≫ g = 0) (H : φ ≫ f + g ≫ χ = 𝟙 B) :

category_theory.exact f g

source

theorem category_theory.split.exact {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] (h : category_theory.split f g) :

category_theory.exact f g

source

theorem category_theory.split.left_split {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] (h : category_theory.split f g) :

category_theory.left_split f g

source

theorem category_theory.split.right_split {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] (h : category_theory.split f g) :

category_theory.right_split f g

source

theorem category_theory.split.short_exact {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] (h : category_theory.split f g) :

category_theory.short_exact f g

source

theorem category_theory.split.map {𝒜 : Type u_1} {ℬ : Type u_2} [category_theory.category 𝒜] [category_theory.preadditive 𝒜] [category_theory.category ℬ] [category_theory.preadditive ℬ] (F : 𝒜 ⥤ ℬ) [F.additive] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} (h : category_theory.split f g) :

category_theory.split (F.map f) (F.map g)

source

theorem category_theory.exact_inl_snd {𝒜 : Type u_1} [category_theory.category 𝒜] [category_theory.preadditive 𝒜] [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (A B : 𝒜) :

category_theory.exact category_theory.limits.biprod.inl category_theory.limits.biprod.snd

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

source

theorem category_theory.exact_inr_fst {𝒜 : Type u_1} [category_theory.category 𝒜] [category_theory.preadditive 𝒜] [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (A B : 𝒜) :

category_theory.exact category_theory.limits.biprod.inr category_theory.limits.biprod.fst

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

source

@[nolint]

structure category_theory.splitting {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} (f : A ⟶ B) (g : B ⟶ C) [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] :

Type u_2

iso : B ≅ A ⊞ C
comp_iso_eq_inl : f ≫ self.iso.hom = category_theory.limits.biprod.inl
iso_comp_snd_eq : self.iso.hom ≫ category_theory.limits.biprod.snd = g

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

source

@[simp]

theorem category_theory.splitting.iso_comp_snd_eq_assoc {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (self : category_theory.splitting f g) {X' : 𝒜} (f' : C ⟶ X') :

self.iso.hom ≫ category_theory.limits.biprod.snd ≫ f' = g ≫ f'

source

@[simp]

theorem category_theory.splitting.comp_iso_eq_inl_assoc {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (self : category_theory.splitting f g) {X' : 𝒜} (f' : A ⊞ C ⟶ X') :

f ≫ self.iso.hom ≫ f' = category_theory.limits.biprod.inl ≫ f'

source

@[simp]

theorem category_theory.splitting.inl_comp_iso_eq {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

category_theory.limits.biprod.inl ≫ h.iso.inv = f

source

@[simp]

theorem category_theory.splitting.inl_comp_iso_eq_assoc {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) {X' : 𝒜} (f' : B ⟶ X') :

category_theory.limits.biprod.inl ≫ h.iso.inv ≫ f' = f ≫ f'

source

@[simp]

theorem category_theory.splitting.iso_comp_eq_snd_assoc {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) {X' : 𝒜} (f' : C ⟶ X') :

h.iso.inv ≫ g ≫ f' = category_theory.limits.biprod.snd ≫ f'

source

@[simp]

theorem category_theory.splitting.iso_comp_eq_snd {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

h.iso.inv ≫ g = category_theory.limits.biprod.snd

source

noncomputable def category_theory.splitting.section {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f 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

h.section = category_theory.limits.biprod.inr ≫ h.iso.inv

Instances for category_theory.splitting.section

category_theory.splitting.section.category_theory.mono

source

noncomputable def category_theory.splitting.retraction {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f 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

h.retraction = h.iso.hom ≫ category_theory.limits.biprod.fst

Instances for category_theory.splitting.retraction

category_theory.splitting.retraction.category_theory.epi

source

@[simp]

theorem category_theory.splitting.section_π_assoc {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) {X' : 𝒜} (f' : C ⟶ X') :

h.section ≫ g ≫ f' = f'

source

@[simp]

theorem category_theory.splitting.section_π {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

h.section ≫ g = 𝟙 C

source

@[simp]

theorem category_theory.splitting.ι_retraction_assoc {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) {X' : 𝒜} (f' : A ⟶ X') :

f ≫ h.retraction ≫ f' = f'

source

@[simp]

theorem category_theory.splitting.ι_retraction {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

f ≫ h.retraction = 𝟙 A

source

@[simp]

theorem category_theory.splitting.section_retraction_assoc {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) {X' : 𝒜} (f' : A ⟶ X') :

h.section ≫ h.retraction ≫ f' = 0 ≫ f'

source

@[simp]

theorem category_theory.splitting.section_retraction {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

h.section ≫ h.retraction = 0

source

@[protected]

noncomputable def category_theory.splitting.split_mono {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

category_theory.split_mono f

The retraction in a splitting is a split mono.

Equations

h.split_mono = {retraction := h.retraction, id' := _}

source

@[protected]

noncomputable def category_theory.splitting.split_epi {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

category_theory.split_epi g

The section in a splitting is a split epi.

Equations

h.split_epi = {section_ := h.section, id' := _}

source

@[simp]

theorem category_theory.splitting.inr_iso_inv {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

category_theory.limits.biprod.inr ≫ h.iso.inv = h.section

source

@[simp]

theorem category_theory.splitting.inr_iso_inv_assoc {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) {X' : 𝒜} (f' : B ⟶ X') :

category_theory.limits.biprod.inr ≫ h.iso.inv ≫ f' = h.section ≫ f'

source

@[simp]

theorem category_theory.splitting.iso_hom_fst_assoc {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) {X' : 𝒜} (f' : A ⟶ X') :

h.iso.hom ≫ category_theory.limits.biprod.fst ≫ f' = h.retraction ≫ f'

source

@[simp]

theorem category_theory.splitting.iso_hom_fst {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

h.iso.hom ≫ category_theory.limits.biprod.fst = h.retraction

source

noncomputable def category_theory.splitting.splitting_of_is_iso_zero {𝒜 : Type u_1} [category_theory.category 𝒜] [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] {X Y Z : 𝒜} (f : X ⟶ Y) [category_theory.is_iso f] (hZ : category_theory.limits.is_zero Z) :

category_theory.splitting f 0

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

category_theory.splitting.splitting_of_is_iso_zero f hZ = {iso := (category_theory.as_iso f).symm ≪≫ category_theory.limits.iso_biprod_zero hZ, comp_iso_eq_inl := _, iso_comp_snd_eq := _}

source

@[protected]

theorem category_theory.splitting.mono {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

category_theory.mono f

source

@[protected]

theorem category_theory.splitting.epi {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

category_theory.epi g

source

@[protected, instance]

def category_theory.splitting.section.category_theory.mono {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

category_theory.mono h.section

source

@[protected, instance]

def category_theory.splitting.retraction.category_theory.epi {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.limits.has_zero_morphisms 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

category_theory.epi h.retraction

source

theorem category_theory.splitting.split_add {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

h.retraction ≫ f + g ≫ h.section = 𝟙 B

source

theorem category_theory.splitting.retraction_ι_eq_id_sub {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

h.retraction ≫ f = 𝟙 B - g ≫ h.section

source

theorem category_theory.splitting.retraction_ι_eq_id_sub_assoc {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) {X' : 𝒜} (f' : B ⟶ X') :

h.retraction ≫ f ≫ f' = (𝟙 B - g ≫ h.section) ≫ f'

source

theorem category_theory.splitting.π_section_eq_id_sub_assoc {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) {X' : 𝒜} (f' : B ⟶ X') :

g ≫ h.section ≫ f' = (𝟙 B - h.retraction ≫ f) ≫ f'

source

theorem category_theory.splitting.π_section_eq_id_sub {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

g ≫ h.section = 𝟙 B - h.retraction ≫ f

source

theorem category_theory.splitting.splittings_comm {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h h' : category_theory.splitting f g) :

h'.section ≫ h.retraction = -h.section ≫ h'.retraction

source

theorem category_theory.splitting.split {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

category_theory.split f g

source

theorem category_theory.splitting.comp_eq_zero_assoc {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) {X' : 𝒜} (f' : C ⟶ X') :

f ≫ g ≫ f' = 0 ≫ f'

source

theorem category_theory.splitting.comp_eq_zero {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) :

f ≫ g = 0

source

@[protected]

theorem category_theory.splitting.exact {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] [category_theory.limits.has_zero_object 𝒜] [category_theory.limits.has_cokernels 𝒜] :

category_theory.exact f g

source

@[protected]

theorem category_theory.splitting.short_exact {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} {f : A ⟶ B} {g : B ⟶ C} [category_theory.preadditive 𝒜] [category_theory.limits.has_binary_biproducts 𝒜] (h : category_theory.splitting f g) [category_theory.limits.has_kernels 𝒜] [category_theory.limits.has_images 𝒜] [category_theory.limits.has_zero_object 𝒜] [category_theory.limits.has_cokernels 𝒜] :

category_theory.short_exact f g

mathlib3 documentation

Short exact sequences, and splittings. #

See also #