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.
- preserves : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Mono f], CategoryTheory.Mono (F.map f)
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)
[CategoryTheory.Functor.PreservesMonomorphisms F]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
CategoryTheory.Mono (F.map f)
Equations
- ⋯ = ⋯
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.
- preserves : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.Epi f], CategoryTheory.Epi (F.map f)
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)
[CategoryTheory.Functor.PreservesEpimorphisms F]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Epi f]
:
CategoryTheory.Epi (F.map f)
Equations
- ⋯ = ⋯
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.
- reflects : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Mono (F.map f) → CategoryTheory.Mono f
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)
[CategoryTheory.Functor.ReflectsMonomorphisms F]
{X : C}
{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.
- reflects : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.Epi (F.map f) → CategoryTheory.Epi f
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)
[CategoryTheory.Functor.ReflectsEpimorphisms F]
{X : C}
{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)
[CategoryTheory.Functor.PreservesMonomorphisms F]
[CategoryTheory.Functor.PreservesMonomorphisms G]
:
Equations
- ⋯ = ⋯
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)
[CategoryTheory.Functor.PreservesEpimorphisms F]
[CategoryTheory.Functor.PreservesEpimorphisms G]
:
Equations
- ⋯ = ⋯
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)
[CategoryTheory.Functor.ReflectsMonomorphisms F]
[CategoryTheory.Functor.ReflectsMonomorphisms G]
:
Equations
- ⋯ = ⋯
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)
[CategoryTheory.Functor.ReflectsEpimorphisms F]
[CategoryTheory.Functor.ReflectsEpimorphisms G]
:
Equations
- ⋯ = ⋯
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)
[CategoryTheory.Functor.PreservesEpimorphisms (CategoryTheory.Functor.comp F G)]
[CategoryTheory.Functor.ReflectsEpimorphisms G]
:
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)
[CategoryTheory.Functor.PreservesMonomorphisms (CategoryTheory.Functor.comp F G)]
[CategoryTheory.Functor.ReflectsMonomorphisms G]
:
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)
[CategoryTheory.Functor.PreservesEpimorphisms G]
[CategoryTheory.Functor.ReflectsEpimorphisms (CategoryTheory.Functor.comp F G)]
:
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)
[CategoryTheory.Functor.PreservesMonomorphisms G]
[CategoryTheory.Functor.ReflectsMonomorphisms (CategoryTheory.Functor.comp F G)]
:
theorem
CategoryTheory.Functor.preservesMonomorphisms.of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[CategoryTheory.Functor.PreservesMonomorphisms F]
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.preservesMonomorphisms.iso_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.preservesEpimorphisms.of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[CategoryTheory.Functor.PreservesEpimorphisms F]
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.preservesEpimorphisms.iso_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.reflectsMonomorphisms.of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[CategoryTheory.Functor.ReflectsMonomorphisms F]
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.reflectsMonomorphisms.iso_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.reflectsEpimorphisms.of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
[CategoryTheory.Functor.ReflectsEpimorphisms F]
(α : F ≅ G)
:
theorem
CategoryTheory.Functor.reflectsEpimorphisms.iso_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(α : F ≅ G)
:
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)
:
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)
[CategoryTheory.IsLeftAdjoint F]
:
Equations
- ⋯ = ⋯
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)
:
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)
[CategoryTheory.IsRightAdjoint F]
:
Equations
- ⋯ = ⋯
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)
[CategoryTheory.Functor.Faithful F]
:
Equations
- ⋯ = ⋯
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)
[CategoryTheory.Functor.Faithful F]
:
Equations
- ⋯ = ⋯
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 : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Functor.Full F]
[CategoryTheory.Functor.Faithful F]
:
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 : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Functor.Full F]
[CategoryTheory.Functor.Faithful F]
:
CategoryTheory.IsSplitEpi (F.map f) ↔ CategoryTheory.IsSplitEpi f
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 : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Functor.Full F]
[CategoryTheory.Functor.Faithful F]
:
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 : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.Functor.Full F]
[CategoryTheory.Functor.Faithful F]
:
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 : C}
{Y : C}
(f : X ⟶ Y)
[hF₁ : CategoryTheory.Functor.PreservesEpimorphisms F]
[hF₂ : CategoryTheory.Functor.ReflectsEpimorphisms F]
:
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 : C}
{Y : C}
(f : X ⟶ Y)
[hF₁ : CategoryTheory.Functor.PreservesMonomorphisms F]
[hF₂ : CategoryTheory.Functor.ReflectsMonomorphisms F]
:
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)
[CategoryTheory.Functor.IsEquivalence F]
[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 : C}
{B : C}
(adj : F ⊣ F')
(f : A ⟶ B)
[h₁ : CategoryTheory.Functor.PreservesMonomorphisms F']
[h₂ : CategoryTheory.Functor.PreservesEpimorphisms F]
[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 : C}
{B : C}
[CategoryTheory.Functor.IsEquivalence F]
(f : A ⟶ B)
[_h : CategoryTheory.StrongEpi f]
:
CategoryTheory.StrongEpi (F.map f)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Adjunction.instMonoObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorCoeEquivHomObjToPrefunctorHomInstFunLikeEquivHomEquiv
{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]
[CategoryTheory.Functor.ReflectsMonomorphisms F]
:
CategoryTheory.Mono ((adj.homEquiv X Y) f)
Equations
- ⋯ = ⋯
@[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 : C}
{B : C}
(f : A ⟶ B)
[CategoryTheory.Functor.IsEquivalence F]
:
CategoryTheory.StrongEpi (F.map f) ↔ CategoryTheory.StrongEpi f