map_map — Mathlib

English

If f: R → S and g: S → T are local homomorphisms, then the induced residue-field maps compose compatibly: map g (map f x) = map (g ∘ f) x.

Русский

Если f: R → S и g: S → T — локальные гомоморфизмы, то индуцированные отображения полей остатка композиционно совместимы: map g (map f x) = map (g ∘ f) x.

LaTeX

$$$ \\operatorname{map}_g (\\operatorname{map}_f x) = \\operatorname{map}_{g \\circ f} x $$$

Lean4

@[simp]
theorem map_map (f : R →+* S) (g : S →+* T) (x : ResidueField R) [IsLocalHom f] [IsLocalHom g] :
    map g (map f x) = map (g.comp f) x :=
  DFunLike.congr_fun (map_comp f g).symm x

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