Exact sequences #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In a category with zero morphisms, images, and equalizers we say that f : A ⟶ B and g : B ⟶ C
are exact if f ≫ g = 0 and the natural map image f ⟶ kernel g is an epimorphism.
In any preadditive category this is equivalent to the homology at B vanishing.
However in general it is weaker than other reasonable definitions of exactness, particularly that
- the inclusion map
image.ι fis a kernel ofgor image f ⟶ kernel gis an isomorphism orimage_subobject f = kernel_subobject f. However when the category is abelian, these all become equivalent; these results are found incategory_theory/abelian/exact.lean.
Main results #
- Suppose that cokernels exist and that
fandgare exact. Ifsis any kernel fork overgandtis any cokernel cofork overf, thenfork.ι s ≫ cofork.π t = 0. - Precomposing the first morphism with an epimorphism retains exactness. Postcomposing the second morphism with a monomorphism retains exactness.
- If
fandgare exact andiis an isomorphism, thenf ≫ i.homandi.inv ≫ gare also exact.
Future work #
- Short exact sequences, split exact sequences, the splitting lemma (maybe only for abelian categories?)
- Two adjacent maps in a chain complex are exact iff the homology vanishes
structure
category_theory.exact
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C) :
Prop
- w : f ≫ g = 0
- epi : category_theory.epi (image_to_kernel f g _)
Two morphisms f : A ⟶ B, g : B ⟶ C are called exact if w : f ≫ g = 0 and the natural map
image_to_kernel f g w : image_subobject f ⟶ kernel_subobject g is an epimorphism.
In any preadditive category, this is equivalent to w : f ≫ g = 0 and homology f g w ≅ 0.
In an abelian category, this is equivalent to image_to_kernel f g w being an isomorphism,
and hence equivalent to the usual definition,
image_subobject f = kernel_subobject g.
theorem
category_theory.exact.w_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
{A B C : V}
{f : A ⟶ B}
{g : B ⟶ C}
(self : category_theory.exact f g)
{X' : V}
(f' : C ⟶ X') :
theorem
category_theory.preadditive.exact_iff_homology_zero
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_object V]
[category_theory.preadditive V]
[category_theory.limits.has_kernels V]
[category_theory.limits.has_cokernels V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C) :
In any preadditive category,
composable morphisms f g are exact iff they compose to zero and the homology vanishes.
theorem
category_theory.preadditive.exact_of_iso_of_exact
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_object V]
[category_theory.preadditive V]
[category_theory.limits.has_kernels V]
[category_theory.limits.has_cokernels V]
{A₁ B₁ C₁ A₂ B₂ C₂ : V}
(f₁ : A₁ ⟶ B₁)
(g₁ : B₁ ⟶ C₁)
(f₂ : A₂ ⟶ B₂)
(g₂ : B₂ ⟶ C₂)
(α : category_theory.arrow.mk f₁ ≅ category_theory.arrow.mk f₂)
(β : category_theory.arrow.mk g₁ ≅ category_theory.arrow.mk g₂)
(p : α.hom.right = β.hom.left)
(h : category_theory.exact f₁ g₁) :
category_theory.exact f₂ g₂
theorem
category_theory.preadditive.exact_of_iso_of_exact'
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_object V]
[category_theory.preadditive V]
[category_theory.limits.has_kernels V]
[category_theory.limits.has_cokernels V]
{A₁ B₁ C₁ A₂ B₂ C₂ : V}
(f₁ : A₁ ⟶ B₁)
(g₁ : B₁ ⟶ C₁)
(f₂ : A₂ ⟶ B₂)
(g₂ : B₂ ⟶ C₂)
(α : A₁ ≅ A₂)
(β : B₁ ≅ B₂)
(γ : C₁ ≅ C₂)
(hsq₁ : α.hom ≫ f₂ = f₁ ≫ β.hom)
(hsq₂ : β.hom ≫ g₂ = g₁ ≫ γ.hom)
(h : category_theory.exact f₁ g₁) :
category_theory.exact f₂ g₂
A reformulation of preadditive.exact_of_iso_of_exact that does not involve the arrow
category.
theorem
category_theory.preadditive.exact_iff_exact_of_iso
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_object V]
[category_theory.preadditive V]
[category_theory.limits.has_kernels V]
[category_theory.limits.has_cokernels V]
{A₁ B₁ C₁ A₂ B₂ C₂ : V}
(f₁ : A₁ ⟶ B₁)
(g₁ : B₁ ⟶ C₁)
(f₂ : A₂ ⟶ B₂)
(g₂ : B₂ ⟶ C₂)
(α : category_theory.arrow.mk f₁ ≅ category_theory.arrow.mk f₂)
(β : category_theory.arrow.mk g₁ ≅ category_theory.arrow.mk g₂)
(p : α.hom.right = β.hom.left) :
category_theory.exact f₁ g₁ ↔ category_theory.exact f₂ g₂
theorem
category_theory.comp_eq_zero_of_image_eq_kernel
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
(p : category_theory.limits.image_subobject f = category_theory.limits.kernel_subobject g) :
theorem
category_theory.image_to_kernel_is_iso_of_image_eq_kernel
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
(p : category_theory.limits.image_subobject f = category_theory.limits.kernel_subobject g) :
theorem
category_theory.exact_of_image_eq_kernel
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
(p : category_theory.limits.image_subobject f = category_theory.limits.kernel_subobject g) :
theorem
category_theory.exact_comp_hom_inv_comp
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C D : V}
{f : A ⟶ B}
{g : B ⟶ C}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
(i : B ≅ D)
(h : category_theory.exact f g) :
category_theory.exact (f ≫ i.hom) (i.inv ≫ g)
theorem
category_theory.exact_comp_inv_hom_comp
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C D : V}
{f : A ⟶ B}
{g : B ⟶ C}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
(i : D ≅ B)
(h : category_theory.exact f g) :
category_theory.exact (f ≫ i.inv) (i.hom ≫ g)
theorem
category_theory.exact_comp_hom_inv_comp_iff
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C D : V}
{f : A ⟶ B}
{g : B ⟶ C}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
(i : B ≅ D) :
category_theory.exact (f ≫ i.hom) (i.inv ≫ g) ↔ category_theory.exact f g
theorem
category_theory.exact_epi_comp
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C D : V}
{f : A ⟶ B}
{g : B ⟶ C}
{h : C ⟶ D}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
(hgh : category_theory.exact g h)
[category_theory.epi f] :
category_theory.exact (f ≫ g) h
@[simp]
theorem
category_theory.exact_iso_comp
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C D : V}
{f : A ⟶ B}
{g : B ⟶ C}
{h : C ⟶ D}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
[category_theory.is_iso f] :
category_theory.exact (f ≫ g) h ↔ category_theory.exact g h
theorem
category_theory.exact_comp_mono
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C D : V}
{f : A ⟶ B}
{g : B ⟶ C}
{h : C ⟶ D}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
(hfg : category_theory.exact f g)
[category_theory.mono h] :
category_theory.exact f (g ≫ h)
theorem
category_theory.exact_comp_mono_iff
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C D : V}
{f : A ⟶ B}
{g : B ⟶ C}
{h : C ⟶ D}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
[category_theory.mono h] :
category_theory.exact f (g ≫ h) ↔ category_theory.exact f g
The dual of this lemma is only true when V is abelian, see abelian.exact_epi_comp_iff.
@[simp]
theorem
category_theory.exact_comp_iso
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C D : V}
{f : A ⟶ B}
{g : B ⟶ C}
{h : C ⟶ D}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
[category_theory.is_iso h] :
category_theory.exact f (g ≫ h) ↔ category_theory.exact f g
theorem
category_theory.exact_kernel_subobject_arrow
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B : V}
{f : A ⟶ B}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V] :
theorem
category_theory.exact_kernel_ι
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B : V}
{f : A ⟶ B}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V] :
@[protected, instance]
def
category_theory.limits.factor_thru_kernel_subobject.epi
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C : V}
{f : A ⟶ B}
{g : B ⟶ C}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
(h : category_theory.exact f g) :
@[protected, instance]
def
category_theory.limits.kernel.lift.epi
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C : V}
{f : A ⟶ B}
{g : B ⟶ C}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
(h : category_theory.exact f g) :
theorem
category_theory.kernel_subobject_arrow_eq_zero_of_exact_zero_left
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
(A : V)
{B C : V}
{g : B ⟶ C}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
(h : category_theory.exact 0 g) :
theorem
category_theory.kernel_ι_eq_zero_of_exact_zero_left
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
(A : V)
{B C : V}
{g : B ⟶ C}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
(h : category_theory.exact 0 g) :
theorem
category_theory.exact_zero_left_of_mono
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
(A : V)
{B C : V}
{g : B ⟶ C}
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_zero_object V]
[category_theory.mono g] :
@[simp]
theorem
category_theory.kernel_comp_cokernel
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
(h : category_theory.exact f g) :
@[simp]
theorem
category_theory.kernel_comp_cokernel_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
(h : category_theory.exact f g)
{X' : V}
(f' : category_theory.limits.cokernel f ⟶ X') :
category_theory.limits.kernel.ι g ≫ category_theory.limits.cokernel.π f ≫ f' = 0 ≫ f'
theorem
category_theory.comp_eq_zero_of_exact
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
(h : category_theory.exact f g)
{X Y : V}
{ι : X ⟶ B}
(hι : ι ≫ g = 0)
{π : B ⟶ Y}
(hπ : f ≫ π = 0) :
@[simp]
theorem
category_theory.fork_ι_comp_cofork_π
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
(h : category_theory.exact f g)
(s : category_theory.limits.kernel_fork g)
(t : category_theory.limits.cokernel_cofork f) :
@[simp]
theorem
category_theory.fork_ι_comp_cofork_π_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_cokernels V]
(h : category_theory.exact f g)
(s : category_theory.limits.kernel_fork g)
(t : category_theory.limits.cokernel_cofork f)
{X' : V}
(f' : ((category_theory.functor.const category_theory.limits.walking_parallel_pair).obj t.X).obj category_theory.limits.walking_parallel_pair.one ⟶ X') :
category_theory.limits.fork.ι s ≫ category_theory.limits.cofork.π t ≫ f' = 0 ≫ f'
theorem
category_theory.exact_of_zero
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
{A C : V}
(f : A ⟶ 0)
(g : 0 ⟶ C) :
theorem
category_theory.exact_zero_mono
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
{B C : V}
(f : B ⟶ C)
[category_theory.mono f] :
theorem
category_theory.exact_epi_zero
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
{A B : V}
(f : A ⟶ B)
[category_theory.epi f] :
theorem
category_theory.mono_iff_exact_zero_left
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_object V]
[category_theory.preadditive V]
[category_theory.limits.has_kernels V]
{B C : V}
(f : B ⟶ C) :
theorem
category_theory.epi_iff_exact_zero_right
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_object V]
[category_theory.preadditive V]
[category_theory.limits.has_equalizers V]
{A B : V}
(f : A ⟶ B) :
@[class]
structure
category_theory.functor.reflects_exact_sequences
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
{W : Type u₂}
[category_theory.category W]
[category_theory.limits.has_images W]
[category_theory.limits.has_zero_morphisms W]
[category_theory.limits.has_kernels W]
(F : V ⥤ W) :
- reflects : ∀ {A B C : V} (f : A ⟶ B) (g : B ⟶ C), category_theory.exact (F.map f) (F.map g) → category_theory.exact f g
A functor reflects exact sequences if any composable pair of morphisms that is mapped to an exact pair is itself exact.
Instances of this typeclass
Instances of other typeclasses for category_theory.functor.reflects_exact_sequences
- category_theory.functor.reflects_exact_sequences.has_sizeof_inst
theorem
category_theory.functor.exact_of_exact_map
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_images V]
[category_theory.limits.has_zero_morphisms V]
[category_theory.limits.has_kernels V]
{W : Type u₂}
[category_theory.category W]
[category_theory.limits.has_images W]
[category_theory.limits.has_zero_morphisms W]
[category_theory.limits.has_kernels W]
(F : V ⥤ W)
[F.reflects_exact_sequences]
{A B C : V}
{f : A ⟶ B}
{g : B ⟶ C}
(hfg : category_theory.exact (F.map f) (F.map g)) :