from_union_surjective_of_isColimit

English

If D is a colimit of F, then the canonical union map from the disjoint union of the indexed components to D.pt is surjective.

Русский

Если D — колимит функции F, то образующая карта объединения из дисъjoint множества к D.pt сюръективна.

LaTeX

$$$\\text{Surjective}\\,\\big(\\lambda a, D.ι.app a.1 a.2\\big)$$$

Lean4

theorem from_union_surjective_of_isColimit {D : Cocone F} (hD : IsColimit D) :
    let ff : (Σ j : J, ToType (F.obj j)) → ToType D.pt := fun a => D.ι.app a.1 a.2
    Function.Surjective ff :=
  by
  intro ff x
  let E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
  let hE : IsColimit E := isColimitOfPreserves (forget C) hD
  obtain ⟨j, y, hy⟩ := Types.jointly_surjective_of_isColimit hE x
  exact ⟨⟨j, y⟩, hy⟩

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