instEffectiveEpiDescOfEffectiveEpiFamily

English

If HasCoproduct X and X π is an effective epi family, then Sigma.desc π is an effective epi map.

Русский

Если есть копродукт X и X π образует эффективное эпиморфное семейство, то Sigma.desc π является эффективной эпипропускной цепочкой.

LaTeX

$$$[\text{HasCoproduct} X] \wedge [\operatorname{EffectiveEpiFamily} X \pi] \Rightarrow \operatorname{EffectiveEpi}(\Sigma.\mathrm{desc}\,\pi)$$$

Lean4

instance {B : C} {α : Type*} (X : α → C) (π : (a : α) → (X a ⟶ B)) [HasCoproduct X] [EffectiveEpiFamily X π] :
    EffectiveEpi (Sigma.desc π) :=
  by
  let e := effectiveEpiStructIsColimitDescOfEffectiveEpiFamily X _ (coproductIsCoproduct _) π
  simp only [Cofan.mk_pt, coproductIsCoproduct, colimit.cocone_x, IsColimit.ofIsoColimit_desc, Cocones.ext_inv_hom,
    Iso.refl_inv, colimit.isColimit_desc, Category.id_comp] at e
  exact ⟨⟨e⟩⟩

Похожие утверждения