Preserving images #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
In this file, we show that if a functor preserves span and cospan, then it preserves images.
@[simp]
theorem
category_theory.preserves_image.iso_hom
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.limits.has_equalizers A]
[category_theory.limits.has_images A]
[category_theory.strong_epi_category B]
[category_theory.limits.has_images B]
(L : A ⥤ B)
[Π {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), category_theory.limits.preserves_limit (category_theory.limits.cospan f g) L]
[Π {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), category_theory.limits.preserves_colimit (category_theory.limits.span f g) L]
{X Y : A}
(f : X ⟶ Y) :
(category_theory.preserves_image.iso L f).hom = category_theory.limits.image.lift {I := L.obj (category_theory.limits.image f), m := L.map (category_theory.limits.image.ι f), m_mono := _, e := L.map (category_theory.limits.factor_thru_image f), fac' := _}
@[simp]
theorem
category_theory.preserves_image.iso_inv
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.limits.has_equalizers A]
[category_theory.limits.has_images A]
[category_theory.strong_epi_category B]
[category_theory.limits.has_images B]
(L : A ⥤ B)
[Π {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), category_theory.limits.preserves_limit (category_theory.limits.cospan f g) L]
[Π {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), category_theory.limits.preserves_colimit (category_theory.limits.span f g) L]
{X Y : A}
(f : X ⟶ Y) :
(category_theory.preserves_image.iso L f).inv = (category_theory.limits.strong_epi_mono_factorisation.mk {I := L.obj (category_theory.limits.image f), m := L.map (category_theory.limits.image.ι f), m_mono := _, e := L.map (category_theory.limits.factor_thru_image f), fac' := _}).to_mono_is_image.lift (category_theory.limits.image.mono_factorisation (L.map f))
noncomputable
def
category_theory.preserves_image.iso
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.limits.has_equalizers A]
[category_theory.limits.has_images A]
[category_theory.strong_epi_category B]
[category_theory.limits.has_images B]
(L : A ⥤ B)
[Π {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), category_theory.limits.preserves_limit (category_theory.limits.cospan f g) L]
[Π {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), category_theory.limits.preserves_colimit (category_theory.limits.span f g) L]
{X Y : A}
(f : X ⟶ Y) :
category_theory.limits.image (L.map f) ≅ L.obj (category_theory.limits.image f)
If a functor preserves span and cospan, then it preserves images.
Equations
- category_theory.preserves_image.iso L f = let aux1 : category_theory.limits.strong_epi_mono_factorisation (L.map f) := category_theory.limits.strong_epi_mono_factorisation.mk {I := L.obj (category_theory.limits.image f), m := L.map (category_theory.limits.image.ι f), m_mono := _, e := L.map (category_theory.limits.factor_thru_image f), fac' := _} in (category_theory.limits.image.is_image (L.map f)).iso_ext aux1.to_mono_is_image
theorem
category_theory.preserves_image.factor_thru_image_comp_hom_assoc
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.limits.has_equalizers A]
[category_theory.limits.has_images A]
[category_theory.strong_epi_category B]
[category_theory.limits.has_images B]
(L : A ⥤ B)
[Π {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), category_theory.limits.preserves_limit (category_theory.limits.cospan f g) L]
[Π {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), category_theory.limits.preserves_colimit (category_theory.limits.span f g) L]
{X Y : A}
(f : X ⟶ Y)
{X' : B}
(f' : L.obj (category_theory.limits.image f) ⟶ X') :
category_theory.limits.factor_thru_image (L.map f) ≫ (category_theory.preserves_image.iso L f).hom ≫ f' = L.map (category_theory.limits.factor_thru_image f) ≫ f'
theorem
category_theory.preserves_image.factor_thru_image_comp_hom
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.limits.has_equalizers A]
[category_theory.limits.has_images A]
[category_theory.strong_epi_category B]
[category_theory.limits.has_images B]
(L : A ⥤ B)
[Π {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), category_theory.limits.preserves_limit (category_theory.limits.cospan f g) L]
[Π {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), category_theory.limits.preserves_colimit (category_theory.limits.span f g) L]
{X Y : A}
(f : X ⟶ Y) :
theorem
category_theory.preserves_image.hom_comp_map_image_ι
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.limits.has_equalizers A]
[category_theory.limits.has_images A]
[category_theory.strong_epi_category B]
[category_theory.limits.has_images B]
(L : A ⥤ B)
[Π {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), category_theory.limits.preserves_limit (category_theory.limits.cospan f g) L]
[Π {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), category_theory.limits.preserves_colimit (category_theory.limits.span f g) L]
{X Y : A}
(f : X ⟶ Y) :
theorem
category_theory.preserves_image.hom_comp_map_image_ι_assoc
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.limits.has_equalizers A]
[category_theory.limits.has_images A]
[category_theory.strong_epi_category B]
[category_theory.limits.has_images B]
(L : A ⥤ B)
[Π {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), category_theory.limits.preserves_limit (category_theory.limits.cospan f g) L]
[Π {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), category_theory.limits.preserves_colimit (category_theory.limits.span f g) L]
{X Y : A}
(f : X ⟶ Y)
{X' : B}
(f' : L.obj Y ⟶ X') :
(category_theory.preserves_image.iso L f).hom ≫ L.map (category_theory.limits.image.ι f) ≫ f' = category_theory.limits.image.ι (L.map f) ≫ f'
theorem
category_theory.preserves_image.inv_comp_image_ι_map_assoc
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.limits.has_equalizers A]
[category_theory.limits.has_images A]
[category_theory.strong_epi_category B]
[category_theory.limits.has_images B]
(L : A ⥤ B)
[Π {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), category_theory.limits.preserves_limit (category_theory.limits.cospan f g) L]
[Π {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), category_theory.limits.preserves_colimit (category_theory.limits.span f g) L]
{X Y : A}
(f : X ⟶ Y)
{X' : B}
(f' : L.obj Y ⟶ X') :
(category_theory.preserves_image.iso L f).inv ≫ category_theory.limits.image.ι (L.map f) ≫ f' = L.map (category_theory.limits.image.ι f) ≫ f'
theorem
category_theory.preserves_image.inv_comp_image_ι_map
{A : Type u₁}
{B : Type u₂}
[category_theory.category A]
[category_theory.category B]
[category_theory.limits.has_equalizers A]
[category_theory.limits.has_images A]
[category_theory.strong_epi_category B]
[category_theory.limits.has_images B]
(L : A ⥤ B)
[Π {X Y Z : A} (f : X ⟶ Z) (g : Y ⟶ Z), category_theory.limits.preserves_limit (category_theory.limits.cospan f g) L]
[Π {X Y Z : A} (f : X ⟶ Y) (g : X ⟶ Z), category_theory.limits.preserves_colimit (category_theory.limits.span f g) L]
{X Y : A}
(f : X ⟶ Y) :