residueFieldMap_comp — Mathlib

English

Composition of residue field maps along a composition of morphisms equals the residue field map of the composition.

Русский

Сложение карт поля остатка вдоль композиции морфизмов равняется карте поля остатка композиции.

LaTeX

$$$$ \mathrm{Hom.residueFieldMap}(\,f, g\,)(x) = g.\mathrm{residueFieldMap}(f.\mathrm{base}(x)) \circ f.\mathrm{residueFieldMap}(x). $$$$

Lean4

@[simp]
theorem residueFieldMap_comp {Z : Scheme.{u}} (g : Y ⟶ Z) (x : X) :
    (f ≫ g).residueFieldMap x = g.residueFieldMap (f.base x) ≫ f.residueFieldMap x :=
  LocallyRingedSpace.residueFieldMap_comp _ _ _

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