Preserving images

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

noncomputable 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 limit spans and colimit cospans, then it preserves images.

Equations

• One or more equations did not get rendered due to their size.

@[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 { I := L.obj (Limits.image f), m := L.map (Limits.image.ι f), m_mono := ⋯, e := L.map (Limits.factorThruImage f), fac := ⋯ }

@[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 = { I := L.obj (Limits.image f), m := L.map (Limits.image.ι f), m_mono := ⋯, e := L.map (Limits.factorThruImage f), fac := ⋯, e_strong_epi := ⋯ }.toMonoIsImage.lift (Limits.Image.monoFactorisation (L.map f))

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)

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

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)

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

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)

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