English
If there exists a forgetful functor into Type that preserves the relevant multi-span colimits and the required limits, then every element of the glued object is obtained from some leg of the glue data.
Русский
Пусть существует забывающий функтор в Type, сохраняющий соответствующие мульти-пределы и требуемые пределы; тогда каждый элемент склеенного объекта получается как образ некоторого компонента склейки.
LaTeX
$$$\forall x:\, F(D.glued),\; \exists i: D.J,\; \exists y:\, F.obj(D.U(i)),\; F.map(D.\u03b7 i)\, y = x$$$
Lean4
/-- If there is a forgetful functor into `Type` that preserves enough (co)limits, then `D.ι` will
be jointly surjective. -/
theorem ι_jointly_surjective (F : C ⥤ Type v) [PreservesColimit D.diagram.multispan F]
[∀ i j k : D.J, PreservesLimit (cospan (D.f i j) (D.f i k)) F] (x : F.obj D.glued) :
∃ (i : _) (y : F.obj (D.U i)), F.map (D.ι i) y = x :=
by
let e := D.gluedIso F
obtain ⟨i, y, eq⟩ := (D.mapGlueData F).types_ι_jointly_surjective (e.hom x)
replace eq := congr_arg e.inv eq
change ((D.mapGlueData F).ι i ≫ e.inv) y = (e.hom ≫ e.inv) x at eq
rw [e.hom_inv_id, D.ι_gluedIso_inv] at eq
exact ⟨i, y, eq⟩
