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₂)

source

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

source

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

⋯ = ⋯

source

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.

Instances

source

theorem CategoryTheory.Functor.PreservesEffectiveEpis.preserves {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {D : Type u_2} {inst_1 : CategoryTheory.Category.{u_4, u_2} D} {F : CategoryTheory.Functor C D} [self : F.PreservesEffectiveEpis] {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.EffectiveEpi f], CategoryTheory.EffectiveEpi (F.map f)

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

source

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

CategoryTheory.EffectiveEpi (F.map f)

Equations

⋯ = ⋯

source

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.

Instances

source

theorem CategoryTheory.Functor.PreservesEffectiveEpiFamilies.preserves {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {D : Type u_2} {inst_1 : CategoryTheory.Category.{u_4, u_2} D} {F : CategoryTheory.Functor C D} [self : F.PreservesEffectiveEpiFamilies] {α : Type u} {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) [inst_2 : 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.

source

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

⋯ = ⋯

source

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.

Instances

source

theorem CategoryTheory.Functor.PreservesFiniteEffectiveEpiFamilies.preserves {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {D : Type u_2} {inst_1 : CategoryTheory.Category.{u_4, u_2} D} {F : CategoryTheory.Functor C D} [self : F.PreservesFiniteEffectiveEpiFamilies] {α : Type} [inst_2 : Finite α] {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) [inst_3 : 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.

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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

⋯ = ⋯

source

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.

Instances

source

theorem CategoryTheory.Functor.ReflectsEffectiveEpis.reflects {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {D : Type u_2} {inst_1 : CategoryTheory.Category.{u_4, u_2} D} {F : CategoryTheory.Functor C D} [self : F.ReflectsEffectiveEpis] {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.

source

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

CategoryTheory.EffectiveEpi f

source

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.

Instances

source

theorem CategoryTheory.Functor.ReflectsEffectiveEpiFamilies.reflects {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {D : Type u_2} {inst_1 : CategoryTheory.Category.{u_4, u_2} D} {F : CategoryTheory.Functor C D} [self : F.ReflectsEffectiveEpiFamilies] {α : 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.

source

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 π

source

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.

Instances

source

theorem CategoryTheory.Functor.ReflectsFiniteEffectiveEpiFamilies.reflects {C : Type u_1} :

∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {D : Type u_2} {inst_1 : CategoryTheory.Category.{u_4, u_2} D} {F : CategoryTheory.Functor C D} [self : F.ReflectsFiniteEffectiveEpiFamilies] {α : Type} [inst_2 : 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.

source