fromSpecStalk_toSpecΓ — Mathlib

English

The composition of the ΓSpecIso hom with the inverse of the stalkClosedPointIso inv equals the germ map at the closed point; equivalently, the two canonical isomorphisms align the algebraic and topological data at the closed point.

Русский

Сходимость ГΓSpecIso с обратной стороной stalkClosedPointIso равна гёрму в закрытой точке; канонические изоморфизмы согласованы на закрытой точке.

LaTeX

$$(Scheme.ΓSpecIso R).hom ≫ (stalkClosedPointIso R).inv = (Spec R).presheaf.germ ⊤ (closedPoint _) trivial$$

Lean4

@[reassoc]
theorem fromSpecStalk_toSpecΓ (X : Scheme.{u}) (x : X) :
    X.fromSpecStalk x ≫ X.toSpecΓ = Spec.map (X.presheaf.germ ⊤ x trivial) :=
  by
  rw [Scheme.toSpecΓ_naturality, ← SpecMap_ΓSpecIso_hom, ← Spec.map_comp, Scheme.fromSpecStalk_appTop]
  simp

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