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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.PreservesMonomorphisms]
{X Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
CategoryTheory.Mono (F.map f)
class
CategoryTheory.Functor.PreservesEpimorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.PreservesEpimorphisms]
{X Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
CategoryTheory.Epi (F.map f)
class
CategoryTheory.Functor.ReflectsMonomorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.ReflectsMonomorphisms]
{X Y : C}
{f : X ⟶ Y}
(h : CategoryTheory.Mono (F.map f))
:
class
CategoryTheory.Functor.ReflectsEpimorphisms
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.ReflectsEpimorphisms]
{X Y : C}
{f : X ⟶ Y}
(h : CategoryTheory.Epi (F.map f))
:
instance
CategoryTheory.Functor.preservesMonomorphisms_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.PreservesMonomorphisms]
[G.PreservesMonomorphisms]
:
(F.comp G).PreservesMonomorphisms
instance
CategoryTheory.Functor.preservesEpimorphisms_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.PreservesEpimorphisms]
[G.PreservesEpimorphisms]
:
(F.comp G).PreservesEpimorphisms
instance
CategoryTheory.Functor.reflectsMonomorphisms_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.ReflectsMonomorphisms]
[G.ReflectsMonomorphisms]
:
(F.comp G).ReflectsMonomorphisms
instance
CategoryTheory.Functor.reflectsEpimorphisms_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.ReflectsEpimorphisms]
[G.ReflectsEpimorphisms]
:
(F.comp G).ReflectsEpimorphisms
theorem
CategoryTheory.Functor.preservesEpimorphisms_of_preserves_of_reflects
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[(F.comp G).PreservesEpimorphisms]
[G.ReflectsEpimorphisms]
:
F.PreservesEpimorphisms
theorem
CategoryTheory.Functor.preservesMonomorphisms_of_preserves_of_reflects
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[(F.comp G).PreservesMonomorphisms]
[G.ReflectsMonomorphisms]
:
F.PreservesMonomorphisms
theorem
CategoryTheory.Functor.reflectsEpimorphisms_of_preserves_of_reflects
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[G.PreservesEpimorphisms]
[(F.comp G).ReflectsEpimorphisms]
:
F.ReflectsEpimorphisms
theorem
CategoryTheory.Functor.reflectsMonomorphisms_of_preserves_of_reflects
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[G.PreservesMonomorphisms]
[(F.comp G).ReflectsMonomorphisms]
:
F.ReflectsMonomorphisms
theorem
CategoryTheory.Functor.preservesMonomorphisms.of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D}
[F.PreservesMonomorphisms]
(α : F ≅ G)
:
G.PreservesMonomorphisms
theorem
CategoryTheory.Functor.preservesMonomorphisms.iso_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D}
(α : F ≅ G)
:
F.PreservesMonomorphisms ↔ G.PreservesMonomorphisms
theorem
CategoryTheory.Functor.preservesEpimorphisms.of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D}
[F.PreservesEpimorphisms]
(α : F ≅ G)
:
G.PreservesEpimorphisms
theorem
CategoryTheory.Functor.preservesEpimorphisms.iso_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D}
(α : F ≅ G)
:
F.PreservesEpimorphisms ↔ G.PreservesEpimorphisms
theorem
CategoryTheory.Functor.reflectsMonomorphisms.of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D}
[F.ReflectsMonomorphisms]
(α : F ≅ G)
:
G.ReflectsMonomorphisms
theorem
CategoryTheory.Functor.reflectsMonomorphisms.iso_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D}
(α : F ≅ G)
:
F.ReflectsMonomorphisms ↔ G.ReflectsMonomorphisms
theorem
CategoryTheory.Functor.reflectsEpimorphisms.of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D}
[F.ReflectsEpimorphisms]
(α : F ≅ G)
:
G.ReflectsEpimorphisms
theorem
CategoryTheory.Functor.reflectsEpimorphisms.iso_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F G : CategoryTheory.Functor C D}
(α : F ≅ G)
:
F.ReflectsEpimorphisms ↔ G.ReflectsEpimorphisms
theorem
CategoryTheory.Functor.preservesEpimorphsisms_of_adjunction
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
:
F.PreservesEpimorphisms
@[instance 100]
instance
CategoryTheory.Functor.preservesEpimorphisms_of_isLeftAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.IsLeftAdjoint]
:
F.PreservesEpimorphisms
theorem
CategoryTheory.Functor.preservesMonomorphisms_of_adjunction
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
:
G.PreservesMonomorphisms
@[instance 100]
instance
CategoryTheory.Functor.preservesMonomorphisms_of_isRightAdjoint
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.IsRightAdjoint]
:
F.PreservesMonomorphisms
@[instance 100]
instance
CategoryTheory.Functor.reflectsMonomorphisms_of_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Faithful]
:
F.ReflectsMonomorphisms
@[instance 100]
instance
CategoryTheory.Functor.reflectsEpimorphisms_of_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Faithful]
:
F.ReflectsEpimorphisms
noncomputable def
CategoryTheory.Functor.splitEpiEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X Y : C}
(f : X ⟶ Y)
[F.Full]
[F.Faithful]
:
CategoryTheory.SplitEpi f ≃ CategoryTheory.SplitEpi (F.map f)
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X Y : C}
(f : X ⟶ Y)
[F.Full]
[F.Faithful]
:
CategoryTheory.IsSplitEpi (F.map f) ↔ CategoryTheory.IsSplitEpi f
noncomputable def
CategoryTheory.Functor.splitMonoEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X Y : C}
(f : X ⟶ Y)
[F.Full]
[F.Faithful]
:
CategoryTheory.SplitMono f ≃ CategoryTheory.SplitMono (F.map f)
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₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X Y : C}
(f : X ⟶ Y)
[F.Full]
[F.Faithful]
:
CategoryTheory.IsSplitMono (F.map f) ↔ CategoryTheory.IsSplitMono f
@[simp]
theorem
CategoryTheory.Functor.epi_map_iff_epi
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X Y : C}
(f : X ⟶ Y)
[hF₁ : F.PreservesEpimorphisms]
[hF₂ : F.ReflectsEpimorphisms]
:
CategoryTheory.Epi (F.map f) ↔ CategoryTheory.Epi f
@[simp]
theorem
CategoryTheory.Functor.mono_map_iff_mono
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X Y : C}
(f : X ⟶ Y)
[hF₁ : F.PreservesMonomorphisms]
[hF₂ : F.ReflectsMonomorphisms]
:
CategoryTheory.Mono (F.map f) ↔ CategoryTheory.Mono f
theorem
CategoryTheory.Functor.splitEpiCategoryImpOfIsEquivalence
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.IsEquivalence]
[CategoryTheory.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}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
{F : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor D C}
{A B : C}
(adj : F ⊣ F')
(f : A ⟶ B)
[F'.PreservesMonomorphisms]
[F.PreservesEpimorphisms]
[CategoryTheory.StrongEpi f]
:
CategoryTheory.StrongEpi (F.map f)
instance
CategoryTheory.Adjunction.strongEpi_map_of_isEquivalence
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
{F : CategoryTheory.Functor C D}
{A B : C}
[F.IsEquivalence]
(f : A ⟶ B)
[_h : CategoryTheory.StrongEpi f]
:
CategoryTheory.StrongEpi (F.map f)
instance
CategoryTheory.Adjunction.instMonoCoeEquivHomObjHomEquivOfReflectsMonomorphisms
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
{F : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor D C}
(adj : F ⊣ F')
{X : C}
{Y : D}
(f : F.obj X ⟶ Y)
[hf : CategoryTheory.Mono f]
[F.ReflectsMonomorphisms]
:
CategoryTheory.Mono ((adj.homEquiv X Y) f)
@[simp]
theorem
CategoryTheory.Functor.strongEpi_map_iff_strongEpi_of_isEquivalence
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
{F : CategoryTheory.Functor C D}
{A B : C}
(f : A ⟶ B)
[F.IsEquivalence]
:
CategoryTheory.StrongEpi (F.map f) ↔ CategoryTheory.StrongEpi f