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 C]
{D : Type u_2}
[Category D]
(e : Equivalence C D)
{B : C}
{α : Type u_3}
(X : α → C)
(π : (a : α) → Quiver.Hom (X a) B)
{W : D}
(ε : (a : α) → Quiver.Hom (e.functor.obj (X a)) W)
(h :
∀ {Z : D} (a₁ a₂ : α) (g₁ : Quiver.Hom Z (e.functor.obj (X a₁))) (g₂ : Quiver.Hom Z (e.functor.obj (X a₂))),
Eq (CategoryStruct.comp g₁ (e.functor.map (π a₁))) (CategoryStruct.comp g₂ (e.functor.map (π a₂))) →
Eq (CategoryStruct.comp g₁ (ε a₁)) (CategoryStruct.comp g₂ (ε a₂)))
{Z : C}
(a₁ a₂ : α)
(g₁ : Quiver.Hom Z (X a₁))
(g₂ : Quiver.Hom Z (X a₂))
(hg : Eq (CategoryStruct.comp g₁ (π a₁)) (CategoryStruct.comp g₂ (π a₂)))
:
Eq (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 C]
{D : Type u_2}
[Category D]
(e : Equivalence C D)
{B : C}
{α : Type u_3}
(X : α → C)
(π : (a : α) → Quiver.Hom (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
theorem
CategoryTheory.instEffectiveEpiFamilyObjMapOfIsEquivalence
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
{B : C}
{α : Type u_3}
(X : α → C)
(π : (a : α) → Quiver.Hom (X a) B)
[EffectiveEpiFamily X π]
(F : Functor C D)
[F.IsEquivalence]
:
EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)
structure
CategoryTheory.Functor.PreservesEffectiveEpis
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category 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 For
theorem
CategoryTheory.Functor.map_effectiveEpi
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.PreservesEffectiveEpis]
{X Y : C}
(f : Quiver.Hom X Y)
[EffectiveEpi f]
:
EffectiveEpi (F.map f)
structure
CategoryTheory.Functor.PreservesEffectiveEpiFamilies
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
:
A class describing the property of preserving effective epimorphic families.
- preserves {α : Type u} {B : C} (X : α → C) (π : (a : α) → Quiver.Hom (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 For
theorem
CategoryTheory.Functor.map_effectiveEpiFamily
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.PreservesEffectiveEpiFamilies]
{α : Type u}
{B : C}
(X : α → C)
(π : (a : α) → Quiver.Hom (X a) B)
[EffectiveEpiFamily X π]
:
EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)
structure
CategoryTheory.Functor.PreservesFiniteEffectiveEpiFamilies
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
:
A class describing the property of preserving finite effective epimorphic families.
- preserves {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → Quiver.Hom (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 For
theorem
CategoryTheory.Functor.map_finite_effectiveEpiFamily
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.PreservesFiniteEffectiveEpiFamilies]
{α : Type}
[Finite α]
{B : C}
(X : α → C)
(π : (a : α) → Quiver.Hom (X a) B)
[EffectiveEpiFamily X π]
:
EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)
theorem
CategoryTheory.Functor.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.PreservesEffectiveEpiFamilies]
:
theorem
CategoryTheory.Functor.instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.PreservesFiniteEffectiveEpiFamilies]
:
theorem
CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.IsEquivalence]
:
structure
CategoryTheory.Functor.ReflectsEffectiveEpis
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category 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 For
theorem
CategoryTheory.Functor.effectiveEpi_of_map
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.ReflectsEffectiveEpis]
{X Y : C}
(f : Quiver.Hom X Y)
(h : EffectiveEpi (F.map f))
:
structure
CategoryTheory.Functor.ReflectsEffectiveEpiFamilies
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
:
A class describing the property of reflecting effective epimorphic families.
- reflects {α : Type u} {B : C} (X : α → C) (π : (a : α) → Quiver.Hom (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 For
theorem
CategoryTheory.Functor.effectiveEpiFamily_of_map
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.ReflectsEffectiveEpiFamilies]
{α : Type u}
{B : C}
(X : α → C)
(π : (a : α) → Quiver.Hom (X a) B)
(h : EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a))
:
structure
CategoryTheory.Functor.ReflectsFiniteEffectiveEpiFamilies
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
:
A class describing the property of reflecting finite effective epimorphic families.
- reflects {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → Quiver.Hom (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 For
theorem
CategoryTheory.Functor.finite_effectiveEpiFamily_of_map
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.ReflectsFiniteEffectiveEpiFamilies]
{α : Type}
[Finite α]
{B : C}
(X : α → C)
(π : (a : α) → Quiver.Hom (X a) B)
(h : EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a))
:
theorem
CategoryTheory.Functor.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.ReflectsEffectiveEpiFamilies]
:
theorem
CategoryTheory.Functor.instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.ReflectsFiniteEffectiveEpiFamilies]
:
theorem
CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence_1
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.IsEquivalence]
:
theorem
CategoryTheory.Functor.instReflectsEffectiveEpiFamiliesOfIsEquivalence
{C : Type u_1}
[Category C]
{D : Type u_2}
[Category D]
(F : Functor C D)
[F.IsEquivalence]
: