basicOpen_hom_ext — Mathlib

English

Two morphisms into Spec s how to ext with respect to a basic open; uniqueness of glueing along basic opens.

Русский

Два морфизма в Spec объясняются через базовые открытые: единство продолжений по базовым открытым.

LaTeX

$$$\text{basicOpen_hom_ext}$$$

Lean4

theorem basicOpen_hom_ext {X : RingedSpace.{u}} {R : CommRingCat.{u}} {α β : X ⟶ Spec.sheafedSpaceObj R}
    (w : α.base = β.base)
    (h :
      ∀ r : R,
        let U := PrimeSpectrum.basicOpen r
        (toOpen R U ≫ α.c.app (op U)) ≫ X.presheaf.map (eqToHom (by rw [w])) = toOpen R U ≫ β.c.app (op U)) :
    α = β := by
  ext : 1
  · exact w
  · apply ((TopCat.Sheaf.pushforward _ β.base).obj X.sheaf).hom_ext _ PrimeSpectrum.isBasis_basic_opens
    intro r
    apply (StructureSheaf.to_basicOpen_epi R r).1
    simpa using h r

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