residueFieldCongr_fromSpecResidueField

English

If h: x = y, then the map on residue fields induced by h composes with the fromSpecResidueField maps as in the displayed equality.

Русский

Если h: x = y, то отображение между остаточными полями, индуцированное h, компонуется с отображениями fromSpecResidueField так, как указано в следующем равенстве.

LaTeX

$$Spec.map (X.residueFieldCongr h).hom ≫ X.fromSpecResidueField x = X.fromSpecResidueField y$$

Lean4

@[reassoc (attr := simp)]
theorem residueFieldCongr_fromSpecResidueField {x y : X} (h : x = y) :
    Spec.map (X.residueFieldCongr h).hom ≫ X.fromSpecResidueField _ = X.fromSpecResidueField _ := by subst h; simp

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