Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.Images

Preserving images #

In this file, we show that if a functor preserves span and cospan, then it preserves images.

source
def CategoryTheory.PreservesImage.iso {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Limits.HasEqualizers A] [Limits.HasImages A] [StrongEpiCategory B] [Limits.HasImages B] (L : Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), Limits.PreservesLimit (Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), Limits.PreservesColimit (Limits.span f g) L] {X Y : A} (f : X ⟶ Y) :
Limits.image (L.map f) ≅ L.obj (Limits.image f)

If a functor preserves span and cospan, then it preserves images.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.PreservesImage.iso_inv {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Limits.HasEqualizers A] [Limits.HasImages A] [StrongEpiCategory B] [Limits.HasImages B] (L : Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), Limits.PreservesLimit (Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), Limits.PreservesColimit (Limits.span f g) L] {X Y : A} (f : X ⟶ Y) :
    (iso L f).inv = (Limits.StrongEpiMonoFactorisation.mk (Limits.MonoFactorisation.mk (L.obj (Limits.image f)) (L.map (Limits.image.ι f)) (L.map (Limits.factorThruImage f)) ⋯)).toMonoIsImage.lift (Limits.Image.monoFactorisation (L.map f))
    source
    @[simp]
    theorem CategoryTheory.PreservesImage.iso_hom {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Limits.HasEqualizers A] [Limits.HasImages A] [StrongEpiCategory B] [Limits.HasImages B] (L : Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), Limits.PreservesLimit (Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), Limits.PreservesColimit (Limits.span f g) L] {X Y : A} (f : X ⟶ Y) :
    (iso L f).hom = Limits.image.lift (Limits.MonoFactorisation.mk (L.obj (Limits.image f)) (L.map (Limits.image.ι f)) (L.map (Limits.factorThruImage f)) ⋯)
    source
    theorem CategoryTheory.PreservesImage.factorThruImage_comp_hom {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Limits.HasEqualizers A] [Limits.HasImages A] [StrongEpiCategory B] [Limits.HasImages B] (L : Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), Limits.PreservesLimit (Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), Limits.PreservesColimit (Limits.span f g) L] {X Y : A} (f : X ⟶ Y) :
    CategoryStruct.comp (Limits.factorThruImage (L.map f)) (iso L f).hom = L.map (Limits.factorThruImage f)
    source
    theorem CategoryTheory.PreservesImage.factorThruImage_comp_hom_assoc {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Limits.HasEqualizers A] [Limits.HasImages A] [StrongEpiCategory B] [Limits.HasImages B] (L : Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), Limits.PreservesLimit (Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), Limits.PreservesColimit (Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj (Limits.image f) ⟶ Z) :
    CategoryStruct.comp (Limits.factorThruImage (L.map f)) (CategoryStruct.comp (iso L f).hom h) = CategoryStruct.comp (L.map (Limits.factorThruImage f)) h
    source
    theorem CategoryTheory.PreservesImage.hom_comp_map_image_ι {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Limits.HasEqualizers A] [Limits.HasImages A] [StrongEpiCategory B] [Limits.HasImages B] (L : Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), Limits.PreservesLimit (Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), Limits.PreservesColimit (Limits.span f g) L] {X Y : A} (f : X ⟶ Y) :
    CategoryStruct.comp (iso L f).hom (L.map (Limits.image.ι f)) = Limits.image.ι (L.map f)
    source
    theorem CategoryTheory.PreservesImage.hom_comp_map_image_ι_assoc {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Limits.HasEqualizers A] [Limits.HasImages A] [StrongEpiCategory B] [Limits.HasImages B] (L : Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), Limits.PreservesLimit (Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), Limits.PreservesColimit (Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj Y ⟶ Z) :
    CategoryStruct.comp (iso L f).hom (CategoryStruct.comp (L.map (Limits.image.ι f)) h) = CategoryStruct.comp (Limits.image.ι (L.map f)) h
    source
    theorem CategoryTheory.PreservesImage.inv_comp_image_ι_map {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Limits.HasEqualizers A] [Limits.HasImages A] [StrongEpiCategory B] [Limits.HasImages B] (L : Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), Limits.PreservesLimit (Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), Limits.PreservesColimit (Limits.span f g) L] {X Y : A} (f : X ⟶ Y) :
    CategoryStruct.comp (iso L f).inv (Limits.image.ι (L.map f)) = L.map (Limits.image.ι f)
    source
    theorem CategoryTheory.PreservesImage.inv_comp_image_ι_map_assoc {A : Type u₁} {B : Type u₂} [Category.{v₁, u₁} A] [Category.{v₂, u₂} B] [Limits.HasEqualizers A] [Limits.HasImages A] [StrongEpiCategory B] [Limits.HasImages B] (L : Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), Limits.PreservesLimit (Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), Limits.PreservesColimit (Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj Y ⟶ Z) :
    CategoryStruct.comp (iso L f).inv (CategoryStruct.comp (Limits.image.ι (L.map f)) h) = CategoryStruct.comp (L.map (Limits.image.ι f)) h