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.
See also #
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}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
:
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.
- mono : CategoryTheory.Mono f
- epi : CategoryTheory.Epi g
- exact : CategoryTheory.Exact f g
Instances For
structure
CategoryTheory.LeftSplit
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
:
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).
- left_split : ∃ (φ : B ⟶ A), CategoryTheory.CategoryStruct.comp f φ = CategoryTheory.CategoryStruct.id A
- epi : CategoryTheory.Epi g
- exact : CategoryTheory.Exact f g
Instances For
theorem
CategoryTheory.LeftSplit.shortExact
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
{f : A ⟶ B}
{g : B ⟶ C}
(h : CategoryTheory.LeftSplit f g)
:
structure
CategoryTheory.RightSplit
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
:
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).
- right_split : ∃ (χ : C ⟶ B), CategoryTheory.CategoryStruct.comp χ g = CategoryTheory.CategoryStruct.id C
- mono : CategoryTheory.Mono f
- exact : CategoryTheory.Exact f g
Instances For
theorem
CategoryTheory.RightSplit.shortExact
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
{f : A ⟶ B}
{g : B ⟶ C}
(h : CategoryTheory.RightSplit f g)
:
structure
CategoryTheory.Split
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Preadditive 𝒜]
:
An exact sequence A -f⟶ B -g⟶ C is split if there exist
φ : B ⟶ A and χ : C ⟶ B such that:
f ≫ φ = 𝟙 Aχ ≫ g = 𝟙 Cf ≫ g = 0χ ≫ φ = 0φ ≫ f + g ≫ χ = 𝟙 B
Such a sequence is automatically short exact (i.e., f is mono and g is epi).
- split : ∃ (φ : B ⟶ A) (χ : C ⟶ B), CategoryTheory.CategoryStruct.comp f φ = CategoryTheory.CategoryStruct.id A ∧ CategoryTheory.CategoryStruct.comp χ g = CategoryTheory.CategoryStruct.id C ∧ CategoryTheory.CategoryStruct.comp f g = 0 ∧ CategoryTheory.CategoryStruct.comp χ φ = 0 ∧ CategoryTheory.CategoryStruct.comp φ f + CategoryTheory.CategoryStruct.comp g χ = CategoryTheory.CategoryStruct.id B
Instances For
theorem
CategoryTheory.exact_of_split
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
{χ : C ⟶ B}
{φ : B ⟶ A}
(hfg : CategoryTheory.CategoryStruct.comp f g = 0)
(H : CategoryTheory.CategoryStruct.comp φ f + CategoryTheory.CategoryStruct.comp g χ = CategoryTheory.CategoryStruct.id B)
:
theorem
CategoryTheory.Split.exact
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
(h : CategoryTheory.Split f g)
:
theorem
CategoryTheory.Split.leftSplit
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
(h : CategoryTheory.Split f g)
:
theorem
CategoryTheory.Split.rightSplit
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
(h : CategoryTheory.Split f g)
:
theorem
CategoryTheory.Split.shortExact
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
(h : CategoryTheory.Split f g)
:
theorem
CategoryTheory.Split.map
{𝒜 : Type u_2}
{ℬ : Type u_3}
[CategoryTheory.Category.{u_4, u_2} 𝒜]
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Category.{u_5, u_3} ℬ]
[CategoryTheory.Preadditive ℬ]
(F : CategoryTheory.Functor 𝒜 ℬ)
[CategoryTheory.Functor.Additive F]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
(h : CategoryTheory.Split f g)
:
CategoryTheory.Split (F.map f) (F.map g)
theorem
CategoryTheory.exact_inl_snd
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(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}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(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}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
:
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.
- comp_iso_eq_inl : CategoryTheory.CategoryStruct.comp f s.iso.hom = CategoryTheory.Limits.biprod.inl
- iso_comp_snd_eq : CategoryTheory.CategoryStruct.comp s.iso.hom CategoryTheory.Limits.biprod.snd = g
Instances For
@[simp]
theorem
CategoryTheory.Splitting.comp_iso_eq_inl_assoc
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(self : CategoryTheory.Splitting f g)
{Z : 𝒜}
(h : A ⊞ C ⟶ Z)
:
CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp self.iso.hom h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h
@[simp]
theorem
CategoryTheory.Splitting.iso_comp_snd_eq_assoc
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(self : CategoryTheory.Splitting f g)
{Z : 𝒜}
(h : C ⟶ Z)
:
CategoryTheory.CategoryStruct.comp self.iso.hom
(CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h) = CategoryTheory.CategoryStruct.comp g h
@[simp]
theorem
CategoryTheory.Splitting.inl_comp_iso_eq_assoc
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
{Z : 𝒜}
(h : B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl (CategoryTheory.CategoryStruct.comp h✝.iso.inv h) = CategoryTheory.CategoryStruct.comp f h
@[simp]
theorem
CategoryTheory.Splitting.inl_comp_iso_eq
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl h.iso.inv = f
@[simp]
theorem
CategoryTheory.Splitting.iso_comp_eq_snd_assoc
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
{Z : 𝒜}
(h : C ⟶ Z)
:
CategoryTheory.CategoryStruct.comp h✝.iso.inv (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.snd h
@[simp]
theorem
CategoryTheory.Splitting.iso_comp_eq_snd
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
CategoryTheory.CategoryStruct.comp h.iso.inv g = CategoryTheory.Limits.biprod.snd
def
CategoryTheory.Splitting.section
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.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
- CategoryTheory.Splitting.section h = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h.iso.inv
Instances For
def
CategoryTheory.Splitting.retraction
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.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
- CategoryTheory.Splitting.retraction h = CategoryTheory.CategoryStruct.comp h.iso.hom CategoryTheory.Limits.biprod.fst
Instances For
@[simp]
theorem
CategoryTheory.Splitting.section_π_assoc
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
{Z : 𝒜}
(h : C ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Splitting.section_π
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
@[simp]
theorem
CategoryTheory.Splitting.ι_retraction_assoc
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
{Z : 𝒜}
(h : A ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Splitting.ι_retraction
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
@[simp]
theorem
CategoryTheory.Splitting.section_retraction_assoc
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
{Z : 𝒜}
(h : A ⟶ Z)
:
@[simp]
theorem
CategoryTheory.Splitting.section_retraction
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
def
CategoryTheory.Splitting.splitMono
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
The retraction in a splitting is a split mono.
Equations
Instances For
def
CategoryTheory.Splitting.splitEpi
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
The section in a splitting is a split epi.
Equations
Instances For
@[simp]
theorem
CategoryTheory.Splitting.inr_iso_inv_assoc
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
{Z : 𝒜}
(h : B ⟶ Z)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr (CategoryTheory.CategoryStruct.comp h✝.iso.inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Splitting.section h✝) h
@[simp]
theorem
CategoryTheory.Splitting.inr_iso_inv
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inr h.iso.inv = CategoryTheory.Splitting.section h
@[simp]
theorem
CategoryTheory.Splitting.iso_hom_fst_assoc
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
{Z : 𝒜}
(h : A ⟶ Z)
:
CategoryTheory.CategoryStruct.comp h✝.iso.hom (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Splitting.retraction h✝) h
@[simp]
theorem
CategoryTheory.Splitting.iso_hom_fst
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
CategoryTheory.CategoryStruct.comp h.iso.hom CategoryTheory.Limits.biprod.fst = CategoryTheory.Splitting.retraction h
def
CategoryTheory.Splitting.splittingOfIsIsoZero
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
{X : 𝒜}
{Y : 𝒜}
{Z : 𝒜}
(f : X ⟶ Y)
[CategoryTheory.IsIso f]
(hZ : CategoryTheory.Limits.IsZero Z)
:
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
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Splitting.mono
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
theorem
CategoryTheory.Splitting.epi
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
instance
CategoryTheory.Splitting.instMonoSection
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
Equations
instance
CategoryTheory.Splitting.instEpiRetraction
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Limits.HasZeroMorphisms 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
Equations
theorem
CategoryTheory.Splitting.split_add
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
theorem
CategoryTheory.Splitting.retraction_ι_eq_id_sub_assoc
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
{Z : 𝒜}
(h : B ⟶ Z)
:
theorem
CategoryTheory.Splitting.retraction_ι_eq_id_sub
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
theorem
CategoryTheory.Splitting.π_section_eq_id_sub_assoc
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
{Z : 𝒜}
(h : B ⟶ Z)
:
theorem
CategoryTheory.Splitting.π_section_eq_id_sub
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
theorem
CategoryTheory.Splitting.splittings_comm
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
(h' : CategoryTheory.Splitting f g)
:
theorem
CategoryTheory.Splitting.split
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
theorem
CategoryTheory.Splitting.comp_eq_zero_assoc
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
{Z : 𝒜}
(h : C ⟶ Z)
:
theorem
CategoryTheory.Splitting.comp_eq_zero
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
:
theorem
CategoryTheory.Splitting.exact
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
[CategoryTheory.Limits.HasZeroObject 𝒜]
[CategoryTheory.Limits.HasCokernels 𝒜]
:
theorem
CategoryTheory.Splitting.shortExact
{𝒜 : Type u_1}
[CategoryTheory.Category.{u_2, u_1} 𝒜]
{A : 𝒜}
{B : 𝒜}
{C : 𝒜}
{f : A ⟶ B}
{g : B ⟶ C}
[CategoryTheory.Preadditive 𝒜]
[CategoryTheory.Limits.HasBinaryBiproducts 𝒜]
(h : CategoryTheory.Splitting f g)
[CategoryTheory.Limits.HasKernels 𝒜]
[CategoryTheory.Limits.HasImages 𝒜]
[CategoryTheory.Limits.HasZeroObject 𝒜]
[CategoryTheory.Limits.HasCokernels 𝒜]
: