Effective epimorphic families and coproducts

This file proves that an effective epimorphic family induces an effective epi from the coproduct if the coproduct exists, and the converse under some more conditions on the coproduct (that it interacts well with pullbacks).

noncomputable def CategoryTheory.effectiveEpiStructIsColimitDescOfEffectiveEpiFamily {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (c : CategoryTheory.Limits.Cofan X) (hc : CategoryTheory.Limits.IsColimit c) (π : (a : α) → X a ⟶ B) [CategoryTheory.EffectiveEpiFamily X π] : CategoryTheory.EffectiveEpiStruct (hc.desc (CategoryTheory.Limits.Cofan.mk B π))

Given an EffectiveEpiFamily X π and a corresponding coproduct cocone, the family descends to an EffectiveEpi from the coproduct.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.effectiveEpiStructDescOfEffectiveEpiFamily {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.EffectiveEpiFamily X π] : CategoryTheory.EffectiveEpiStruct (CategoryTheory.Limits.Sigma.desc π)

Given an EffectiveEpiFamily X π such that the coproduct of X exists, Sigma.desc π is an EffectiveEpi.

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.instEffectiveEpiDescOfEffectiveEpiFamily {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.EffectiveEpiFamily X π] : CategoryTheory.EffectiveEpi (CategoryTheory.Limits.Sigma.desc π)

Equations

• ⋯ = ⋯

theorem CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc_aux {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} {X : α → C} {π : (a : α) → X a ⟶ B} [CategoryTheory.Limits.HasCoproduct X] [∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), CategoryTheory.Limits.HasPullback g (CategoryTheory.Limits.Sigma.ι X a)] [∀ {Z : C} (g : Z ⟶ ∐ X), CategoryTheory.Limits.HasCoproduct fun (a : α) => CategoryTheory.Limits.pullback g (CategoryTheory.Limits.Sigma.ι X a)] [∀ {Z : C} (g : Z ⟶ ∐ X), CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc fun (a : α) => CategoryTheory.Limits.pullback.fst g (CategoryTheory.Limits.Sigma.ι X a))] {W : C} {e : (a : α) → X a ⟶ W} (h : ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂), CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) → CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) {Z : C} {g₁ : Z ⟶ ∐ fun (b : α) => X b} {g₂ : Z ⟶ ∐ fun (b : α) => X b} (hg : CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Sigma.desc π) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Sigma.desc π)) : CategoryTheory.CategoryStruct.comp g₁ (CategoryTheory.Limits.Sigma.desc e) = CategoryTheory.CategoryStruct.comp g₂ (CategoryTheory.Limits.Sigma.desc e)

This is an auxiliary lemma used twice in the definition of EffectiveEpiFamilyOfEffectiveEpiDesc. It is the h hypothesis of EffectiveEpi.desc and EffectiveEpi.fac. 

noncomputable def CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] {B : C} {α : Type u_2} (X : α → C) (π : (a : α) → X a ⟶ B) [CategoryTheory.Limits.HasCoproduct X] [CategoryTheory.EffectiveEpi (CategoryTheory.Limits.Sigma.desc π)] [∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), CategoryTheory.Limits.HasPullback g (CategoryTheory.Limits.Sigma.ι X a)] [∀ {Z : C} (g : Z ⟶ ∐ X), CategoryTheory.Limits.HasCoproduct fun (a : α) => CategoryTheory.Limits.pullback g (CategoryTheory.Limits.Sigma.ι X a)] [∀ {Z : C} (g : Z ⟶ ∐ X), CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc fun (a : α) => CategoryTheory.Limits.pullback.fst g (CategoryTheory.Limits.Sigma.ι X a))] : CategoryTheory.EffectiveEpiFamilyStruct X π

If a coproduct interacts well enough with pullbacks, then a family whose domains are the terms of the coproduct is effective epimorphic whenever Sigma.desc induces an effective epimorphism from the coproduct itself.

Equations

• One or more equations did not get rendered due to their size.