SpecToEquivOfLocalRing — Mathlib

English

Equivalence between Spec R ⟶ X and pairs (x, f) with x ∈ X and f: O_{X,x} ⟶ R a local ring homomorphism.

Русский

Эквалентность между морфизмами Spec R ⟶ X и парами (x, f) с x ∈ X и f: O_{X,x} ⟶ R локального кольца.

LaTeX

$$$\\mathrm{Spec\\toEquiv\\;local\\;ring} : (\\mathrm{Spec}\\ R \\to X) \\simeq \\Sigma x,\\{ f: \\mathcal O_{X,x} \\to R \\;|\\; \\mathrm{IsLocalHom} f\\}$$$

Lean4

/-- Given a local ring `R` and scheme `X`, morphisms `Spec R ⟶ X` corresponds to pairs
`(x, f)` where `x : X` and `f : 𝒪_{X, x} ⟶ R` is a local ring homomorphism.
-/
@[simps]
noncomputable def SpecToEquivOfLocalRing : (Spec R ⟶ X) ≃ Σ x, { f : X.presheaf.stalk x ⟶ R // IsLocalHom f.hom }
    where
  toFun f := ⟨f.base (closedPoint R), Scheme.stalkClosedPointTo f, inferInstance⟩
  invFun xf := Spec.map xf.2.1 ≫ X.fromSpecStalk xf.1
  left_inv := Scheme.Spec_stalkClosedPointTo_fromSpecStalk
  right_inv
    xf := by
    obtain ⟨x, ⟨f, hf⟩⟩ := xf
    symm
    refine SpecToEquivOfLocalRing_eq_iff.mpr ⟨?_, ?_⟩
    ·
      simp only [Scheme.comp_coeBase, TopCat.coe_comp, Function.comp_apply, Spec_closedPoint,
        Scheme.fromSpecStalk_closedPoint]
    · refine TopCat.Presheaf.stalk_hom_ext _ fun U hxU ↦ ?_
      simp only [Scheme.germ_stalkClosedPointTo_Spec_fromSpecStalk, TopCat.Presheaf.stalkCongr_hom,
        TopCat.Presheaf.germ_stalkSpecializes_assoc]

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