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}
[Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(c : Limits.Cofan X)
(hc : Limits.IsColimit c)
(π : (a : α) → X a ⟶ B)
[EffectiveEpiFamily X π]
:
EffectiveEpiStruct (hc.desc (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.
Instances For
instance
CategoryTheory.instEffectiveEpiDescOfEffectiveEpiFamily
{C : Type u_1}
[Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[Limits.HasCoproduct X]
[EffectiveEpiFamily X π]
:
theorem
CategoryTheory.effectiveEpiFamilyStructOfEffectiveEpiDesc_aux
{C : Type u_1}
[Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
{X : α → C}
{π : (a : α) → X a ⟶ B}
[Limits.HasCoproduct X]
[∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), Limits.HasPullback g (Limits.Sigma.ι X a)]
[∀ {Z : C} (g : Z ⟶ ∐ X), Limits.HasCoproduct fun (a : α) => Limits.pullback g (Limits.Sigma.ι X a)]
[∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Limits.Sigma.desc fun (a : α) => Limits.pullback.fst g (Limits.Sigma.ι X a))]
{W : C}
{e : (a : α) → X a ⟶ W}
(h :
∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
CategoryStruct.comp g₁ (π a₁) = CategoryStruct.comp g₂ (π a₂) →
CategoryStruct.comp g₁ (e a₁) = CategoryStruct.comp g₂ (e a₂))
{Z : C}
{g₁ g₂ : Z ⟶ ∐ fun (b : α) => X b}
(hg : CategoryStruct.comp g₁ (Limits.Sigma.desc π) = CategoryStruct.comp g₂ (Limits.Sigma.desc π))
:
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}
[Category.{u_3, u_1} C]
{B : C}
{α : Type u_2}
(X : α → C)
(π : (a : α) → X a ⟶ B)
[Limits.HasCoproduct X]
[EffectiveEpi (Limits.Sigma.desc π)]
[∀ {Z : C} (g : Z ⟶ ∐ X) (a : α), Limits.HasPullback g (Limits.Sigma.ι X a)]
[∀ {Z : C} (g : Z ⟶ ∐ X), Limits.HasCoproduct fun (a : α) => Limits.pullback g (Limits.Sigma.ι X a)]
[∀ {Z : C} (g : Z ⟶ ∐ X), Epi (Limits.Sigma.desc fun (a : α) => Limits.pullback.fst g (Limits.Sigma.ι X a))]
:
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.