isoSpec_hom_base_apply — Mathlib

English

For a point x in U, the base map of hU.isoSpec.hom at x is the germ map from the local ring of X at x; more precisely, hU.isoSpec.hom.base x equals the base map induced by the germ map.

Русский

Для точки x в U основание отображения hU.isoSpec.hom в точке x задаётся через локальную структуру кольца в точке x: hU.isoSpec.hom.base x равняется базовому отображению, индуцированному germ-отображением.

LaTeX

$$hU.isoSpec.hom.base x = (Spec.map (X.presheaf.germ U x x.2)).base (closedPoint _)$$

Lean4

theorem isoSpec_hom_base_apply (x : U) :
    hU.isoSpec.hom.base x = (Spec.map (X.presheaf.germ U x x.2)).base (closedPoint _) :=
  by
  dsimp [IsAffineOpen.isoSpec_hom, Scheme.isoSpec_hom, Scheme.toSpecΓ_base, Scheme.Opens.toSpecΓ]
  rw [← Scheme.comp_base_apply, ← Spec.map_comp,
    (Iso.eq_comp_inv _).mpr (Scheme.Opens.germ_stalkIso_hom U (V := ⊤) x trivial), X.presheaf.germ_res_assoc,
    Spec.map_comp, Scheme.comp_base_apply]
  congr 1
  exact IsLocalRing.comap_closedPoint (U.stalkIso x).inv.hom

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