germ_stalkClosedPointTo_Spec_fromSpecStalk

English

A variant version of the germ-stalk compatibility with Spec.map φ and X.fromSpecStalk x, under IsLocalHom assumptions.

Русский

Вариант той же совместимости: germ-stalk с Spec.map φ и X.fromSpecStalk x при условии IsLocalHom.

LaTeX

$$$\\text{germ}_{U} \\; (\\mathrm{Spec.map}\\; f \\; \\gg \\; X.fromSpecStalk x) = \\text{germ}_{U}(x) \\; \\gg \\; f$$$

Lean4

@[reassoc]
theorem germ_stalkClosedPointTo_Spec_fromSpecStalk {x : X} (f : X.presheaf.stalk x ⟶ R) [IsLocalHom f.hom] (U : Opens X)
    (hU) :
    X.presheaf.germ U _ hU ≫ stalkClosedPointTo (Spec.map f ≫ X.fromSpecStalk x) =
      X.presheaf.germ U x (by simpa using hU) ≫ f :=
  by
  have : (Spec.map f ≫ X.fromSpecStalk x).base (closedPoint R) = x := by
    rw [comp_base_apply, Spec_closedPoint, fromSpecStalk_closedPoint]
  have : x ∈ U := this ▸ hU
  simp only [germ_stalkClosedPointTo, comp_app, fromSpecStalk_app (X := X) (x := x) this, Category.assoc, Iso.trans_hom,
    Functor.mapIso_hom, (Spec.map f).app_eq_appLE, Hom.appLE_map_assoc, Hom.map_appLE_assoc]
  simp_rw [← Opens.map_top (Spec.map f).base]
  rw [← (Spec.map f).app_eq_appLE, ΓSpecIso_naturality, Iso.inv_hom_id_assoc]

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