Preservation and reflection of monomorphisms and epimorphisms #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We provide typeclasses that state that a functor preserves or reflects monomorphisms or epimorphisms.
@[class]
structure
category_theory.functor.preserves_monomorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Prop
- preserves : ∀ {X Y : C} (f : X ⟶ Y) [_inst_4 : category_theory.mono f], category_theory.mono (F.map f)
A functor preserves monomorphisms if it maps monomorphisms to monomorphisms.
@[protected, instance]
def
category_theory.functor.map_mono
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.preserves_monomorphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.mono f] :
category_theory.mono (F.map f)
@[class]
structure
category_theory.functor.preserves_epimorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Prop
- preserves : ∀ {X Y : C} (f : X ⟶ Y) [_inst_4 : category_theory.epi f], category_theory.epi (F.map f)
A functor preserves epimorphisms if it maps epimorphisms to epimorphisms.
@[protected, instance]
def
category_theory.functor.map_epi
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.preserves_epimorphisms]
{X Y : C}
(f : X ⟶ Y)
[category_theory.epi f] :
category_theory.epi (F.map f)
@[class]
structure
category_theory.functor.reflects_monomorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Prop
- reflects : ∀ {X Y : C} (f : X ⟶ Y), category_theory.mono (F.map f) → category_theory.mono f
A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves monomorphisms.
theorem
category_theory.functor.mono_of_mono_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.reflects_monomorphisms]
{X Y : C}
{f : X ⟶ Y}
(h : category_theory.mono (F.map f)) :
@[class]
structure
category_theory.functor.reflects_epimorphisms
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Prop
- reflects : ∀ {X Y : C} (f : X ⟶ Y), category_theory.epi (F.map f) → category_theory.epi f
A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves epimorphisms.
theorem
category_theory.functor.epi_of_epi_map
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[F.reflects_epimorphisms]
{X Y : C}
{f : X ⟶ Y}
(h : category_theory.epi (F.map f)) :
@[protected, instance]
def
category_theory.functor.preserves_monomorphisms_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[F.preserves_monomorphisms]
[G.preserves_monomorphisms] :
(F ⋙ G).preserves_monomorphisms
@[protected, instance]
def
category_theory.functor.preserves_epimorphisms_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[F.preserves_epimorphisms]
[G.preserves_epimorphisms] :
(F ⋙ G).preserves_epimorphisms
@[protected, instance]
def
category_theory.functor.reflects_monomorphisms_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[F.reflects_monomorphisms]
[G.reflects_monomorphisms] :
(F ⋙ G).reflects_monomorphisms
@[protected, instance]
def
category_theory.functor.reflects_epimorphisms_comp
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[F.reflects_epimorphisms]
[G.reflects_epimorphisms] :
(F ⋙ G).reflects_epimorphisms
theorem
category_theory.functor.preserves_epimorphisms_of_preserves_of_reflects
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[(F ⋙ G).preserves_epimorphisms]
[G.reflects_epimorphisms] :
theorem
category_theory.functor.preserves_monomorphisms_of_preserves_of_reflects
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[(F ⋙ G).preserves_monomorphisms]
[G.reflects_monomorphisms] :
theorem
category_theory.functor.reflects_epimorphisms_of_preserves_of_reflects
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[G.preserves_epimorphisms]
[(F ⋙ G).reflects_epimorphisms] :
theorem
category_theory.functor.reflects_monomorphisms_of_preserves_of_reflects
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u₃}
[category_theory.category E]
(F : C ⥤ D)
(G : D ⥤ E)
[G.preserves_monomorphisms]
[(F ⋙ G).reflects_monomorphisms] :
theorem
category_theory.functor.preserves_monomorphisms.of_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
[F.preserves_monomorphisms]
(α : F ≅ G) :
theorem
category_theory.functor.preserves_monomorphisms.iso_iff
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G) :
theorem
category_theory.functor.preserves_epimorphisms.of_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
[F.preserves_epimorphisms]
(α : F ≅ G) :
theorem
category_theory.functor.preserves_epimorphisms.iso_iff
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G) :
theorem
category_theory.functor.reflects_monomorphisms.of_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
[F.reflects_monomorphisms]
(α : F ≅ G) :
theorem
category_theory.functor.reflects_monomorphisms.iso_iff
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G) :
theorem
category_theory.functor.reflects_epimorphisms.of_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
[F.reflects_epimorphisms]
(α : F ≅ G) :
theorem
category_theory.functor.reflects_epimorphisms.iso_iff
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F G : C ⥤ D}
(α : F ≅ G) :
theorem
category_theory.functor.preserves_epimorphsisms_of_adjunction
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G) :
@[protected, instance]
def
category_theory.functor.preserves_epimorphisms_of_is_left_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.is_left_adjoint F] :
theorem
category_theory.functor.preserves_monomorphisms_of_adjunction
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
{G : D ⥤ C}
(adj : F ⊣ G) :
@[protected, instance]
def
category_theory.functor.preserves_monomorphisms_of_is_right_adjoint
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.is_right_adjoint F] :
@[protected, instance]
def
category_theory.functor.reflects_monomorphisms_of_faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.faithful F] :
@[protected, instance]
def
category_theory.functor.reflects_epimorphisms_of_faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.faithful F] :
def
category_theory.functor.split_epi_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[category_theory.full F]
[category_theory.faithful F] :
If F is a fully faithful functor, split epimorphisms are preserved and reflected by F.
@[simp]
theorem
category_theory.functor.is_split_epi_iff
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[category_theory.full F]
[category_theory.faithful F] :
def
category_theory.functor.split_mono_equiv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[category_theory.full F]
[category_theory.faithful F] :
If F is a fully faithful functor, split monomorphisms are preserved and reflected by F.
Equations
- F.split_mono_equiv f = {to_fun := λ (f_1 : category_theory.split_mono f), f_1.map F, inv_fun := λ (s : category_theory.split_mono (F.map f)), {retraction := F.preimage s.retraction, id' := _}, left_inv := _, right_inv := _}
@[simp]
theorem
category_theory.functor.is_split_mono_iff
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[category_theory.full F]
[category_theory.faithful F] :
@[simp]
theorem
category_theory.functor.epi_map_iff_epi
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[hF₁ : F.preserves_epimorphisms]
[hF₂ : F.reflects_epimorphisms] :
category_theory.epi (F.map f) ↔ category_theory.epi f
@[simp]
theorem
category_theory.functor.mono_map_iff_mono
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
{X Y : C}
(f : X ⟶ Y)
[hF₁ : F.preserves_monomorphisms]
[hF₂ : F.reflects_monomorphisms] :
category_theory.mono (F.map f) ↔ category_theory.mono f
def
category_theory.functor.split_epi_category_imp_of_is_equivalence
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.is_equivalence F]
[category_theory.split_epi_category C] :
If F : C ⥤ D is an equivalence of categories and C is a split_epi_category,
then D also is.
Equations
theorem
category_theory.adjunction.strong_epi_map_of_strong_epi
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
{F : C ⥤ D}
{F' : D ⥤ C}
{A B : C}
(adj : F ⊣ F')
(f : A ⟶ B)
[h₁ : F'.preserves_monomorphisms]
[h₂ : F.preserves_epimorphisms]
[category_theory.strong_epi f] :
@[protected, instance]
def
category_theory.adjunction.strong_epi_map_of_is_equivalence
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
{F : C ⥤ D}
{A B : C}
[category_theory.is_equivalence F]
(f : A ⟶ B)
[h : category_theory.strong_epi f] :
@[simp]
theorem
category_theory.functor.strong_epi_map_iff_strong_epi_of_is_equivalence
{C : Type u_1}
{D : Type u_2}
[category_theory.category C]
[category_theory.category D]
{F : C ⥤ D}
{A B : C}
(f : A ⟶ B)
[category_theory.is_equivalence F] :