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
.
Equivalences preserve effective epimorphic families
Equations
- One or more equations did not get rendered due to their size.
Instances For
A class describing the property of preserving 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
A class describing the property of preserving effective epimorphic families.
- preserves : ∀ {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) [inst : CategoryTheory.EffectiveEpiFamily X π], CategoryTheory.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
A class describing the property of preserving finite effective epimorphic families.
- preserves : ∀ {α : Type} [inst : Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) [inst : CategoryTheory.EffectiveEpiFamily X π], CategoryTheory.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
A class describing the property of reflecting effective epimorphisms.
- reflects : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.EffectiveEpi (F.map f) → CategoryTheory.EffectiveEpi f
A functor reflects effective epimorphisms if morphisms that are mapped to epimorphisms are themselves effective epimorphisms.
Instances
A class describing the property of reflecting effective epimorphic families.
- reflects : ∀ {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B), (CategoryTheory.EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)) → CategoryTheory.EffectiveEpiFamily X π
A functor reflects effective epimorphic families if families that are mapped to effective epimorphic families are themselves effective epimorphic families.
Instances
A class describing the property of reflecting finite effective epimorphic families.
- reflects : ∀ {α : Type} [inst : Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B), (CategoryTheory.EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)) → CategoryTheory.EffectiveEpiFamily X π
A functor reflects finite effective epimorphic families if finite families that are mapped to effective epimorphic families are themselves effective epimorphic families.