Image-to-kernel comparison maps #
Whenever f : A ⟶ B and g : B ⟶ C satisfy w : f ≫ g = 0,
we have image_le_kernel f g w : imageSubobject f ≤ kernelSubobject g
(assuming the appropriate images and kernels exist).
imageToKernel 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 imageToKernel f g w.
Note: As part of the transition to the new homology API, homology is temporarily
renamed homology'. It is planned that this definition shall be removed and replaced by
ShortComplex.homology.
theorem
image_le_kernel
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
:
def
imageToKernel
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
:
CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f) ⟶ CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g)
The canonical morphism imageSubobject f ⟶ kernelSubobject g when f ≫ g = 0.
Equations
Instances For
instance
instMonoObjSubobjectToQuiverToCategoryStructSmallCategoryToPreorderInstPartialOrderSubobjectToQuiverToCategoryStructToPrefunctorUnderlyingImageSubobjectKernelSubobjectImageToKernel
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
:
CategoryTheory.Mono (imageToKernel f g w)
Equations
- ⋯ = ⋯
@[simp]
theorem
subobject_ofLE_as_imageToKernel
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
(h : CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g)
:
Prefer imageToKernel.
@[simp]
theorem
imageToKernel_arrow_assoc
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{Z : V}
(h : B ⟶ Z)
:
@[simp]
theorem
imageToKernel_arrow
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
:
@[simp]
theorem
imageToKernel_arrow_apply
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
[CategoryTheory.ConcreteCategory V]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
(x : (CategoryTheory.forget V).obj (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f)))
:
theorem
factorThruImageSubobject_comp_imageToKernel
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
:
@[simp]
theorem
imageToKernel_zero_left
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasZeroObject V]
{w : CategoryTheory.CategoryStruct.comp 0 g = 0}
:
imageToKernel 0 g w = 0
theorem
imageToKernel_zero_right
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImages V]
{w : CategoryTheory.CategoryStruct.comp f 0 = 0}
:
theorem
imageToKernel_comp_right
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasImages V]
{D : V}
(h : C ⟶ D)
(w : CategoryTheory.CategoryStruct.comp f g = 0)
:
theorem
imageToKernel_comp_left
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasImages V]
{Z : V}
(h : Z ⟶ A)
(w : CategoryTheory.CategoryStruct.comp f g = 0)
:
@[simp]
theorem
imageToKernel_comp_mono
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasImages V]
{D : V}
(h : C ⟶ D)
[CategoryTheory.Mono h]
(w : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = 0)
:
@[simp]
theorem
imageToKernel_epi_comp
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasImages V]
{Z : V}
(h : Z ⟶ A)
[CategoryTheory.Epi h]
(w : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp h f) g = 0)
:
@[simp]
theorem
imageToKernel_comp_hom_inv_comp
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasEqualizers V]
[CategoryTheory.Limits.HasImages V]
{Z : V}
{i : B ≅ Z}
(w : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f i.hom)
(CategoryTheory.CategoryStruct.comp i.inv g) = 0)
:
imageToKernel (CategoryTheory.CategoryStruct.comp f i.hom) (CategoryTheory.CategoryStruct.comp i.inv g) w = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectCompIso f i.hom).hom
(CategoryTheory.CategoryStruct.comp (imageToKernel f g ⋯)
(CategoryTheory.Limits.kernelSubobjectIsoComp i.inv g).inv)
instance
imageToKernel_epi_of_zero_of_mono
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasZeroObject V]
[CategoryTheory.Mono g]
:
CategoryTheory.Epi (imageToKernel 0 g ⋯)
imageToKernel for A --0--> B --g--> C, where g is a mono is itself an epi
(i.e. the sequence is exact at B).
Equations
- ⋯ = ⋯
instance
imageToKernel_epi_of_epi_of_zero
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Epi f]
:
CategoryTheory.Epi (imageToKernel f 0 ⋯)
imageToKernel for A --f--> B --0--> C, where g is an epi is itself an epi
(i.e. the sequence is exact at B).
Equations
- ⋯ = ⋯
def
homology'
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
[CategoryTheory.Limits.HasCokernel (imageToKernel 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 imageToKernel morphism for f and g.
Equations
- homology' f g w = CategoryTheory.Limits.cokernel (imageToKernel f g w)
Instances For
def
homology'.π
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
:
CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g) ⟶ homology' f g w
The morphism from cycles to homology.
Equations
- homology'.π f g w = CategoryTheory.Limits.cokernel.π (imageToKernel f g w)
Instances For
@[simp]
theorem
homology'.condition
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
:
CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (homology'.π f g w) = 0
def
homology'.desc
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
{D : V}
(k : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g) ⟶ D)
(p : CategoryTheory.CategoryStruct.comp (imageToKernel 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 = CategoryTheory.Limits.cokernel.desc (imageToKernel f g w) k p
Instances For
@[simp]
theorem
homology'.π_desc_assoc
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
{D : V}
(k : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g) ⟶ D)
(p : CategoryTheory.CategoryStruct.comp (imageToKernel f g w) k = 0)
{Z : V}
(h : D ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (homology'.π f g w)
(CategoryTheory.CategoryStruct.comp (homology'.desc f g w k p) h) = CategoryTheory.CategoryStruct.comp k h
@[simp]
theorem
homology'.π_desc
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
{D : V}
(k : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g) ⟶ D)
(p : CategoryTheory.CategoryStruct.comp (imageToKernel f g w) k = 0)
:
CategoryTheory.CategoryStruct.comp (homology'.π f g w) (homology'.desc f g w k p) = k
theorem
homology'.ext
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
{D : V}
{k : homology' f g w ⟶ D}
{k' : homology' f g w ⟶ D}
(p : CategoryTheory.CategoryStruct.comp (homology'.π f g w) k = CategoryTheory.CategoryStruct.comp (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.
def
homology'OfZeroRight
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
[CategoryTheory.Limits.HasImage f]
[CategoryTheory.Limits.HasCokernel (imageToKernel f 0 ⋯)]
[CategoryTheory.Limits.HasCokernel f]
[CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.image.ι f)]
[CategoryTheory.Epi (CategoryTheory.Limits.factorThruImage f)]
:
homology' f 0 ⋯ ≅ CategoryTheory.Limits.cokernel f
The cokernel of the map Im f ⟶ Ker 0 is isomorphic to the cokernel of f.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
homology'OfZeroLeft
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernel g]
[CategoryTheory.Limits.HasZeroObject V]
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasImage 0]
[CategoryTheory.Limits.HasCokernel (imageToKernel 0 g ⋯)]
:
homology' 0 g ⋯ ≅ CategoryTheory.Limits.kernel g
The kernel of the map Im 0 ⟶ Ker f is isomorphic to the kernel of f.
Equations
- homology'OfZeroLeft g = (CategoryTheory.Limits.cokernelIsoOfEq ⋯ ≪≫ CategoryTheory.Limits.cokernelZeroIsoTarget) ≪≫ CategoryTheory.Limits.kernelSubobjectIso g
Instances For
@[simp]
theorem
homology'ZeroZero_hom
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
[CategoryTheory.Limits.HasZeroObject V]
[CategoryTheory.Limits.HasImage 0]
[CategoryTheory.Limits.HasCokernel (imageToKernel 0 0 ⋯)]
:
homology'ZeroZero.hom = homology'.desc 0 0 ⋯ (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject 0)) ⋯
@[simp]
theorem
homology'ZeroZero_inv
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
[CategoryTheory.Limits.HasZeroObject V]
[CategoryTheory.Limits.HasImage 0]
[CategoryTheory.Limits.HasCokernel (imageToKernel 0 0 ⋯)]
:
homology'ZeroZero.inv = CategoryTheory.CategoryStruct.comp
(CategoryTheory.inv (CategoryTheory.Subobject.arrow (CategoryTheory.Limits.kernelSubobject 0))) (homology'.π 0 0 ⋯)
def
homology'ZeroZero
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
[CategoryTheory.Limits.HasZeroObject V]
[CategoryTheory.Limits.HasImage 0]
[CategoryTheory.Limits.HasCokernel (imageToKernel 0 0 ⋯)]
:
homology 0 0 _ is just the middle object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
imageSubobjectMap_comp_imageToKernel_assoc
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
[CategoryTheory.Limits.HasImage f]
{g : B ⟶ C}
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{A' : V}
{B' : V}
{C' : V}
{f' : A' ⟶ B'}
[CategoryTheory.Limits.HasImage f']
{g' : B' ⟶ C'}
[CategoryTheory.Limits.HasKernel g']
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
(α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
[CategoryTheory.Limits.HasImageMap α]
(β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g')
(p : α.right = β.left)
{Z : V}
(h : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g') ⟶ Z)
:
theorem
imageSubobjectMap_comp_imageToKernel
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
[CategoryTheory.Limits.HasImage f]
{g : B ⟶ C}
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{A' : V}
{B' : V}
{C' : V}
{f' : A' ⟶ B'}
[CategoryTheory.Limits.HasImage f']
{g' : B' ⟶ C'}
[CategoryTheory.Limits.HasKernel g']
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
(α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
[CategoryTheory.Limits.HasImageMap α]
(β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.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 imageToKernel morphisms intertwine the induced map on kernels and the induced map on images.
def
homology'.map
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
[CategoryTheory.Limits.HasImage f]
{g : B ⟶ C}
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{A' : V}
{B' : V}
{C' : V}
{f' : A' ⟶ B'}
[CategoryTheory.Limits.HasImage f']
{g' : B' ⟶ C'}
[CategoryTheory.Limits.HasKernel g']
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
(α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
[CategoryTheory.Limits.HasImageMap α]
(β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g')
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
[CategoryTheory.Limits.HasCokernel (imageToKernel 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
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
homology'.π_map_assoc
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
[CategoryTheory.Limits.HasImage f]
{g : B ⟶ C}
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{A' : V}
{B' : V}
{C' : V}
{f' : A' ⟶ B'}
[CategoryTheory.Limits.HasImage f']
{g' : B' ⟶ C'}
[CategoryTheory.Limits.HasKernel g']
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
(α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
[CategoryTheory.Limits.HasImageMap α]
(β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g')
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
[CategoryTheory.Limits.HasCokernel (imageToKernel f' g' w')]
(p : α.right = β.left)
{Z : V}
(h : homology' f' g' w' ⟶ Z)
:
@[simp]
theorem
homology'.π_map
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
[CategoryTheory.Limits.HasImage f]
{g : B ⟶ C}
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{A' : V}
{B' : V}
{C' : V}
{f' : A' ⟶ B'}
[CategoryTheory.Limits.HasImage f']
{g' : B' ⟶ C'}
[CategoryTheory.Limits.HasKernel g']
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
(α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
[CategoryTheory.Limits.HasImageMap α]
(β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g')
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
[CategoryTheory.Limits.HasCokernel (imageToKernel f' g' w')]
(p : α.right = β.left)
:
CategoryTheory.CategoryStruct.comp (homology'.π f g w) (homology'.map w w' α β p) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap β) (homology'.π f' g' w')
@[simp]
theorem
homology'.π_map_apply
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
[CategoryTheory.Limits.HasImage f]
{g : B ⟶ C}
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{A' : V}
{B' : V}
{C' : V}
{f' : A' ⟶ B'}
[CategoryTheory.Limits.HasImage f']
{g' : B' ⟶ C'}
[CategoryTheory.Limits.HasKernel g']
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
(α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
[CategoryTheory.Limits.HasImageMap α]
(β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g')
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
[CategoryTheory.Limits.HasCokernel (imageToKernel f' g' w')]
[CategoryTheory.ConcreteCategory V]
(p : α.right = β.left)
(x : (CategoryTheory.forget V).obj (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g)))
:
(homology'.map w w' α β p) ((homology'.π f g w) x) = (homology'.π f' g' w') ((CategoryTheory.Limits.kernelSubobjectMap β) x)
@[simp]
theorem
homology'.map_desc_assoc
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
[CategoryTheory.Limits.HasImage f]
{g : B ⟶ C}
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{A' : V}
{B' : V}
{C' : V}
{f' : A' ⟶ B'}
[CategoryTheory.Limits.HasImage f']
{g' : B' ⟶ C'}
[CategoryTheory.Limits.HasKernel g']
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
(α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
[CategoryTheory.Limits.HasImageMap α]
(β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g')
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
[CategoryTheory.Limits.HasCokernel (imageToKernel f' g' w')]
(p : α.right = β.left)
{D : V}
(k : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g') ⟶ D)
(z : CategoryTheory.CategoryStruct.comp (imageToKernel f' g' w') k = 0)
{Z : V}
(h : D ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (homology'.map w w' α β p)
(CategoryTheory.CategoryStruct.comp (homology'.desc f' g' w' k z) h) = CategoryTheory.CategoryStruct.comp
(homology'.desc f g w (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap β) k) ⋯) h
@[simp]
theorem
homology'.map_desc_apply
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
[CategoryTheory.Limits.HasImage f]
{g : B ⟶ C}
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{A' : V}
{B' : V}
{C' : V}
{f' : A' ⟶ B'}
[CategoryTheory.Limits.HasImage f']
{g' : B' ⟶ C'}
[CategoryTheory.Limits.HasKernel g']
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
(α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
[CategoryTheory.Limits.HasImageMap α]
(β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g')
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
[CategoryTheory.Limits.HasCokernel (imageToKernel f' g' w')]
(p : α.right = β.left)
{D : V}
(k : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g') ⟶ D)
(z : CategoryTheory.CategoryStruct.comp (imageToKernel f' g' w') k = 0)
[inst : CategoryTheory.ConcreteCategory V]
(x : (CategoryTheory.forget V).obj (homology' f g w))
:
(homology'.desc f' g' w' k z) ((homology'.map w w' α β p) x) = (homology'.desc f g w (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap β) k) ⋯) x
@[simp]
theorem
homology'.map_desc
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
[CategoryTheory.Limits.HasImage f]
{g : B ⟶ C}
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{A' : V}
{B' : V}
{C' : V}
{f' : A' ⟶ B'}
[CategoryTheory.Limits.HasImage f']
{g' : B' ⟶ C'}
[CategoryTheory.Limits.HasKernel g']
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
(α : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f')
[CategoryTheory.Limits.HasImageMap α]
(β : CategoryTheory.Arrow.mk g ⟶ CategoryTheory.Arrow.mk g')
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
[CategoryTheory.Limits.HasCokernel (imageToKernel f' g' w')]
(p : α.right = β.left)
{D : V}
(k : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject g') ⟶ D)
(z : CategoryTheory.CategoryStruct.comp (imageToKernel f' g' w') k = 0)
:
CategoryTheory.CategoryStruct.comp (homology'.map w w' α β p) (homology'.desc f' g' w' k z) = homology'.desc f g w (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap β) k) ⋯
@[simp]
theorem
homology'.map_id
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
[CategoryTheory.Limits.HasImage f]
{g : B ⟶ C}
[CategoryTheory.Limits.HasKernel g]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
[CategoryTheory.Limits.HasCokernel (imageToKernel f g w)]
:
theorem
homology'.comp_right_eq_comp_left
{V : Type u_2}
[CategoryTheory.Category.{u_3, u_2} V]
{A₁ : V}
{B₁ : V}
{C₁ : V}
{A₂ : V}
{B₂ : V}
{C₂ : V}
{A₃ : V}
{B₃ : V}
{C₃ : V}
{f₁ : A₁ ⟶ B₁}
{g₁ : B₁ ⟶ C₁}
{f₂ : A₂ ⟶ B₂}
{g₂ : B₂ ⟶ C₂}
{f₃ : A₃ ⟶ B₃}
{g₃ : B₃ ⟶ C₃}
{α₁ : CategoryTheory.Arrow.mk f₁ ⟶ CategoryTheory.Arrow.mk f₂}
{β₁ : CategoryTheory.Arrow.mk g₁ ⟶ CategoryTheory.Arrow.mk g₂}
{α₂ : CategoryTheory.Arrow.mk f₂ ⟶ CategoryTheory.Arrow.mk f₃}
{β₂ : CategoryTheory.Arrow.mk g₂ ⟶ CategoryTheory.Arrow.mk g₃}
(p₁ : α₁.right = β₁.left)
(p₂ : α₂.right = β₂.left)
:
(CategoryTheory.CategoryStruct.comp α₁ α₂).right = (CategoryTheory.CategoryStruct.comp β₁ β₂).left
Auxiliary lemma for homology computations.
theorem
homology'.map_comp_assoc
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A₁ : V}
{B₁ : V}
{C₁ : V}
{f₁ : A₁ ⟶ B₁}
[CategoryTheory.Limits.HasImage f₁]
{g₁ : B₁ ⟶ C₁}
[CategoryTheory.Limits.HasKernel g₁]
(w₁ : CategoryTheory.CategoryStruct.comp f₁ g₁ = 0)
{A₂ : V}
{B₂ : V}
{C₂ : V}
{f₂ : A₂ ⟶ B₂}
[CategoryTheory.Limits.HasImage f₂]
{g₂ : B₂ ⟶ C₂}
[CategoryTheory.Limits.HasKernel g₂]
(w₂ : CategoryTheory.CategoryStruct.comp f₂ g₂ = 0)
{A₃ : V}
{B₃ : V}
{C₃ : V}
{f₃ : A₃ ⟶ B₃}
[CategoryTheory.Limits.HasImage f₃]
{g₃ : B₃ ⟶ C₃}
[CategoryTheory.Limits.HasKernel g₃]
(w₃ : CategoryTheory.CategoryStruct.comp f₃ g₃ = 0)
(α₁ : CategoryTheory.Arrow.mk f₁ ⟶ CategoryTheory.Arrow.mk f₂)
[CategoryTheory.Limits.HasImageMap α₁]
(β₁ : CategoryTheory.Arrow.mk g₁ ⟶ CategoryTheory.Arrow.mk g₂)
(α₂ : CategoryTheory.Arrow.mk f₂ ⟶ CategoryTheory.Arrow.mk f₃)
[CategoryTheory.Limits.HasImageMap α₂]
(β₂ : CategoryTheory.Arrow.mk g₂ ⟶ CategoryTheory.Arrow.mk g₃)
[CategoryTheory.Limits.HasCokernel (imageToKernel f₁ g₁ w₁)]
[CategoryTheory.Limits.HasCokernel (imageToKernel f₂ g₂ w₂)]
[CategoryTheory.Limits.HasCokernel (imageToKernel f₃ g₃ w₃)]
(p₁ : α₁.right = β₁.left)
(p₂ : α₂.right = β₂.left)
{Z : V}
(h : homology' f₃ g₃ w₃ ⟶ Z)
:
CategoryTheory.CategoryStruct.comp (homology'.map w₁ w₂ α₁ β₁ p₁)
(CategoryTheory.CategoryStruct.comp (homology'.map w₂ w₃ α₂ β₂ p₂) h) = CategoryTheory.CategoryStruct.comp
(homology'.map w₁ w₃ (CategoryTheory.CategoryStruct.comp α₁ α₂) (CategoryTheory.CategoryStruct.comp β₁ β₂) ⋯) h
theorem
homology'.map_comp
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A₁ : V}
{B₁ : V}
{C₁ : V}
{f₁ : A₁ ⟶ B₁}
[CategoryTheory.Limits.HasImage f₁]
{g₁ : B₁ ⟶ C₁}
[CategoryTheory.Limits.HasKernel g₁]
(w₁ : CategoryTheory.CategoryStruct.comp f₁ g₁ = 0)
{A₂ : V}
{B₂ : V}
{C₂ : V}
{f₂ : A₂ ⟶ B₂}
[CategoryTheory.Limits.HasImage f₂]
{g₂ : B₂ ⟶ C₂}
[CategoryTheory.Limits.HasKernel g₂]
(w₂ : CategoryTheory.CategoryStruct.comp f₂ g₂ = 0)
{A₃ : V}
{B₃ : V}
{C₃ : V}
{f₃ : A₃ ⟶ B₃}
[CategoryTheory.Limits.HasImage f₃]
{g₃ : B₃ ⟶ C₃}
[CategoryTheory.Limits.HasKernel g₃]
(w₃ : CategoryTheory.CategoryStruct.comp f₃ g₃ = 0)
(α₁ : CategoryTheory.Arrow.mk f₁ ⟶ CategoryTheory.Arrow.mk f₂)
[CategoryTheory.Limits.HasImageMap α₁]
(β₁ : CategoryTheory.Arrow.mk g₁ ⟶ CategoryTheory.Arrow.mk g₂)
(α₂ : CategoryTheory.Arrow.mk f₂ ⟶ CategoryTheory.Arrow.mk f₃)
[CategoryTheory.Limits.HasImageMap α₂]
(β₂ : CategoryTheory.Arrow.mk g₂ ⟶ CategoryTheory.Arrow.mk g₃)
[CategoryTheory.Limits.HasCokernel (imageToKernel f₁ g₁ w₁)]
[CategoryTheory.Limits.HasCokernel (imageToKernel f₂ g₂ w₂)]
[CategoryTheory.Limits.HasCokernel (imageToKernel f₃ g₃ w₃)]
(p₁ : α₁.right = β₁.left)
(p₂ : α₂.right = β₂.left)
:
CategoryTheory.CategoryStruct.comp (homology'.map w₁ w₂ α₁ β₁ p₁) (homology'.map w₂ w₃ α₂ β₂ p₂) = homology'.map w₁ w₃ (CategoryTheory.CategoryStruct.comp α₁ α₂) (CategoryTheory.CategoryStruct.comp β₁ β₂) ⋯
def
homology'.mapIso
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A₁ : V}
{B₁ : V}
{C₁ : V}
{f₁ : A₁ ⟶ B₁}
[CategoryTheory.Limits.HasImage f₁]
{g₁ : B₁ ⟶ C₁}
[CategoryTheory.Limits.HasKernel g₁]
(w₁ : CategoryTheory.CategoryStruct.comp f₁ g₁ = 0)
{A₂ : V}
{B₂ : V}
{C₂ : V}
{f₂ : A₂ ⟶ B₂}
[CategoryTheory.Limits.HasImage f₂]
{g₂ : B₂ ⟶ C₂}
[CategoryTheory.Limits.HasKernel g₂]
(w₂ : CategoryTheory.CategoryStruct.comp f₂ g₂ = 0)
[CategoryTheory.Limits.HasCokernel (imageToKernel f₁ g₁ w₁)]
[CategoryTheory.Limits.HasCokernel (imageToKernel f₂ g₂ w₂)]
(α : CategoryTheory.Arrow.mk f₁ ≅ CategoryTheory.Arrow.mk f₂)
(β : CategoryTheory.Arrow.mk g₁ ≅ CategoryTheory.Arrow.mk g₂)
(p : α.hom.right = β.hom.left)
:
An isomorphism between two three-term complexes induces an isomorphism on homology.
Equations
- homology'.mapIso w₁ w₂ α β p = { hom := homology'.map w₁ w₂ α.hom β.hom p, inv := homology'.map w₂ w₁ α.inv β.inv ⋯, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
@[simp]
theorem
homology'.congr_inv
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
{g : B ⟶ C}
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{f' : A ⟶ B}
{g' : B ⟶ C}
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasCokernels V]
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasImageMaps V]
(pf : f = f')
(pg : g = g')
:
(homology'.congr w w' pf pg).inv = homology'.map w' w
{ left := CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk f').left,
right := CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk f').right, w := ⋯ }
{ left := CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk g').left,
right := CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk g').right, w := ⋯ }
⋯
@[simp]
theorem
homology'.congr_hom
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
{g : B ⟶ C}
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{f' : A ⟶ B}
{g' : B ⟶ C}
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasCokernels V]
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasImageMaps V]
(pf : f = f')
(pg : g = g')
:
(homology'.congr w w' pf pg).hom = homology'.map w w'
{ left := CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk f).left,
right := CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk f).right, w := ⋯ }
{ left := CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk g).left,
right := CategoryTheory.CategoryStruct.id (CategoryTheory.Arrow.mk g).right, w := ⋯ }
⋯
def
homology'.congr
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
{f : A ⟶ B}
{g : B ⟶ C}
(w : CategoryTheory.CategoryStruct.comp f g = 0)
{f' : A ⟶ B}
{g' : B ⟶ C}
(w' : CategoryTheory.CategoryStruct.comp f' g' = 0)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasCokernels V]
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasImageMaps 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
- One or more equations did not get rendered due to their size.
Instances For
We provide a variant imageToKernel' : image f ⟶ kernel g,
and use this to give alternative formulas for homology f g w.
def
imageToKernel'
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasImages V]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
:
While imageToKernel f g w provides a morphism
imageSubobject f ⟶ kernelSubobject g
in terms of the subobject API,
this variant provides a morphism
image f ⟶ kernel g,
which is sometimes more convenient.
Equations
Instances For
@[simp]
theorem
imageSubobjectIso_imageToKernel'
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasImages V]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
:
@[simp]
theorem
imageToKernel'_kernelSubobjectIso
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasImages V]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
:
def
homology'IsoCokernelImageToKernel'
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasCokernels V]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
:
homology' f g w ≅ CategoryTheory.Limits.cokernel (imageToKernel' f g w)
homology' f g w can be computed as the cokernel of imageToKernel' f g w.
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
homology'IsoCokernelLift
{V : Type u}
[CategoryTheory.Category.{v, u} V]
[CategoryTheory.Limits.HasZeroMorphisms V]
{A : V}
{B : V}
{C : V}
(f : A ⟶ B)
(g : B ⟶ C)
[CategoryTheory.Limits.HasKernels V]
[CategoryTheory.Limits.HasImages V]
[CategoryTheory.Limits.HasCokernels V]
[CategoryTheory.Limits.HasEqualizers V]
(w : CategoryTheory.CategoryStruct.comp f g = 0)
:
homology f g w can be computed as the cokernel of kernel.lift g f w.
Equations
- One or more equations did not get rendered due to their size.