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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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₂)

noncomputable def CategoryTheory.effectiveEpiFamilyStructOfEquivalence {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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

instance CategoryTheory.instEffectiveEpiFamilyObjMapOfIsEquivalence {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : Prop

A class describing the property of preserving effective epimorphisms.

• preserves {X Y : C} (f : X ⟶ Y) [EffectiveEpi f] : EffectiveEpi (F.map f)

  A functor preserves effective epimorphisms if it maps effective epimorphisms to effective epimorphisms.

instance CategoryTheory.Functor.map_effectiveEpi {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) [F.PreservesEffectiveEpis] {X Y : C} (f : X ⟶ Y) [EffectiveEpi f] : EffectiveEpi (F.map f)

instance CategoryTheory.Functor.instPreservesEffectiveEpisOfIsRegularEpiCategoryOfPreservesEpimorphismsOfHasPullbacks {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] [IsRegularEpiCategory D] (F : Functor C D) [F.PreservesEpimorphisms] [Limits.HasPullbacks D] : F.PreservesEffectiveEpis

class CategoryTheory.Functor.PreservesEffectiveEpiFamilies {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : Prop

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.

instance CategoryTheory.Functor.map_effectiveEpiFamily {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : Prop

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.

instance CategoryTheory.Functor.map_finite_effectiveEpiFamily {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) [F.PreservesEffectiveEpiFamilies] : F.PreservesFiniteEffectiveEpiFamilies

instance CategoryTheory.Functor.instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) [F.PreservesFiniteEffectiveEpiFamilies] : F.PreservesEffectiveEpis

instance CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) [F.IsEquivalence] : F.PreservesEffectiveEpiFamilies

instance CategoryTheory.Functor.instPreservesEffectiveEpisComp {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {E : Type u_3} [Category.{v_3, u_3} E] (F : Functor C D) (G : Functor D E) [F.PreservesEffectiveEpis] [G.PreservesEffectiveEpis] : (F.comp G).PreservesEffectiveEpis

instance CategoryTheory.Functor.instPreservesFiniteEffectiveEpiFamiliesComp {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {E : Type u_3} [Category.{v_3, u_3} E] (F : Functor C D) (G : Functor D E) [F.PreservesFiniteEffectiveEpiFamilies] [G.PreservesFiniteEffectiveEpiFamilies] : (F.comp G).PreservesFiniteEffectiveEpiFamilies

instance CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesComp {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {E : Type u_3} [Category.{v_3, u_3} E] (F : Functor C D) (G : Functor D E) [F.PreservesEffectiveEpiFamilies] [G.PreservesEffectiveEpiFamilies] : (F.comp G).PreservesEffectiveEpiFamilies

class CategoryTheory.Functor.ReflectsEffectiveEpis {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : Prop

A class describing the property of reflecting effective epimorphisms.

• reflects {X Y : C} (f : X ⟶ Y) : EffectiveEpi (F.map f) → EffectiveEpi f

  A functor reflects effective epimorphisms if morphisms that are mapped to epimorphisms are themselves effective epimorphisms.

theorem CategoryTheory.Functor.effectiveEpi_of_map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) [F.ReflectsEffectiveEpis] {X Y : C} (f : X ⟶ Y) (h : EffectiveEpi (F.map f)) : EffectiveEpi f

class CategoryTheory.Functor.ReflectsEffectiveEpiFamilies {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : Prop

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.

theorem CategoryTheory.Functor.effectiveEpiFamily_of_map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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)) : EffectiveEpiFamily X π

class CategoryTheory.Functor.ReflectsFiniteEffectiveEpiFamilies {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) : Prop

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.

theorem CategoryTheory.Functor.finite_effectiveEpiFamily_of_map {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, 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)) : EffectiveEpiFamily X π

instance CategoryTheory.Functor.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) [F.ReflectsEffectiveEpiFamilies] : F.ReflectsFiniteEffectiveEpiFamilies

instance CategoryTheory.Functor.instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) [F.ReflectsFiniteEffectiveEpiFamilies] : F.ReflectsEffectiveEpis

instance CategoryTheory.Functor.instReflectsEffectiveEpiFamiliesOfIsEquivalence {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] (F : Functor C D) [F.IsEquivalence] : F.ReflectsEffectiveEpiFamilies

instance CategoryTheory.Functor.instReflectsEffectiveEpisComp {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {E : Type u_3} [Category.{v_3, u_3} E] (F : Functor C D) (G : Functor D E) [F.ReflectsEffectiveEpis] [G.ReflectsEffectiveEpis] : (F.comp G).ReflectsEffectiveEpis

instance CategoryTheory.Functor.instReflectsFiniteEffectiveEpiFamiliesComp {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {E : Type u_3} [Category.{v_3, u_3} E] (F : Functor C D) (G : Functor D E) [F.ReflectsFiniteEffectiveEpiFamilies] [G.ReflectsFiniteEffectiveEpiFamilies] : (F.comp G).ReflectsFiniteEffectiveEpiFamilies

instance CategoryTheory.Functor.instReflectsEffectiveEpiFamiliesComp {C : Type u_1} [Category.{v_1, u_1} C] {D : Type u_2} [Category.{v_2, u_2} D] {E : Type u_3} [Category.{v_3, u_3} E] (F : Functor C D) (G : Functor D E) [F.ReflectsEffectiveEpiFamilies] [G.ReflectsEffectiveEpiFamilies] : (F.comp G).ReflectsEffectiveEpiFamilies