descResidueField_stalkClosedPointTo_fromSpecResidueField

English

If K is a field and f: Spec(𝔽) ⟶ X, then the equality holds with stalkClosedPointTo and fromSpecResidueField.

Русский

Для поля K и отображения f: Spec(𝔽) ⟶ X равенство сохраняется с stalkClosedPointTo и fromSpecResidueField.

LaTeX

$$Spec.map (X.descResidueField (Scheme.stalkClosedPointTo f)) ≫ X.fromSpecResidueField (f.base (closedPoint K)) = f$$

Lean4

theorem descResidueField_stalkClosedPointTo_fromSpecResidueField (K : Type u) [Field K] (X : Scheme.{u})
    (f : Spec (.of K) ⟶ X) :
    Spec.map (@descResidueField (CommRingCat.of K) _ X _ (Scheme.stalkClosedPointTo f) _) ≫
        X.fromSpecResidueField (f.base (closedPoint K)) =
      f :=
  by
  rw [X.descResidueField_fromSpecResidueField]
  rw [Scheme.Spec_stalkClosedPointTo_fromSpecStalk]

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