autEquivRootsOfUnity_apply_rootOfSplit

English

For a field K with irreducible X^n − C a and a split field L, any automorphism σ of L over K sends the distinguished root to a scalar multiple by a root of unity: σ(root) = autEquivRootsOfUnity(hζ,H,L) σ · root.

Русский

Для поля K с ирредукцией X^n − C a и разворачивающего поля L, любой автоморфизм σ поля L над K отправляет выбранный корень в кратность корню единства: σ(root) = autEquivRootsOfUnity(hζ,H,L) σ · root.

LaTeX

$$$\sigma(\text{rootOfSplitsXPowSubC}(\mathrm{pos}\, n, a, L)) = \mathrm{autEquivRootsOfUnity}(hζ,H,L)\,σ\cdot \text{rootOfSplitsXPowSubC}(\mathrm{pos}\, n, a, L).$$$

Lean4

theorem autEquivRootsOfUnity_apply_rootOfSplit [NeZero n] (σ : L ≃ₐ[K] L) :
    σ (rootOfSplitsXPowSubC (NeZero.pos n) a L) =
      autEquivRootsOfUnity hζ H L σ • (rootOfSplitsXPowSubC (NeZero.pos n) a L) :=
  by
  obtain ⟨η, rfl⟩ := (autEquivRootsOfUnity hζ H L).symm.surjective σ
  rw [MulEquiv.apply_symm_apply, autEquivRootsOfUnity]
  simp only [MulEquiv.symm_trans_apply, AlgEquiv.autCongr_symm, AlgEquiv.symm_symm, MulEquiv.symm_symm,
    AlgEquiv.autCongr_apply, AlgEquiv.trans_apply, adjoinRootXPowSubCEquiv_symm_eq_root,
    autAdjoinRootXPowSubCEquiv_root, map_smul, adjoinRootXPowSubCEquiv_root]
  rfl

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