Functors preserving effective epimorphisms #
This file concerns functors which preserve and/or reflect effective epimorphisms and effective epimorphic families.
TODO #
- Find nice sufficient conditions in terms of preserving/reflecting (co)limits, to preserve/reflect
effective epis, similar to
CategoryTheory.preserves_epi_of_preservesColimit.
theorem
CategoryTheory.effectiveEpiFamilyStructOfEquivalence_aux
{C : Type u_1}
[Category.{u_5, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(e : C ≌ D)
{B : C}
{α : Type u_3}
(X : α → C)
(π : (a : α) → X a ⟶ B)
{W : D}
(ε : (a : α) → e.functor.obj (X a) ⟶ W)
(h :
∀ {Z : D} (a₁ a₂ : α) (g₁ : Z ⟶ e.functor.obj (X a₁)) (g₂ : Z ⟶ e.functor.obj (X a₂)),
CategoryStruct.comp g₁ (e.functor.map (π a₁)) = CategoryStruct.comp g₂ (e.functor.map (π a₂)) →
CategoryStruct.comp g₁ (ε a₁) = CategoryStruct.comp g₂ (ε a₂))
{Z : C}
(a₁ a₂ : α)
(g₁ : Z ⟶ X a₁)
(g₂ : Z ⟶ X a₂)
(hg : CategoryStruct.comp g₁ (π a₁) = CategoryStruct.comp g₂ (π a₂))
:
CategoryStruct.comp g₁ ((fun (a : α) => CategoryStruct.comp (e.unit.app (X a)) (e.inverse.map (ε a))) a₁) = CategoryStruct.comp g₂ ((fun (a : α) => CategoryStruct.comp (e.unit.app (X a)) (e.inverse.map (ε a))) a₂)
def
CategoryTheory.effectiveEpiFamilyStructOfEquivalence
{C : Type u_1}
[Category.{u_4, u_1} C]
{D : Type u_2}
[Category.{u_5, u_2} D]
(e : C ≌ D)
{B : C}
{α : Type u_3}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[EffectiveEpiFamily X π]
:
EffectiveEpiFamilyStruct (fun (a : α) => e.functor.obj (X a)) fun (a : α) => e.functor.map (π a)
Equivalences preserve effective epimorphic families
Equations
- One or more equations did not get rendered due to their size.
Instances For
instance
CategoryTheory.instEffectiveEpiFamilyObjMapOfIsEquivalence
{C : Type u_1}
[Category.{u_4, u_1} C]
{D : Type u_2}
[Category.{u_5, u_2} D]
{B : C}
{α : Type u_3}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[EffectiveEpiFamily X π]
(F : Functor C D)
[F.IsEquivalence]
:
EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)
class
CategoryTheory.Functor.PreservesEffectiveEpis
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
:
A class describing the property of preserving effective epimorphisms.
A functor preserves effective epimorphisms if it maps effective epimorphisms to effective epimorphisms.
Instances
instance
CategoryTheory.Functor.map_effectiveEpi
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.PreservesEffectiveEpis]
{X Y : C}
(f : X ⟶ Y)
[EffectiveEpi f]
:
EffectiveEpi (F.map f)
class
CategoryTheory.Functor.PreservesEffectiveEpiFamilies
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
:
A class describing the property of preserving effective epimorphic families.
- preserves {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) [EffectiveEpiFamily X π] : EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)
A functor preserves effective epimorphic families if it maps effective epimorphic families to effective epimorphic families.
Instances
instance
CategoryTheory.Functor.map_effectiveEpiFamily
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.PreservesEffectiveEpiFamilies]
{α : Type u}
{B : C}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[EffectiveEpiFamily X π]
:
EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)
class
CategoryTheory.Functor.PreservesFiniteEffectiveEpiFamilies
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
:
A class describing the property of preserving finite effective epimorphic families.
- preserves {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) [EffectiveEpiFamily X π] : EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)
A functor preserves finite effective epimorphic families if it maps finite effective epimorphic families to effective epimorphic families.
Instances
instance
CategoryTheory.Functor.map_finite_effectiveEpiFamily
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.PreservesFiniteEffectiveEpiFamilies]
{α : Type}
[Finite α]
{B : C}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[EffectiveEpiFamily X π]
:
EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)
instance
CategoryTheory.Functor.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.PreservesEffectiveEpiFamilies]
:
instance
CategoryTheory.Functor.instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.PreservesFiniteEffectiveEpiFamilies]
:
instance
CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.IsEquivalence]
:
class
CategoryTheory.Functor.ReflectsEffectiveEpis
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
:
A class describing the property of reflecting effective epimorphisms.
A functor reflects effective epimorphisms if morphisms that are mapped to epimorphisms are themselves effective epimorphisms.
Instances
theorem
CategoryTheory.Functor.effectiveEpi_of_map
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.ReflectsEffectiveEpis]
{X Y : C}
(f : X ⟶ Y)
(h : EffectiveEpi (F.map f))
:
class
CategoryTheory.Functor.ReflectsEffectiveEpiFamilies
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
:
A class describing the property of reflecting effective epimorphic families.
- reflects {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) : (EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)) → EffectiveEpiFamily X π
A functor reflects effective epimorphic families if families that are mapped to effective epimorphic families are themselves effective epimorphic families.
Instances
theorem
CategoryTheory.Functor.effectiveEpiFamily_of_map
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.ReflectsEffectiveEpiFamilies]
{α : Type u}
{B : C}
(X : α → C)
(π : (a : α) → X a ⟶ B)
(h : EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a))
:
class
CategoryTheory.Functor.ReflectsFiniteEffectiveEpiFamilies
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
:
A class describing the property of reflecting finite effective epimorphic families.
- reflects {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) : (EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)) → EffectiveEpiFamily X π
A functor reflects finite effective epimorphic families if finite families that are mapped to effective epimorphic families are themselves effective epimorphic families.
Instances
theorem
CategoryTheory.Functor.finite_effectiveEpiFamily_of_map
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.ReflectsFiniteEffectiveEpiFamilies]
{α : Type}
[Finite α]
{B : C}
(X : α → C)
(π : (a : α) → X a ⟶ B)
(h : EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a))
:
instance
CategoryTheory.Functor.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.ReflectsEffectiveEpiFamilies]
:
instance
CategoryTheory.Functor.instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.ReflectsFiniteEffectiveEpiFamilies]
:
instance
CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence_1
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.IsEquivalence]
:
instance
CategoryTheory.Functor.instReflectsEffectiveEpiFamiliesOfIsEquivalence
{C : Type u_1}
[Category.{u_3, u_1} C]
{D : Type u_2}
[Category.{u_4, u_2} D]
(F : Functor C D)
[F.IsEquivalence]
: