Composition of effective epimorphisms

This file provides EffectiveEpi instances for certain compositions.

noncomputable def CategoryTheory.effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi' {C : Type u_1} [Category.{v_1, u_1} C] {α : Type u_2} {B : C} {X Y : α → C} (f : (a : α) → X a ⟶ B) (g : (a : α) → Y a ⟶ X a) (i : (a : α) → X a ⟶ Y a) (hi : ∀ (a : α), CategoryStruct.comp (i a) (g a) = CategoryStruct.id (X a)) [EffectiveEpiFamily X f] : EffectiveEpiFamilyStruct Y fun (a : α) => 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.

noncomputable def CategoryTheory.effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi {C : Type u_1} [Category.{v_1, u_1} C] {α : Type u_2} {B : C} {X Y : α → C} (f : (a : α) → X a ⟶ B) (g : (a : α) → Y a ⟶ X a) [∀ (a : α), IsSplitEpi (g a)] [EffectiveEpiFamily X f] : EffectiveEpiFamilyStruct Y fun (a : α) => CategoryStruct.comp (g a) (f a)

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

instance CategoryTheory.instEffectiveEpiFamilyCompOfIsSplitEpi {C : Type u_1} [Category.{v_1, u_1} C] {α : Type u_2} {B : C} {X Y : α → C} (f : (a : α) → X a ⟶ B) (g : (a : α) → Y a ⟶ X a) [∀ (a : α), IsSplitEpi (g a)] [EffectiveEpiFamily X f] : EffectiveEpiFamily Y fun (a : α) => CategoryStruct.comp (g a) (f a)

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

noncomputable def CategoryTheory.effectiveEpiFamilyStructOfComp {C : Type u_2} [Category.{v_2, u_2} C] {I : Type u_3} {Z Y : I → C} {X : C} (g : (i : I) → Z i ⟶ Y i) (f : (i : I) → Y i ⟶ X) [EffectiveEpiFamily Z fun (i : I) => CategoryStruct.comp (g i) (f i)] [∀ (i : I), Epi (g i)] : 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.

theorem CategoryTheory.effectiveEpiFamily_of_effectiveEpi_epi_comp {C : Type u_1} [Category.{v_1, u_1} C] {α : Type u_2} {B : C} {X Y : α → C} (f : (a : α) → X a ⟶ B) (g : (a : α) → Y a ⟶ X a) [∀ (a : α), Epi (g a)] [EffectiveEpiFamily Y fun (a : α) => CategoryStruct.comp (g a) (f a)] : EffectiveEpiFamily X f

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

theorem CategoryTheory.effectiveEpiFamilyStructCompIso_aux {C : Type u_1} [Category.{v_1, u_1} C] {B 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₂), CategoryStruct.comp g₁ (CategoryStruct.comp (π a₁) i) = CategoryStruct.comp g₂ (CategoryStruct.comp (π a₂) i) → CategoryStruct.comp g₁ (e a₁) = CategoryStruct.comp g₂ (e a₂)) {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂) (hg : CategoryStruct.comp g₁ (π a₁) = CategoryStruct.comp g₂ (π a₂)) : CategoryStruct.comp g₁ (e a₁) = CategoryStruct.comp g₂ (e a₂)

noncomputable def CategoryTheory.effectiveEpiFamilyStructCompIso {C : Type u_1} [Category.{v_1, u_1} C] {B B' : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) (i : B ⟶ B') [EffectiveEpiFamily X π] [IsIso i] : EffectiveEpiFamilyStruct X fun (a : α) => CategoryStruct.comp (π a) i

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

instance CategoryTheory.instEffectiveEpiFamilyComp {C : Type u_1} [Category.{v_1, u_1} C] {B B' : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) (i : B ⟶ B') [EffectiveEpiFamily X π] [IsIso i] : EffectiveEpiFamily X fun (a : α) => CategoryStruct.comp (π a) i