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
@[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 : A} {Y : A} (f : X ⟶ Y) :
(CategoryTheory.PreservesImage.iso L f).inv = CategoryTheory.Limits.IsImage.lift (CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage (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))))) (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 : A} {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
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 : A} {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.

Instances For
    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 : A} {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.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 : A} {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.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 : A} {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.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 : A} {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.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 : A} {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
    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 : A} {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)