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₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) :
CategoryTheory.Limits.image (L.map f) ≅ L.obj (CategoryTheory.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₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) :
    (CategoryTheory.PreservesImage.iso L f).inv = (CategoryTheory.Limits.StrongEpiMonoFactorisation.mk (CategoryTheory.Limits.MonoFactorisation.mk (L.obj (CategoryTheory.Limits.image f)) (L.map (CategoryTheory.Limits.image.ι f)) (L.map (CategoryTheory.Limits.factorThruImage f)) ⋯)).toMonoIsImage.lift (CategoryTheory.Limits.Image.monoFactorisation (L.map f))
    source
    @[simp]
    theorem CategoryTheory.PreservesImage.iso_hom {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) :
    (CategoryTheory.PreservesImage.iso L f).hom = CategoryTheory.Limits.image.lift (CategoryTheory.Limits.MonoFactorisation.mk (L.obj (CategoryTheory.Limits.image f)) (L.map (CategoryTheory.Limits.image.ι f)) (L.map (CategoryTheory.Limits.factorThruImage f)) ⋯)
    source
    theorem CategoryTheory.PreservesImage.factorThruImage_comp_hom {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (L.map f)) (CategoryTheory.PreservesImage.iso L f).hom = L.map (CategoryTheory.Limits.factorThruImage f)
    source
    theorem CategoryTheory.PreservesImage.factorThruImage_comp_hom_assoc {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj (CategoryTheory.Limits.image f) ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.factorThruImage (L.map f)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom h) = CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.factorThruImage f)) h
    source
    theorem CategoryTheory.PreservesImage.hom_comp_map_image_ι {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom (L.map (CategoryTheory.Limits.image.ι f)) = CategoryTheory.Limits.image.ι (L.map f)
    source
    theorem CategoryTheory.PreservesImage.hom_comp_map_image_ι_assoc {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj Y ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).hom (CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.image.ι f)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (L.map f)) h
    source
    theorem CategoryTheory.PreservesImage.inv_comp_image_ι_map {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).inv (CategoryTheory.Limits.image.ι (L.map f)) = L.map (CategoryTheory.Limits.image.ι f)
    source
    theorem CategoryTheory.PreservesImage.inv_comp_image_ι_map_assoc {A : Type u₁} {B : Type u₂} [CategoryTheory.Category.{v₁, u₁} A] [CategoryTheory.Category.{v₂, u₂} B] [CategoryTheory.Limits.HasEqualizers A] [CategoryTheory.Limits.HasImages A] [CategoryTheory.StrongEpiCategory B] [CategoryTheory.Limits.HasImages B] (L : CategoryTheory.Functor A B) [∀ {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g) L] [∀ {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span f g) L] {X Y : A} (f : X ⟶ Y) {Z : B} (h : L.obj Y ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.PreservesImage.iso L f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι (L.map f)) h) = CategoryTheory.CategoryStruct.comp (L.map (CategoryTheory.Limits.image.ι f)) h