Lean4
/-- Given an open cover of `X`, and a morphism `𝒰.X x ⟶ Y` for each open subscheme in the cover,
such that these morphisms are compatible in the intersection (pullback), we may glue the morphisms
together into a morphism `X ⟶ Y`.
Note:
If `X` is exactly (defeq to) the gluing of `U i`, then using `Multicoequalizer.desc` suffices.
-/
def glueMorphisms (𝒰 : OpenCover.{v} X) {Y : Scheme.{u}} (f : ∀ x, 𝒰.X x ⟶ Y)
(hf : ∀ x y, pullback.fst (𝒰.f x) (𝒰.f y) ≫ f x = pullback.snd _ _ ≫ f y) : X ⟶ Y :=
by
refine inv 𝒰.ulift.fromGlued ≫ ?_
fapply Multicoequalizer.desc
· exact fun i ↦ f _
rintro ⟨i, j⟩
dsimp
change pullback.fst _ _ ≫ f _ = (_ ≫ _) ≫ f _
simpa [pullbackSymmetry_hom_comp_fst] using hf _ _