Preservation and reflection of monomorphisms and epimorphisms #
We provide typeclasses that state that a functor preserves or reflects monomorphisms or epimorphisms.
class
CategoryTheory.Functor.PreservesMonomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor preserves monomorphisms if it maps monomorphisms to monomorphisms.
A functor preserves monomorphisms if it maps monomorphisms to monomorphisms.
Instances
instance
CategoryTheory.Functor.map_mono
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.PreservesMonomorphisms]
{X Y : C}
(f : X ⟶ Y)
[Mono f]
:
class
CategoryTheory.Functor.PreservesEpimorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor preserves epimorphisms if it maps epimorphisms to epimorphisms.
A functor preserves epimorphisms if it maps epimorphisms to epimorphisms.
Instances
instance
CategoryTheory.Functor.map_epi
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.PreservesEpimorphisms]
{X Y : C}
(f : X ⟶ Y)
[Epi f]
:
class
CategoryTheory.Functor.ReflectsMonomorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves monomorphisms.
A functor reflects monomorphisms if morphisms that are mapped to monomorphisms are themselves monomorphisms.
Instances
theorem
CategoryTheory.Functor.mono_of_mono_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.ReflectsMonomorphisms]
{X Y : C}
{f : X ⟶ Y}
(h : Mono (F.map f))
:
Mono f
class
CategoryTheory.Functor.ReflectsEpimorphisms
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
:
A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves epimorphisms.
A functor reflects epimorphisms if morphisms that are mapped to epimorphisms are themselves epimorphisms.
Instances
theorem
CategoryTheory.Functor.epi_of_epi_map
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.ReflectsEpimorphisms]
{X Y : C}
{f : X ⟶ Y}
(h : Epi (F.map f))
:
Epi f
instance
CategoryTheory.Functor.preservesMonomorphisms_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.PreservesMonomorphisms]
[G.PreservesMonomorphisms]
:
(F.comp G).PreservesMonomorphisms
instance
CategoryTheory.Functor.preservesEpimorphisms_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.PreservesEpimorphisms]
[G.PreservesEpimorphisms]
:
(F.comp G).PreservesEpimorphisms
instance
CategoryTheory.Functor.reflectsMonomorphisms_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.ReflectsMonomorphisms]
[G.ReflectsMonomorphisms]
:
(F.comp G).ReflectsMonomorphisms
instance
CategoryTheory.Functor.reflectsEpimorphisms_comp
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[F.ReflectsEpimorphisms]
[G.ReflectsEpimorphisms]
:
(F.comp G).ReflectsEpimorphisms
theorem
CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[(F.comp G).PreservesEpimorphisms]
[G.ReflectsEpimorphisms]
:
theorem
CategoryTheory.Functor.preservesMonomorphisms_of_preserves_of_reflects
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[(F.comp G).PreservesMonomorphisms]
[G.ReflectsMonomorphisms]
:
theorem
CategoryTheory.Functor.reflectsEpimorphisms_of_preserves_of_reflects
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[G.PreservesEpimorphisms]
[(F.comp G).ReflectsEpimorphisms]
:
theorem
CategoryTheory.Functor.reflectsMonomorphisms_of_preserves_of_reflects
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{E : Type u₃}
[Category.{v₃, u₃} E]
(F : Functor C D)
(G : Functor D E)
[G.PreservesMonomorphisms]
[(F.comp G).ReflectsMonomorphisms]
:
theorem
CategoryTheory.Functor.preservesMonomorphisms.of_iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
[F.PreservesMonomorphisms]
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.preservesMonomorphisms.iso_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.preservesEpimorphisms.of_iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
[F.PreservesEpimorphisms]
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.preservesEpimorphisms.iso_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.reflectsMonomorphisms.of_iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
[F.ReflectsMonomorphisms]
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.reflectsMonomorphisms.iso_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.reflectsEpimorphisms.of_iso
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
[F.ReflectsEpimorphisms]
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.reflectsEpimorphisms.iso_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F G : Functor C D}
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.preservesEpimorphsisms_of_adjunction
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
:
@[instance 100]
instance
CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.IsLeftAdjoint]
:
theorem
CategoryTheory.Functor.preservesMonomorphisms_of_adjunction
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
{F : Functor C D}
{G : Functor D C}
(adj : F ⊣ G)
:
@[instance 100]
instance
CategoryTheory.Functor.preservesMonomorphisms_of_isRightAdjoint
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.IsRightAdjoint]
:
@[instance 100]
instance
CategoryTheory.Functor.reflectsMonomorphisms_of_faithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Faithful]
:
@[instance 100]
instance
CategoryTheory.Functor.reflectsEpimorphisms_of_faithful
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.Faithful]
:
noncomputable def
CategoryTheory.Functor.splitEpiEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{X Y : C}
(f : X ⟶ Y)
[F.Full]
[F.Faithful]
:
If F is a fully faithful functor, split epimorphisms are preserved and reflected by F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.isSplitEpi_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{X Y : C}
(f : X ⟶ Y)
[F.Full]
[F.Faithful]
:
noncomputable def
CategoryTheory.Functor.splitMonoEquiv
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{X Y : C}
(f : X ⟶ Y)
[F.Full]
[F.Faithful]
:
If F is a fully faithful functor, split monomorphisms are preserved and reflected by F.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
CategoryTheory.Functor.isSplitMono_iff
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{X Y : C}
(f : X ⟶ Y)
[F.Full]
[F.Faithful]
:
@[simp]
theorem
CategoryTheory.Functor.epi_map_iff_epi
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{X Y : C}
(f : X ⟶ Y)
[hF₁ : F.PreservesEpimorphisms]
[hF₂ : F.ReflectsEpimorphisms]
:
@[simp]
theorem
CategoryTheory.Functor.mono_map_iff_mono
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
{X Y : C}
(f : X ⟶ Y)
[hF₁ : F.PreservesMonomorphisms]
[hF₂ : F.ReflectsMonomorphisms]
:
theorem
CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence
{C : Type u₁}
[Category.{v₁, u₁} C]
{D : Type u₂}
[Category.{v₂, u₂} D]
(F : Functor C D)
[F.IsEquivalence]
[SplitEpiCategory C]
:
If F : C ⥤ D is an equivalence of categories and C is a split_epi_category,
then D also is.
theorem
CategoryTheory.Adjunction.strongEpi_map_of_strongEpi
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
{F : Functor C D}
{F' : Functor D C}
{A B : C}
(adj : F ⊣ F')
(f : A ⟶ B)
[F'.PreservesMonomorphisms]
[F.PreservesEpimorphisms]
[StrongEpi f]
:
instance
CategoryTheory.Adjunction.strongEpi_map_of_isEquivalence
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
{F : Functor C D}
{A B : C}
[F.IsEquivalence]
(f : A ⟶ B)
[_h : StrongEpi f]
:
instance
CategoryTheory.Adjunction.instMonoCoeEquivHomObjHomEquivOfReflectsMonomorphisms
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
{F : Functor C D}
{F' : Functor D C}
(adj : F ⊣ F')
{X : C}
{Y : D}
(f : F.obj X ⟶ Y)
[hf : Mono f]
[F.ReflectsMonomorphisms]
:
@[simp]
theorem
CategoryTheory.Functor.strongEpi_map_iff_strongEpi_of_isEquivalence
{C : Type u_1}
{D : Type u_2}
[Category.{u_3, u_1} C]
[Category.{u_4, u_2} D]
{F : Functor C D}
{A B : C}
(f : A ⟶ B)
[F.IsEquivalence]
: