map_comp_residue — Mathlib

English

Let R and S be local rings and f: R → S a local homomorphism. The induced map on residue fields commutes with the residue maps: the residue-field map composed with the residue map from R equals the residue map from S composed with f.

Русский

Пусть R и S — локальные кольца, f: R → S — локальный гомоморфизм. Индуцированная карта между полями остатка согласуется с тождественными отображениями: отображение поля остатка, применённое к резидууму от R, равно резидууму от S после применения f.

LaTeX

$$$ (\\operatorname{ResidueField.map} f) \\circ (\\operatorname{residue} R) = (\\operatorname{residue} S) \\circ f $$$

Lean4

theorem map_comp_residue (f : R →+* S) [IsLocalHom f] : (ResidueField.map f).comp (residue R) = (residue S).comp f :=
  rfl

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