Documentation

Mathlib.CategoryTheory.EffectiveEpi.Preserves

Functors preserving effective epimorphisms #

This file concerns functors which preserve and/or reflect effective epimorphisms and effective epimorphic families.

TODO #

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.
Instances For
    theorem 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)

    A class describing the property of preserving effective epimorphisms.

    Instances

      A class describing the property of preserving effective epimorphic families.

      Instances
        theorem 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)

        A class describing the property of preserving finite effective epimorphic families.

        Instances
          theorem 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)

          A class describing the property of reflecting 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
              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)) :

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