glue — Mathlib

English

If S is MV and P satisfies the sheaf condition, then there is a defined glue element in P(op S.X4) glueing u ∈ P(op S.X2) and v ∈ P(op S.X3) with huv equality.

Русский

Если S — MV квадрат, а P удовлетворяет условиюsheaf, то существует элемент glue в P(op S.X4), склеивающий u ∈ P(op S.X2) и v ∈ P(op S.X3) при условии huv.

LaTeX

$$$\text{glue} : P(\mathrm{op}\,S.X_4)\quad\text{with}\quad P.map S.f_{12}.op\,u = ?,\; P.map S.f_{13}.op\,v = ?$$$

Lean4

/-- If `S` is a Mayer-Vietoris square, and `P` is a presheaf
which satisfies the sheaf condition with respect to `S`, then
elements of `P` over `S.X₂` and `S.X₃` can be glued if the
coincide over `S.X₁`. -/
noncomputable def glue : P.obj (op S.X₄) :=
  (PullbackCone.IsLimit.equivPullbackObj h.isLimit).symm ⟨⟨u, v⟩, huv⟩

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