glueMorphismsOfLocallyDirected — Mathlib

Lean4

/-- If `𝒰` is a directed open cover of `X`, to glue morphisms `{gᵢ : 𝒰ᵢ ⟶ Y}` it suffices
to check compatibility with the transition maps.
See `OpenCover.isColimitCoconeOfLocallyDirected` for this result stated in the language of
colimits.
-/
def glueMorphismsOfLocallyDirected (𝒰 : X.OpenCover) [Category 𝒰.I₀] [𝒰.LocallyDirected] {Y : Scheme.{u}}
    (g : ∀ i, 𝒰.X i ⟶ Y) (h : ∀ {i j : 𝒰.I₀} (hij : i ⟶ j), 𝒰.trans hij ≫ g j = g i) : X ⟶ Y :=
  𝒰.glueMorphisms g <| fun i j ↦ by
    apply (𝒰.intersectionOfLocallyDirected i j).hom_ext
    intro k
    simp [h]

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