Functors preserving effective epimorphisms #
This file concerns functors which preserve effective epimorphisms and effective epimporphic families.
TODO #
- Define the classes
PreservesEffectiveEpiFamilies,ReflectsEffectiveEpis, etc. - Find sufficient conditions on functors to preserve/reflect effective epis.
theorem
CategoryTheory.effectiveEpiFamilyStructOfEquivalence_aux
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{D : Type u_2}
[CategoryTheory.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₂)),
CategoryTheory.CategoryStruct.comp g₁ (e.functor.map (π a₁)) = CategoryTheory.CategoryStruct.comp g₂ (e.functor.map (π a₂)) →
CategoryTheory.CategoryStruct.comp g₁ (ε a₁) = CategoryTheory.CategoryStruct.comp g₂ (ε a₂))
{Z : C}
(a₁ : α)
(a₂ : α)
(g₁ : Z ⟶ X a₁)
(g₂ : Z ⟶ X a₂)
(hg : CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂))
:
CategoryTheory.CategoryStruct.comp g₁
((fun (a : α) => CategoryTheory.CategoryStruct.comp (e.unit.app (X a)) (e.inverse.map (ε a))) a₁) = CategoryTheory.CategoryStruct.comp g₂
((fun (a : α) => CategoryTheory.CategoryStruct.comp (e.unit.app (X a)) (e.inverse.map (ε a))) a₂)
def
CategoryTheory.effectiveEpiFamilyStructOfEquivalence
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_5, u_2} D]
(e : C ≌ D)
{B : C}
{α : Type u_3}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.EffectiveEpiFamily X π]
:
CategoryTheory.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.instEffectiveEpiFamilyObjToQuiverToCategoryStructToQuiverToCategoryStructToPrefunctorMap
{C : Type u_1}
[CategoryTheory.Category.{u_4, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_5, u_2} D]
{B : C}
{α : Type u_3}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[CategoryTheory.EffectiveEpiFamily X π]
(F : CategoryTheory.Functor C D)
[CategoryTheory.IsEquivalence F]
:
CategoryTheory.EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)
Equations
- ⋯ = ⋯
class
CategoryTheory.Functor.PreservesEffectiveEpis
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
:
A functor preserves effective epimorphisms if it maps effective epimorphisms to effective epimorphisms.
- preserves : ∀ {X Y : C} (f : X ⟶ Y) [inst : CategoryTheory.EffectiveEpi f], CategoryTheory.EffectiveEpi (F.map f)
A functor preserves effective epimorphisms if it maps effective epimorphisms to effective epimorphisms.
Instances
instance
CategoryTheory.Functor.map_effectiveEpi
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.PreservesEffectiveEpis F]
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.EffectiveEpi f]
:
CategoryTheory.EffectiveEpi (F.map f)
Equations
- ⋯ = ⋯
instance
CategoryTheory.Functor.instPreservesEffectiveEpis
{C : Type u_1}
[CategoryTheory.Category.{u_3, u_1} C]
{D : Type u_2}
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.IsEquivalence F]
:
Equations
- ⋯ = ⋯