Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages

Preservation of coimage-image comparisons #

If a functor preserves kernels and cokernels, then it preserves abelian images, abelian coimages and coimage-image comparisons.

source
def CategoryTheory.Abelian.PreservesImage.iso {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
F.obj (Abelian.image f) ≅ Abelian.image (F.map f)

If a functor preserves kernels and cokernels, it preserves abelian images.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Abelian.PreservesImage.iso_hom_ι {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
    CategoryStruct.comp (iso F f).hom (image.ι (F.map f)) = F.map (image.ι f)
    source
    @[simp]
    theorem CategoryTheory.Abelian.PreservesImage.iso_hom_ι_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) {Z : D} (h : F.obj Y ⟶ Z) :
    CategoryStruct.comp (iso F f).hom (CategoryStruct.comp (image.ι (F.map f)) h) = CategoryStruct.comp (F.map (image.ι f)) h
    source
    @[simp]
    theorem CategoryTheory.Abelian.PreservesImage.factorThruImage_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
    CategoryStruct.comp (F.map (Abelian.factorThruImage f)) (iso F f).hom = Abelian.factorThruImage (F.map f)
    source
    @[simp]
    theorem CategoryTheory.Abelian.PreservesImage.factorThruImage_iso_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) {Z : D} (h : Abelian.image (F.map f) ⟶ Z) :
    CategoryStruct.comp (F.map (Abelian.factorThruImage f)) (CategoryStruct.comp (iso F f).hom h) = CategoryStruct.comp (Abelian.factorThruImage (F.map f)) h
    source
    @[simp]
    theorem CategoryTheory.Abelian.PreservesImage.iso_inv_ι {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
    CategoryStruct.comp (iso F f).inv (F.map (image.ι f)) = image.ι (F.map f)
    source
    @[simp]
    theorem CategoryTheory.Abelian.PreservesImage.iso_inv_ι_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) {Z : D} (h : F.obj Y ⟶ Z) :
    CategoryStruct.comp (iso F f).inv (CategoryStruct.comp (F.map (image.ι f)) h) = CategoryStruct.comp (image.ι (F.map f)) h
    source
    @[simp]
    theorem CategoryTheory.Abelian.PreservesImage.factorThruImage_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
    CategoryStruct.comp (Abelian.factorThruImage (F.map f)) (iso F f).inv = F.map (Abelian.factorThruImage f)
    source
    @[simp]
    theorem CategoryTheory.Abelian.PreservesImage.factorThruImage_iso_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) {Z : D} (h : F.obj (Abelian.image f) ⟶ Z) :
    CategoryStruct.comp (Abelian.factorThruImage (F.map f)) (CategoryStruct.comp (iso F f).inv h) = CategoryStruct.comp (F.map (Abelian.factorThruImage f)) h
    source
    def CategoryTheory.Abelian.PreservesCoimage.iso {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
    F.obj (Abelian.coimage f) ≅ Abelian.coimage (F.map f)

    If a functor preserves kernels and cokernels, it preserves abelian coimages.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Abelian.PreservesCoimage.iso_hom_π {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
      CategoryStruct.comp (F.map (coimage.π f)) (iso F f).hom = coimage.π (F.map f)
      source
      @[simp]
      theorem CategoryTheory.Abelian.PreservesCoimage.iso_hom_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) {Z : D} (h : Abelian.coimage (F.map f) ⟶ Z) :
      CategoryStruct.comp (F.map (coimage.π f)) (CategoryStruct.comp (iso F f).hom h) = CategoryStruct.comp (coimage.π (F.map f)) h
      source
      @[simp]
      theorem CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_inv {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
      CategoryStruct.comp (iso F f).inv (F.map (Abelian.factorThruCoimage f)) = Abelian.factorThruCoimage (F.map f)
      source
      @[simp]
      theorem CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) {Z : D} (h : F.obj Y ⟶ Z) :
      CategoryStruct.comp (iso F f).inv (CategoryStruct.comp (F.map (Abelian.factorThruCoimage f)) h) = CategoryStruct.comp (Abelian.factorThruCoimage (F.map f)) h
      source
      @[simp]
      theorem CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_hom {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
      CategoryStruct.comp (iso F f).hom (Abelian.factorThruCoimage (F.map f)) = F.map (Abelian.factorThruCoimage f)
      source
      @[simp]
      theorem CategoryTheory.Abelian.PreservesCoimage.factorThruCoimage_iso_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) {Z : D} (h : F.obj Y ⟶ Z) :
      CategoryStruct.comp (iso F f).hom (CategoryStruct.comp (Abelian.factorThruCoimage (F.map f)) h) = CategoryStruct.comp (F.map (Abelian.factorThruCoimage f)) h
      source
      @[simp]
      theorem CategoryTheory.Abelian.PreservesCoimage.iso_inv_π {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
      CategoryStruct.comp (coimage.π (F.map f)) (iso F f).inv = F.map (coimage.π f)
      source
      @[simp]
      theorem CategoryTheory.Abelian.PreservesCoimage.iso_inv_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) {Z : D} (h : F.obj (Abelian.coimage f) ⟶ Z) :
      CategoryStruct.comp (coimage.π (F.map f)) (CategoryStruct.comp (iso F f).inv h) = CategoryStruct.comp (F.map (coimage.π f)) h
      source
      theorem CategoryTheory.Abelian.PreservesCoimage.hom_coimageImageComparison {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
      CategoryStruct.comp (iso F f).hom (coimageImageComparison (F.map f)) = CategoryStruct.comp (F.map (coimageImageComparison f)) (PreservesImage.iso F f).hom
      source
      def CategoryTheory.Abelian.PreservesCoimageImageComparison.iso {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
      Arrow.mk (F.map (coimageImageComparison f)) ≅ Arrow.mk (coimageImageComparison (F.map f))

      If a functor preserves kernels and cokernels, it perserves coimage-image comparisons.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_inv_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
        (iso F f).inv.left = (PreservesCoimage.iso F f).inv
        source
        @[simp]
        theorem CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_hom_left {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
        (iso F f).hom.left = (PreservesCoimage.iso F f).hom
        source
        @[simp]
        theorem CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_hom_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
        (iso F f).hom.right = (PreservesImage.iso F f).hom
        source
        @[simp]
        theorem CategoryTheory.Abelian.PreservesCoimageImageComparison.iso_inv_right {C : Type u₁} [Category.{v₁, u₁} C] [Limits.HasZeroMorphisms C] [Limits.HasKernels C] [Limits.HasCokernels C] {D : Type u₂} [Category.{v₂, u₂} D] [Limits.HasZeroMorphisms D] [Limits.HasKernels D] [Limits.HasCokernels D] (F : Functor C D) [F.PreservesZeroMorphisms] [Limits.PreservesLimitsOfShape Limits.WalkingParallelPair F] [Limits.PreservesColimitsOfShape Limits.WalkingParallelPair F] {X Y : C} (f : X ⟶ Y) :
        (iso F f).inv.right = (PreservesImage.iso F f).inv