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] : CategoryTheory.EffectiveEpiFamilyStruct Y fun (a : α) => CategoryTheory.CategoryStruct.comp (g a) (f a)

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.

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] : CategoryTheory.EffectiveEpiFamilyStruct Y fun (a : α) => CategoryTheory.CategoryStruct.comp (g a) (f a)

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

Equations

• CategoryTheory.effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi f g = CategoryTheory.effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi' f g (fun (a : α) => CategoryTheory.section_ (g a)) ⋯

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] : CategoryTheory.EffectiveEpiFamily Y fun (a : α) => CategoryTheory.CategoryStruct.comp (g a) (f a)

Equations

• ⋯ = ⋯

instance CategoryTheory.IsSplitEpi.EffectiveEpi {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} (f : X ⟶ B) [CategoryTheory.IsSplitEpi f] : CategoryTheory.EffectiveEpi f

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.effectiveEpiFamilyStructOfComp {C : Type u_2} [CategoryTheory.Category.{u_4, u_2} C] {I : Type u_3} {Z : I → C} {Y : I → C} {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)] : CategoryTheory.EffectiveEpiFamilyStruct Y f

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.

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)] : CategoryTheory.EffectiveEpiFamily X f

theorem CategoryTheory.effectiveEpi_of_effectiveEpi_epi_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {B : C} {X : C} {Y : C} (f : X ⟶ B) (g : Y ⟶ X) [CategoryTheory.Epi g] [CategoryTheory.EffectiveEpi (CategoryTheory.CategoryStruct.comp g f)] : CategoryTheory.EffectiveEpi f

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₂)) : CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e 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) [CategoryTheory.EffectiveEpiFamily X π] (i : B ⟶ B') [CategoryTheory.IsIso i] : CategoryTheory.EffectiveEpiFamilyStruct X fun (a : α) => CategoryTheory.CategoryStruct.comp (π a) 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.

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) [CategoryTheory.EffectiveEpiFamily X π] (i : B ⟶ B') [CategoryTheory.IsIso i] : CategoryTheory.EffectiveEpiFamily X fun (a : α) => CategoryTheory.CategoryStruct.comp (π a) i

Equations

• ⋯ = ⋯