mathlib3 documentation

algebra.homology.short_exact.preadditive

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.

See also #

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

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.

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

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

structure category_theory.split {𝒜 : Type u_1} [category_theory.category 𝒜] {A B C : 𝒜} (f : A B) (g : B C) [category_theory.preadditive 𝒜] :
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} [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) :
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) :
@[nolint]

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

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

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} [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'
@[simp]
@[protected]

The retraction in a splitting is a split mono.

Equations
@[protected]

The section in a splitting is a split epi.

Equations
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'
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'