Documentation

Mathlib.Algebra.Homology.ImageToKernel

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.

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

    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
    • =

    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
    • =

    We provide a variant imageToKernel' : image f ⟶ kernel g, and use this to give alternative formulas for homology f g w.

    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