Spec_map_residueFieldMap_fromSpecResidueField

English

If X is over Y, then the morphism Spec.map (X.residueFieldMap x) is an over morphism to Y for any x.

Русский

Если X над Y, то отображение Spec.map (X.residueFieldMap x) является morphism over Y для любого x.

LaTeX

$$Spec.map (X.residueFieldMap x) ≫ Y.fromSpecResidueField _ = ...$$

Lean4

@[reassoc (attr := simp)]
theorem Spec_map_residueFieldMap_fromSpecResidueField (x : X) :
    Spec.map (f.residueFieldMap x) ≫ Y.fromSpecResidueField _ = X.fromSpecResidueField x ≫ f :=
  by
  dsimp only [fromSpecResidueField]
  rw [Category.assoc, ← Spec_map_stalkMap_fromSpecStalk, ← Spec.map_comp_assoc, ← Spec.map_comp_assoc]
  rfl

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