Documentation

Mathlib.CategoryTheory.EffectiveEpi.Comp

Composition of effective epimorphisms #

This file provides EffectiveEpi instances for certain compositions.

noncomputable def CategoryTheory.effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi' {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {α : Type u_2} {B : C} {X : αC} {Y : αC} (f : (a : α) → X a B) (g : (a : α) → Y a X a) (i : (a : α) → X a Y a) (hi : ∀ (a : α), CategoryTheory.CategoryStruct.comp (i a) (g a) = CategoryTheory.CategoryStruct.id (X a)) [CategoryTheory.EffectiveEpiFamily X f] :

An effective epi family precomposed by a family of split epis is effective epimorphic. This version takes an explicit section to the split epis, and is mainly used to define effectiveEpiStructCompOfEffectiveEpiSplitEpi, which takes a IsSplitEpi instance instead.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    noncomputable def CategoryTheory.effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {α : Type u_2} {B : C} {X : αC} {Y : αC} (f : (a : α) → X a B) (g : (a : α) → Y a X a) [∀ (a : α), CategoryTheory.IsSplitEpi (g a)] [CategoryTheory.EffectiveEpiFamily X f] :

    An effective epi family precomposed with a family of split epis is effective epimorphic.

    Equations
    Instances For
      instance CategoryTheory.instEffectiveEpiFamilyCompOfIsSplitEpi {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {α : Type u_2} {B : C} {X : αC} {Y : αC} (f : (a : α) → X a B) (g : (a : α) → Y a X a) [∀ (a : α), CategoryTheory.IsSplitEpi (g a)] [CategoryTheory.EffectiveEpiFamily X f] :
      Equations
      • =
      noncomputable def CategoryTheory.effectiveEpiFamilyStructOfComp {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] {I : Type u_3} {Z : IC} {Y : IC} {X : C} (g : (i : I) → Z i Y i) (f : (i : I) → Y i X) [CategoryTheory.EffectiveEpiFamily Z fun (i : I) => CategoryTheory.CategoryStruct.comp (g i) (f i)] [∀ (i : I), CategoryTheory.Epi (g i)] :

      If a family of morphisms with fixed target, precomposed by a family of epis is effective epimorphic, then the original family is as well.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        theorem CategoryTheory.effectiveEpiFamily_of_effectiveEpi_epi_comp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {α : Type u_2} {B : C} {X : αC} {Y : αC} (f : (a : α) → X a B) (g : (a : α) → Y a X a) [∀ (a : α), CategoryTheory.Epi (g a)] [CategoryTheory.EffectiveEpiFamily Y fun (a : α) => CategoryTheory.CategoryStruct.comp (g a) (f a)] :
        theorem CategoryTheory.effectiveEpiFamilyStructCompIso_aux {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {B' : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) (i : B B') {W : C} (e : (a : α) → X a W) (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z X a₁) (g₂ : Z X a₂), CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.CategoryStruct.comp (π a₁) i) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.CategoryStruct.comp (π a₂) i)CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) {Z : C} (a₁ : α) (a₂ : α) (g₁ : Z X a₁) (g₂ : Z X a₂) (hg : CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂)) :
        noncomputable def CategoryTheory.effectiveEpiFamilyStructCompIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {B' : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) (i : B B') [CategoryTheory.EffectiveEpiFamily X π] [CategoryTheory.IsIso i] :

        An effective epi family followed by an iso is an effective epi family.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          instance CategoryTheory.instEffectiveEpiFamilyComp {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {B' : C} {α : Type u_2} (X : αC) (π : (a : α) → X a B) (i : B B') [CategoryTheory.EffectiveEpiFamily X π] [CategoryTheory.IsIso i] :
          Equations
          • =