descResidueField_fromSpecResidueField

English

For K a field and X a scheme, and f: stalk x → κ ⟦K⟧ with IsLocalHom, the composed map equals the other side: Spec.map (descResidueField f) ≫ X.fromSpecResidueField x = Spec.map f ≫ X.fromSpecStalk x.

Русский

Пусть K — поле, X — схема, f: stalk x → κ(K) с IsLocalHom. Тогда композиция совпадает: Spec.map (descResidueField f) ≫ X.fromSpecResidueField x = Spec.map f ≫ X.fromSpecStalk x.

LaTeX

$$Spec.map (X.descResidueField f) ≫ X.fromSpecResidueField x = Spec.map f ≫ X.fromSpecStalk x$$

Lean4

theorem descResidueField_fromSpecResidueField {K : Type*} [Field K] (X : Scheme) {x} (f : X.presheaf.stalk x ⟶ .of K)
    [IsLocalHom f.hom] : Spec.map (X.descResidueField f) ≫ X.fromSpecResidueField x = Spec.map f ≫ X.fromSpecStalk x :=
  by simp [fromSpecResidueField, ← Spec.map_comp_assoc]

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