autAdjoinRootXPowSubC — Mathlib

English

The automorphism-induced homomorphism sends a root to the primitive action on the root, i.e., η ↦ η • root.

Русский

Гомоморфизм, вызываемый автоморфизмом, отправляет корень к действию умножения на корень: η ↦ η • корень.

LaTeX

$$$autAdjoinRootXPowSubCHom\\; η \\; (root) = η \\cdot root$$$

Lean4

/-- The natural embedding of the roots of unity of `K` into `Gal(K[ⁿ√a]/K)`, by sending
`η ↦ (ⁿ√a ↦ η • ⁿ√a)`. This is an isomorphism when `K` contains a primitive root of unity.
See `autAdjoinRootXPowSubCEquiv`. -/
noncomputable def autAdjoinRootXPowSubC : rootsOfUnity n K →* (K[n√a] ≃ₐ[K] K[n√a]) :=
  (AlgEquiv.algHomUnitsEquiv _ _).toMonoidHom.comp (autAdjoinRootXPowSubCHom n a).toHomUnits

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