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} [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.

instance CategoryTheory.instEffectiveEpiFamilyObjMapOfIsEquivalence {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) [F.IsEquivalence] : 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) : Prop

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.

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) [F.PreservesEffectiveEpis] {X Y : C} (f : X ⟶ Y) [CategoryTheory.EffectiveEpi f] : CategoryTheory.EffectiveEpi (F.map f)

Equations

• ⋯ = ⋯

class CategoryTheory.Functor.PreservesEffectiveEpiFamilies {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) : Prop

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.

instance CategoryTheory.Functor.map_effectiveEpiFamily {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) [F.PreservesEffectiveEpiFamilies] {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] : CategoryTheory.EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)

Equations

• ⋯ = ⋯

class CategoryTheory.Functor.PreservesFiniteEffectiveEpiFamilies {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) : Prop

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.

instance CategoryTheory.Functor.map_finite_effectiveEpiFamily {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) [F.PreservesFiniteEffectiveEpiFamilies] {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] : CategoryTheory.EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpiFamilies {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) [F.PreservesEffectiveEpiFamilies] : F.PreservesFiniteEffectiveEpiFamilies

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instPreservesEffectiveEpisOfPreservesFiniteEffectiveEpiFamilies {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) [F.PreservesFiniteEffectiveEpiFamilies] : F.PreservesEffectiveEpis

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence {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) [F.IsEquivalence] : F.PreservesEffectiveEpiFamilies

Equations

• ⋯ = ⋯

class CategoryTheory.Functor.ReflectsEffectiveEpis {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) : Prop

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.

theorem CategoryTheory.Functor.effectiveEpi_of_map {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) [F.ReflectsEffectiveEpis] {X Y : C} (f : X ⟶ Y) (h : CategoryTheory.EffectiveEpi (F.map f)) : CategoryTheory.EffectiveEpi f

class CategoryTheory.Functor.ReflectsEffectiveEpiFamilies {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) : Prop

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.

theorem CategoryTheory.Functor.effectiveEpiFamily_of_map {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) [F.ReflectsEffectiveEpiFamilies] {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) (h : CategoryTheory.EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)) : CategoryTheory.EffectiveEpiFamily X π

class CategoryTheory.Functor.ReflectsFiniteEffectiveEpiFamilies {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) : Prop

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.

theorem CategoryTheory.Functor.finite_effectiveEpiFamily_of_map {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) [F.ReflectsFiniteEffectiveEpiFamilies] {α : Type} [Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) (h : CategoryTheory.EffectiveEpiFamily (fun (a : α) => F.obj (X a)) fun (a : α) => F.map (π a)) : CategoryTheory.EffectiveEpiFamily X π

instance CategoryTheory.Functor.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpiFamilies {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) [F.ReflectsEffectiveEpiFamilies] : F.ReflectsFiniteEffectiveEpiFamilies

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instReflectsEffectiveEpisOfReflectsFiniteEffectiveEpiFamilies {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) [F.ReflectsFiniteEffectiveEpiFamilies] : F.ReflectsEffectiveEpis

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence_1 {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) [F.IsEquivalence] : F.PreservesEffectiveEpiFamilies

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.instReflectsEffectiveEpiFamiliesOfIsEquivalence {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) [F.IsEquivalence] : F.ReflectsEffectiveEpiFamilies

Equations

• ⋯ = ⋯