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.

theorem image_le_kernel {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B 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.imageSubobject f ≤ CategoryTheory.Limits.kernelSubobject g

def imageToKernel {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B 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

• imageToKernel f g w = (CategoryTheory.Limits.imageSubobject f).ofLE (CategoryTheory.Limits.kernelSubobject g) ⋯

instance instMonoImageToKernel {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B 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)

@[simp]

theorem subobject_ofLE_as_imageToKernel {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B 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) : (CategoryTheory.Limits.imageSubobject f).ofLE (CategoryTheory.Limits.kernelSubobject g) h = imageToKernel f g w

Prefer imageToKernel.

@[simp]

theorem imageToKernel_arrow {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.Limits.kernelSubobject g).arrow = (CategoryTheory.Limits.imageSubobject f).arrow

@[simp]

theorem imageToKernel_arrow_assoc {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B 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) : CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobject g).arrow h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow h

@[simp]

theorem imageToKernel_arrow_apply {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) {F : V → V → Type uF} {carrier : V → Type w} {instFunLike : (X Y : V) → FunLike (F X Y) (carrier X) (carrier Y)} [inst : CategoryTheory.ConcreteCategory V F] (x : CategoryTheory.ToType (CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.imageSubobject f))) : (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.kernelSubobject g).arrow) ((CategoryTheory.ConcreteCategory.hom (imageToKernel f g w)) x) = (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.imageSubobject f).arrow) x

theorem factorThruImageSubobject_comp_imageToKernel {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImage f] (g : B ⟶ C) [CategoryTheory.Limits.HasKernel g] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImageSubobject f) (imageToKernel f g w) = CategoryTheory.Limits.factorThruKernelSubobject g f w

@[simp]

theorem imageToKernel_zero_left {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B 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 B C : V} (f : A ⟶ B) [CategoryTheory.Limits.HasImages V] {w : CategoryTheory.CategoryStruct.comp f 0 = 0} : imageToKernel f 0 w = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobject f).arrow (CategoryTheory.inv (CategoryTheory.Limits.kernelSubobject 0).arrow)

theorem imageToKernel_comp_right {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B 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) : imageToKernel f (CategoryTheory.CategoryStruct.comp g h) ⋯ = CategoryTheory.CategoryStruct.comp (imageToKernel f g w) ((CategoryTheory.Limits.kernelSubobject g).ofLE (CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp g h)) ⋯)

theorem imageToKernel_comp_left {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B 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) : imageToKernel (CategoryTheory.CategoryStruct.comp h f) g ⋯ = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f)).ofLE (CategoryTheory.Limits.imageSubobject f) ⋯) (imageToKernel f g w)

@[simp]

theorem imageToKernel_comp_mono {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B 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) : imageToKernel f (CategoryTheory.CategoryStruct.comp g h) w = CategoryTheory.CategoryStruct.comp (imageToKernel f g ⋯) ((CategoryTheory.Limits.kernelSubobject (CategoryTheory.CategoryStruct.comp g h)).isoOfEq (CategoryTheory.Limits.kernelSubobject g) ⋯).inv

@[simp]

theorem imageToKernel_epi_comp {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B 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) : imageToKernel (CategoryTheory.CategoryStruct.comp h f) g w = CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.imageSubobject (CategoryTheory.CategoryStruct.comp h f)).ofLE (CategoryTheory.Limits.imageSubobject f) ⋯) (imageToKernel f g ⋯)

@[simp]

theorem imageToKernel_comp_hom_inv_comp {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B 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 B 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).

instance imageToKernel_epi_of_epi_of_zero {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B 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).

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 B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.Limits.image f ⟶ CategoryTheory.Limits.kernel g

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

• imageToKernel' f g w = CategoryTheory.Limits.kernel.lift g (CategoryTheory.Limits.image.ι f) ⋯

@[simp]

theorem imageSubobjectIso_imageToKernel' {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).hom (imageToKernel' f g w) = CategoryTheory.CategoryStruct.comp (imageToKernel f g w) (CategoryTheory.Limits.kernelSubobjectIso g).hom

@[simp]

theorem imageToKernel'_kernelSubobjectIso {V : Type u} [CategoryTheory.Category.{v, u} V] [CategoryTheory.Limits.HasZeroMorphisms V] {A B C : V} (f : A ⟶ B) (g : B ⟶ C) [CategoryTheory.Limits.HasKernels V] [CategoryTheory.Limits.HasImages V] (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (imageToKernel' f g w) (CategoryTheory.Limits.kernelSubobjectIso g).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.imageSubobjectIso f).inv (imageToKernel f g w)