map — Mathlib

English

The coordinate ring map respects mk, i.e., mapping that mk W' x under map f corresponds to mk of the mapped x.

Русский

Координатное кольцо сопоставление сохраняет mk: отображение mk W' x через map f равно mk W'.map f (x.map).

LaTeX

$$map W' f (mk W' x) = mk (W'.map f) (x.map <| mapRingHom f)$$

Lean4

/-- The ring homomorphism `R[W] →+* S[W.map f]` induced by a ring homomorphism `f : R →+* S`. -/
noncomputable def map (f : R →+* S) : W'.CoordinateRing →+* (W'.map f).toAffine.CoordinateRing :=
  AdjoinRoot.lift ((AdjoinRoot.of _).comp <| mapRingHom f) ((AdjoinRoot.root (W'.map f).toAffine.polynomial)) <| by
    rw [← eval₂_map, ← map_polynomial, AdjoinRoot.eval₂_root]

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