Image-to-kernel comparison maps #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
Whenever f : A ⟶ B and g : B ⟶ C satisfy w : f ≫ g = 0,
we have image_le_kernel f g w : image_subobject f ≤ kernel_subobject g
(assuming the appropriate images and kernels exist).
image_to_kernel f g w is the corresponding morphism between objects in C.
We define homology f g w of such a pair as the cokernel of image_to_kernel f g w.
theorem
image_le_kernel
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0) :
@[protected, instance]
def
image_to_kernel.mono
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0) :
category_theory.mono (image_to_kernel f g w)
noncomputable
def
image_to_kernel
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0) :
The canonical morphism image_subobject f ⟶ kernel_subobject g when f ≫ g = 0.
Equations
Instances for image_to_kernel
@[simp]
theorem
subobject_of_le_as_image_to_kernel
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
(h : category_theory.limits.image_subobject f ≤ category_theory.limits.kernel_subobject g) :
Prefer image_to_kernel.
@[simp]
theorem
image_to_kernel_arrow_apply
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
[I : category_theory.concrete_category V]
(x : ↥↑(category_theory.limits.image_subobject f)) :
⇑((category_theory.limits.kernel_subobject g).arrow) (⇑(image_to_kernel f g w) x) = ⇑((category_theory.limits.image_subobject f).arrow) x
@[simp]
theorem
image_to_kernel_arrow_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
{X' : V}
(f' : B ⟶ X') :
image_to_kernel f g w ≫ (category_theory.limits.kernel_subobject g).arrow ≫ f' = (category_theory.limits.image_subobject f).arrow ≫ f'
@[simp]
theorem
image_to_kernel_arrow
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0) :
theorem
factor_thru_image_subobject_comp_image_to_kernel
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0) :
@[simp]
theorem
image_to_kernel_zero_left
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(g : B ⟶ C)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_zero_object V]
{w : 0 ≫ g = 0} :
image_to_kernel 0 g w = 0
theorem
image_to_kernel_zero_right
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_images V]
{w : f ≫ 0 = 0} :
theorem
image_to_kernel_comp_right
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
{D : V}
(h : C ⟶ D)
(w : f ≫ g = 0) :
image_to_kernel f (g ≫ h) _ = image_to_kernel f g w ≫ (category_theory.limits.kernel_subobject g).of_le (category_theory.limits.kernel_subobject (g ≫ h)) _
theorem
image_to_kernel_comp_left
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
{Z : V}
(h : Z ⟶ A)
(w : f ≫ g = 0) :
image_to_kernel (h ≫ f) g _ = (category_theory.limits.image_subobject (h ≫ f)).of_le (category_theory.limits.image_subobject f) _ ≫ image_to_kernel f g w
@[simp]
theorem
image_to_kernel_comp_mono
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
{D : V}
(h : C ⟶ D)
[category_theory.mono h]
(w : f ≫ g ≫ h = 0) :
image_to_kernel f (g ≫ h) w = image_to_kernel f g _ ≫ ((category_theory.limits.kernel_subobject (g ≫ h)).iso_of_eq (category_theory.limits.kernel_subobject g) _).inv
@[simp]
theorem
image_to_kernel_epi_comp
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
{Z : V}
(h : Z ⟶ A)
[category_theory.epi h]
(w : (h ≫ f) ≫ g = 0) :
image_to_kernel (h ≫ f) g w = (category_theory.limits.image_subobject (h ≫ f)).of_le (category_theory.limits.image_subobject f) _ ≫ image_to_kernel f g _
@[simp]
theorem
image_to_kernel_comp_hom_inv_comp
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_equalizers V]
[category_theory.limits.has_images V]
{Z : V}
{i : B ≅ Z}
(w : (f ≫ i.hom) ≫ i.inv ≫ g = 0) :
image_to_kernel (f ≫ i.hom) (i.inv ≫ g) w = (category_theory.limits.image_subobject_comp_iso f i.hom).hom ≫ image_to_kernel f g _ ≫ (category_theory.limits.kernel_subobject_iso_comp i.inv g).inv
@[protected, instance]
def
image_to_kernel_epi_of_zero_of_mono
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(g : B ⟶ C)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_zero_object V]
[category_theory.mono g] :
category_theory.epi (image_to_kernel 0 g _)
image_to_kernel for A --0--> B --g--> C, where g is a mono is itself an epi
(i.e. the sequence is exact at B).
@[protected, instance]
def
image_to_kernel_epi_of_epi_of_zero
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_images V]
[category_theory.epi f] :
category_theory.epi (image_to_kernel f 0 _)
image_to_kernel for A --f--> B --0--> C, where g is an epi is itself an epi
(i.e. the sequence is exact at B).
noncomputable
def
homology
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
[category_theory.limits.has_cokernel (image_to_kernel f g w)] :
V
The homology of a pair of morphisms f : A ⟶ B and g : B ⟶ C satisfying f ≫ g = 0
is the cokernel of the image_to_kernel morphism for f and g.
Equations
- homology f g w = category_theory.limits.cokernel (image_to_kernel f g w)
noncomputable
def
homology.π
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
[category_theory.limits.has_cokernel (image_to_kernel f g w)] :
The morphism from cycles to homology.
Equations
- homology.π f g w = category_theory.limits.cokernel.π (image_to_kernel f g w)
@[simp]
theorem
homology.condition
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
[category_theory.limits.has_cokernel (image_to_kernel f g w)] :
image_to_kernel f g w ≫ homology.π f g w = 0
noncomputable
def
homology.desc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
[category_theory.limits.has_cokernel (image_to_kernel f g w)]
{D : V}
(k : ↑(category_theory.limits.kernel_subobject g) ⟶ D)
(p : image_to_kernel f g w ≫ k = 0) :
To construct a map out of homology, it suffices to construct a map out of the cycles which vanishes on boundaries.
Equations
- homology.desc f g w k p = category_theory.limits.cokernel.desc (image_to_kernel f g w) k p
@[simp]
theorem
homology.π_desc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
[category_theory.limits.has_cokernel (image_to_kernel f g w)]
{D : V}
(k : ↑(category_theory.limits.kernel_subobject g) ⟶ D)
(p : image_to_kernel f g w ≫ k = 0) :
homology.π f g w ≫ homology.desc f g w k p = k
@[simp]
theorem
homology.π_desc_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
[category_theory.limits.has_cokernel (image_to_kernel f g w)]
{D : V}
(k : ↑(category_theory.limits.kernel_subobject g) ⟶ D)
(p : image_to_kernel f g w ≫ k = 0)
{X' : V}
(f' : D ⟶ X') :
homology.π f g w ≫ homology.desc f g w k p ≫ f' = k ≫ f'
@[simp]
theorem
homology.π_desc_apply
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
[category_theory.limits.has_cokernel (image_to_kernel f g w)]
{D : V}
(k : ↑(category_theory.limits.kernel_subobject g) ⟶ D)
(p : image_to_kernel f g w ≫ k = 0)
[I : category_theory.concrete_category V]
(x : ↥↑(category_theory.limits.kernel_subobject g)) :
⇑(homology.desc f g w k p) (⇑(homology.π f g w) x) = ⇑k x
@[ext]
theorem
homology.ext
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
[category_theory.limits.has_cokernel (image_to_kernel f g w)]
{D : V}
{k k' : homology f g w ⟶ D}
(p : homology.π f g w ≫ k = homology.π f g w ≫ k') :
k = k'
To check two morphisms out of homology f g w are equal, it suffices to check on cycles.
noncomputable
def
homology_of_zero_right
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
[category_theory.limits.has_image f]
[category_theory.limits.has_cokernel (image_to_kernel f 0 category_theory.limits.comp_zero)]
[category_theory.limits.has_cokernel f]
[category_theory.limits.has_cokernel (category_theory.limits.image.ι f)]
[category_theory.epi (category_theory.limits.factor_thru_image f)] :
The cokernel of the map Im f ⟶ Ker 0 is isomorphic to the cokernel of f.
Equations
- homology_of_zero_right f = category_theory.limits.cokernel.map_iso (image_to_kernel f 0 category_theory.limits.comp_zero) (category_theory.limits.image.ι f) (category_theory.limits.image_subobject_iso f) (category_theory.limits.kernel_subobject_iso 0 ≪≫ category_theory.limits.kernel_zero_iso_source) _ ≪≫ category_theory.limits.cokernel_image_ι f
noncomputable
def
homology_of_zero_left
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(g : B ⟶ C)
[category_theory.limits.has_kernel g]
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_kernels V]
[category_theory.limits.has_image 0]
[category_theory.limits.has_cokernel (image_to_kernel 0 g category_theory.limits.zero_comp)] :
The kernel of the map Im 0 ⟶ Ker f is isomorphic to the kernel of f.
@[simp]
theorem
homology_zero_zero_inv
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_image 0]
[category_theory.limits.has_cokernel (image_to_kernel 0 0 homology_zero_zero._proof_3)] :
homology_zero_zero.inv = category_theory.inv (category_theory.limits.kernel_subobject 0).arrow ≫ homology.π 0 0 homology_zero_zero._proof_15
noncomputable
def
homology_zero_zero
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_image 0]
[category_theory.limits.has_cokernel (image_to_kernel 0 0 homology_zero_zero._proof_3)] :
homology 0 0 _ is just the middle object.
Equations
- homology_zero_zero = {hom := homology.desc 0 0 homology_zero_zero._proof_12 (category_theory.limits.kernel_subobject 0).arrow homology_zero_zero._proof_13, inv := category_theory.inv (category_theory.limits.kernel_subobject 0).arrow ≫ homology.π 0 0 homology_zero_zero._proof_15, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
homology_zero_zero_hom
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
[category_theory.limits.has_zero_object V]
[category_theory.limits.has_image 0]
[category_theory.limits.has_cokernel (image_to_kernel 0 0 homology_zero_zero._proof_3)] :
homology_zero_zero.hom = homology.desc 0 0 homology_zero_zero._proof_12 (category_theory.limits.kernel_subobject 0).arrow homology_zero_zero._proof_13
theorem
image_subobject_map_comp_image_to_kernel
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
[category_theory.limits.has_image f]
{g : B ⟶ C}
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
{A' B' C' : V}
{f' : A' ⟶ B'}
[category_theory.limits.has_image f']
{g' : B' ⟶ C'}
[category_theory.limits.has_kernel g']
(w' : f' ≫ g' = 0)
(α : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
[category_theory.limits.has_image_map α]
(β : category_theory.arrow.mk g ⟶ category_theory.arrow.mk g')
(p : α.right = β.left) :
Given compatible commutative squares between
a pair f g and a pair f' g' satisfying f ≫ g = 0 and f' ≫ g' = 0,
the image_to_kernel morphisms intertwine the induced map on kernels and the induced map on images.
theorem
image_subobject_map_comp_image_to_kernel_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
[category_theory.limits.has_image f]
{g : B ⟶ C}
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
{A' B' C' : V}
{f' : A' ⟶ B'}
[category_theory.limits.has_image f']
{g' : B' ⟶ C'}
[category_theory.limits.has_kernel g']
(w' : f' ≫ g' = 0)
(α : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
[category_theory.limits.has_image_map α]
(β : category_theory.arrow.mk g ⟶ category_theory.arrow.mk g')
(p : α.right = β.left)
{X' : V}
(f'_1 : ↑(category_theory.limits.kernel_subobject g') ⟶ X') :
image_to_kernel f g w ≫ category_theory.limits.kernel_subobject_map β ≫ f'_1 = category_theory.limits.image_subobject_map α ≫ image_to_kernel f' g' w' ≫ f'_1
noncomputable
def
homology.map
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
[category_theory.limits.has_image f]
{g : B ⟶ C}
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
{A' B' C' : V}
{f' : A' ⟶ B'}
[category_theory.limits.has_image f']
{g' : B' ⟶ C'}
[category_theory.limits.has_kernel g']
(w' : f' ≫ g' = 0)
(α : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
[category_theory.limits.has_image_map α]
(β : category_theory.arrow.mk g ⟶ category_theory.arrow.mk g')
[category_theory.limits.has_cokernel (image_to_kernel f g w)]
[category_theory.limits.has_cokernel (image_to_kernel f' g' w')]
(p : α.right = β.left) :
Given compatible commutative squares between
a pair f g and a pair f' g' satisfying f ≫ g = 0 and f' ≫ g' = 0,
we get a morphism on homology.
Equations
- homology.map w w' α β p = category_theory.limits.cokernel.desc (image_to_kernel f g w) (category_theory.limits.kernel_subobject_map β ≫ category_theory.limits.cokernel.π (image_to_kernel f' g' w')) _
@[simp]
theorem
homology.π_map_apply
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
[category_theory.limits.has_image f]
{g : B ⟶ C}
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
{A' B' C' : V}
{f' : A' ⟶ B'}
[category_theory.limits.has_image f']
{g' : B' ⟶ C'}
[category_theory.limits.has_kernel g']
(w' : f' ≫ g' = 0)
(α : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
[category_theory.limits.has_image_map α]
(β : category_theory.arrow.mk g ⟶ category_theory.arrow.mk g')
[category_theory.limits.has_cokernel (image_to_kernel f g w)]
[category_theory.limits.has_cokernel (image_to_kernel f' g' w')]
(p : α.right = β.left)
[I : category_theory.concrete_category V]
(x : ↥↑(category_theory.limits.kernel_subobject g)) :
⇑(homology.map w w' α β p) (⇑(homology.π f g w) x) = ⇑(homology.π f' g' w') (⇑(category_theory.limits.kernel_subobject_map β) x)
@[simp]
theorem
homology.π_map_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
[category_theory.limits.has_image f]
{g : B ⟶ C}
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
{A' B' C' : V}
{f' : A' ⟶ B'}
[category_theory.limits.has_image f']
{g' : B' ⟶ C'}
[category_theory.limits.has_kernel g']
(w' : f' ≫ g' = 0)
(α : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
[category_theory.limits.has_image_map α]
(β : category_theory.arrow.mk g ⟶ category_theory.arrow.mk g')
[category_theory.limits.has_cokernel (image_to_kernel f g w)]
[category_theory.limits.has_cokernel (image_to_kernel f' g' w')]
(p : α.right = β.left)
{X' : V}
(f'_1 : homology f' g' w' ⟶ X') :
homology.π f g w ≫ homology.map w w' α β p ≫ f'_1 = category_theory.limits.kernel_subobject_map β ≫ homology.π f' g' w' ≫ f'_1
@[simp]
theorem
homology.π_map
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
[category_theory.limits.has_image f]
{g : B ⟶ C}
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
{A' B' C' : V}
{f' : A' ⟶ B'}
[category_theory.limits.has_image f']
{g' : B' ⟶ C'}
[category_theory.limits.has_kernel g']
(w' : f' ≫ g' = 0)
(α : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
[category_theory.limits.has_image_map α]
(β : category_theory.arrow.mk g ⟶ category_theory.arrow.mk g')
[category_theory.limits.has_cokernel (image_to_kernel f g w)]
[category_theory.limits.has_cokernel (image_to_kernel f' g' w')]
(p : α.right = β.left) :
homology.π f g w ≫ homology.map w w' α β p = category_theory.limits.kernel_subobject_map β ≫ homology.π f' g' w'
@[simp]
theorem
homology.map_desc_apply
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
[category_theory.limits.has_image f]
{g : B ⟶ C}
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
{A' B' C' : V}
{f' : A' ⟶ B'}
[category_theory.limits.has_image f']
{g' : B' ⟶ C'}
[category_theory.limits.has_kernel g']
(w' : f' ≫ g' = 0)
(α : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
[category_theory.limits.has_image_map α]
(β : category_theory.arrow.mk g ⟶ category_theory.arrow.mk g')
[category_theory.limits.has_cokernel (image_to_kernel f g w)]
[category_theory.limits.has_cokernel (image_to_kernel f' g' w')]
(p : α.right = β.left)
{D : V}
(k : ↑(category_theory.limits.kernel_subobject g') ⟶ D)
(z : image_to_kernel f' g' w' ≫ k = 0)
[I : category_theory.concrete_category V]
(x : ↥(homology f g w)) :
⇑(homology.desc f' g' w' k z) (⇑(homology.map w w' α β p) x) = ⇑(homology.desc f g w (category_theory.limits.kernel_subobject_map β ≫ k) _) x
@[simp]
theorem
homology.map_desc_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
[category_theory.limits.has_image f]
{g : B ⟶ C}
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
{A' B' C' : V}
{f' : A' ⟶ B'}
[category_theory.limits.has_image f']
{g' : B' ⟶ C'}
[category_theory.limits.has_kernel g']
(w' : f' ≫ g' = 0)
(α : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
[category_theory.limits.has_image_map α]
(β : category_theory.arrow.mk g ⟶ category_theory.arrow.mk g')
[category_theory.limits.has_cokernel (image_to_kernel f g w)]
[category_theory.limits.has_cokernel (image_to_kernel f' g' w')]
(p : α.right = β.left)
{D : V}
(k : ↑(category_theory.limits.kernel_subobject g') ⟶ D)
(z : image_to_kernel f' g' w' ≫ k = 0)
{X' : V}
(f'_1 : D ⟶ X') :
homology.map w w' α β p ≫ homology.desc f' g' w' k z ≫ f'_1 = homology.desc f g w (category_theory.limits.kernel_subobject_map β ≫ k) _ ≫ f'_1
@[simp]
theorem
homology.map_desc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
[category_theory.limits.has_image f]
{g : B ⟶ C}
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
{A' B' C' : V}
{f' : A' ⟶ B'}
[category_theory.limits.has_image f']
{g' : B' ⟶ C'}
[category_theory.limits.has_kernel g']
(w' : f' ≫ g' = 0)
(α : category_theory.arrow.mk f ⟶ category_theory.arrow.mk f')
[category_theory.limits.has_image_map α]
(β : category_theory.arrow.mk g ⟶ category_theory.arrow.mk g')
[category_theory.limits.has_cokernel (image_to_kernel f g w)]
[category_theory.limits.has_cokernel (image_to_kernel f' g' w')]
(p : α.right = β.left)
{D : V}
(k : ↑(category_theory.limits.kernel_subobject g') ⟶ D)
(z : image_to_kernel f' g' w' ≫ k = 0) :
homology.map w w' α β p ≫ homology.desc f' g' w' k z = homology.desc f g w (category_theory.limits.kernel_subobject_map β ≫ k) _
@[simp]
theorem
homology.map_id
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
[category_theory.limits.has_image f]
{g : B ⟶ C}
[category_theory.limits.has_kernel g]
(w : f ≫ g = 0)
[category_theory.limits.has_cokernel (image_to_kernel f g w)] :
homology.map w w (𝟙 (category_theory.arrow.mk f)) (𝟙 (category_theory.arrow.mk g)) rfl = 𝟙 (homology f g w)
theorem
homology.comp_right_eq_comp_left
{V : Type u_1}
[category_theory.category V]
{A₁ B₁ C₁ A₂ B₂ C₂ A₃ B₃ C₃ : V}
{f₁ : A₁ ⟶ B₁}
{g₁ : B₁ ⟶ C₁}
{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₂}
{α₂ : category_theory.arrow.mk f₂ ⟶ category_theory.arrow.mk f₃}
{β₂ : category_theory.arrow.mk g₂ ⟶ category_theory.arrow.mk g₃}
(p₁ : α₁.right = β₁.left)
(p₂ : α₂.right = β₂.left) :
Auxiliary lemma for homology computations.
theorem
homology.map_comp_assoc
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A₁ B₁ C₁ : V}
{f₁ : A₁ ⟶ B₁}
[category_theory.limits.has_image f₁]
{g₁ : B₁ ⟶ C₁}
[category_theory.limits.has_kernel g₁]
(w₁ : f₁ ≫ g₁ = 0)
{A₂ B₂ C₂ : V}
{f₂ : A₂ ⟶ B₂}
[category_theory.limits.has_image f₂]
{g₂ : B₂ ⟶ C₂}
[category_theory.limits.has_kernel g₂]
(w₂ : f₂ ≫ g₂ = 0)
{A₃ B₃ C₃ : V}
{f₃ : A₃ ⟶ B₃}
[category_theory.limits.has_image f₃]
{g₃ : B₃ ⟶ C₃}
[category_theory.limits.has_kernel g₃]
(w₃ : f₃ ≫ g₃ = 0)
(α₁ : category_theory.arrow.mk f₁ ⟶ category_theory.arrow.mk f₂)
[category_theory.limits.has_image_map α₁]
(β₁ : category_theory.arrow.mk g₁ ⟶ category_theory.arrow.mk g₂)
(α₂ : category_theory.arrow.mk f₂ ⟶ category_theory.arrow.mk f₃)
[category_theory.limits.has_image_map α₂]
(β₂ : category_theory.arrow.mk g₂ ⟶ category_theory.arrow.mk g₃)
[category_theory.limits.has_cokernel (image_to_kernel f₁ g₁ w₁)]
[category_theory.limits.has_cokernel (image_to_kernel f₂ g₂ w₂)]
[category_theory.limits.has_cokernel (image_to_kernel f₃ g₃ w₃)]
(p₁ : α₁.right = β₁.left)
(p₂ : α₂.right = β₂.left)
{X' : V}
(f' : homology f₃ g₃ w₃ ⟶ X') :
homology.map w₁ w₂ α₁ β₁ p₁ ≫ homology.map w₂ w₃ α₂ β₂ p₂ ≫ f' = homology.map w₁ w₃ (α₁ ≫ α₂) (β₁ ≫ β₂) _ ≫ f'
theorem
homology.map_comp
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A₁ B₁ C₁ : V}
{f₁ : A₁ ⟶ B₁}
[category_theory.limits.has_image f₁]
{g₁ : B₁ ⟶ C₁}
[category_theory.limits.has_kernel g₁]
(w₁ : f₁ ≫ g₁ = 0)
{A₂ B₂ C₂ : V}
{f₂ : A₂ ⟶ B₂}
[category_theory.limits.has_image f₂]
{g₂ : B₂ ⟶ C₂}
[category_theory.limits.has_kernel g₂]
(w₂ : f₂ ≫ g₂ = 0)
{A₃ B₃ C₃ : V}
{f₃ : A₃ ⟶ B₃}
[category_theory.limits.has_image f₃]
{g₃ : B₃ ⟶ C₃}
[category_theory.limits.has_kernel g₃]
(w₃ : f₃ ≫ g₃ = 0)
(α₁ : category_theory.arrow.mk f₁ ⟶ category_theory.arrow.mk f₂)
[category_theory.limits.has_image_map α₁]
(β₁ : category_theory.arrow.mk g₁ ⟶ category_theory.arrow.mk g₂)
(α₂ : category_theory.arrow.mk f₂ ⟶ category_theory.arrow.mk f₃)
[category_theory.limits.has_image_map α₂]
(β₂ : category_theory.arrow.mk g₂ ⟶ category_theory.arrow.mk g₃)
[category_theory.limits.has_cokernel (image_to_kernel f₁ g₁ w₁)]
[category_theory.limits.has_cokernel (image_to_kernel f₂ g₂ w₂)]
[category_theory.limits.has_cokernel (image_to_kernel f₃ g₃ w₃)]
(p₁ : α₁.right = β₁.left)
(p₂ : α₂.right = β₂.left) :
homology.map w₁ w₂ α₁ β₁ p₁ ≫ homology.map w₂ w₃ α₂ β₂ p₂ = homology.map w₁ w₃ (α₁ ≫ α₂) (β₁ ≫ β₂) _
noncomputable
def
homology.map_iso
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A₁ B₁ C₁ : V}
{f₁ : A₁ ⟶ B₁}
[category_theory.limits.has_image f₁]
{g₁ : B₁ ⟶ C₁}
[category_theory.limits.has_kernel g₁]
(w₁ : f₁ ≫ g₁ = 0)
{A₂ B₂ C₂ : V}
{f₂ : A₂ ⟶ B₂}
[category_theory.limits.has_image f₂]
{g₂ : B₂ ⟶ C₂}
[category_theory.limits.has_kernel g₂]
(w₂ : f₂ ≫ g₂ = 0)
[category_theory.limits.has_cokernel (image_to_kernel f₁ g₁ w₁)]
[category_theory.limits.has_cokernel (image_to_kernel f₂ g₂ w₂)]
(α : 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) :
An isomorphism between two three-term complexes induces an isomorphism on homology.
Equations
- homology.map_iso w₁ w₂ α β p = {hom := homology.map w₁ w₂ α.hom β.hom p, inv := homology.map w₂ w₁ α.inv β.inv _, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
homology.congr_hom
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
{g : B ⟶ C}
(w : f ≫ g = 0)
{f' : A ⟶ B}
{g' : B ⟶ C}
(w' : f' ≫ g' = 0)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
(pf : f = f')
(pg : g = g') :
(homology.congr w w' pf pg).hom = homology.map w w' {left := 𝟙 (category_theory.arrow.mk f).left, right := 𝟙 (category_theory.arrow.mk f).right, w' := _} {left := 𝟙 (category_theory.arrow.mk g).left, right := 𝟙 (category_theory.arrow.mk g).right, w' := _} _
@[simp]
theorem
homology.congr_inv
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
{g : B ⟶ C}
(w : f ≫ g = 0)
{f' : A ⟶ B}
{g' : B ⟶ C}
(w' : f' ≫ g' = 0)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
(pf : f = f')
(pg : g = g') :
(homology.congr w w' pf pg).inv = homology.map w' w {left := 𝟙 (category_theory.arrow.mk f').left, right := 𝟙 (category_theory.arrow.mk f').right, w' := _} {left := 𝟙 (category_theory.arrow.mk g').left, right := 𝟙 (category_theory.arrow.mk g').right, w' := _} _
noncomputable
def
homology.congr
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
{f : A ⟶ B}
{g : B ⟶ C}
(w : f ≫ g = 0)
{f' : A ⟶ B}
{g' : B ⟶ C}
(w' : f' ≫ g' = 0)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_images V]
[category_theory.limits.has_image_maps V]
(pf : f = f')
(pg : g = g') :
homology f g w ≅ homology f' g' w' if f = f' and g = g'.
(Note the objects are not changing here.)
Equations
- homology.congr w w' pf pg = {hom := homology.map w w' {left := 𝟙 (category_theory.arrow.mk f).left, right := 𝟙 (category_theory.arrow.mk f).right, w' := _} {left := 𝟙 (category_theory.arrow.mk g).left, right := 𝟙 (category_theory.arrow.mk g).right, w' := _} _, inv := homology.map w' w {left := 𝟙 (category_theory.arrow.mk f').left, right := 𝟙 (category_theory.arrow.mk f').right, w' := _} {left := 𝟙 (category_theory.arrow.mk g').left, right := 𝟙 (category_theory.arrow.mk g').right, w' := _} _, hom_inv_id' := _, inv_hom_id' := _}
We provide a variant image_to_kernel' : image f ⟶ kernel g,
and use this to give alternative formulas for homology f g w.
noncomputable
def
image_to_kernel'
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
(w : f ≫ g = 0) :
While image_to_kernel f g w provides a morphism
image_subobject f ⟶ kernel_subobject g
in terms of the subobject API,
this variant provides a morphism
image f ⟶ kernel g,
which is sometimes more convenient.
Equations
@[simp]
theorem
image_subobject_iso_image_to_kernel'
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
(w : f ≫ g = 0) :
@[simp]
theorem
image_to_kernel'_kernel_subobject_iso
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
(w : f ≫ g = 0) :
noncomputable
def
homology_iso_cokernel_image_to_kernel'
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
[category_theory.limits.has_cokernels V]
(w : f ≫ g = 0) :
homology f g w ≅ category_theory.limits.cokernel (image_to_kernel' f g w)
homology f g w can be computed as the cokernel of image_to_kernel' f g w.
Equations
- homology_iso_cokernel_image_to_kernel' f g w = {hom := category_theory.limits.cokernel.map (image_to_kernel f g w) (image_to_kernel' f g w) (category_theory.limits.image_subobject_iso f).hom (category_theory.limits.kernel_subobject_iso g).hom _, inv := category_theory.limits.cokernel.map (image_to_kernel' f g w) (image_to_kernel f g w) (category_theory.limits.image_subobject_iso f).inv (category_theory.limits.kernel_subobject_iso g).inv _, hom_inv_id' := _, inv_hom_id' := _}
noncomputable
def
homology_iso_cokernel_lift
{V : Type u}
[category_theory.category V]
[category_theory.limits.has_zero_morphisms V]
{A B C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[category_theory.limits.has_kernels V]
[category_theory.limits.has_images V]
[category_theory.limits.has_cokernels V]
[category_theory.limits.has_equalizers V]
(w : f ≫ g = 0) :
homology f g w can be computed as the cokernel of kernel.lift g f w.