English
The symmetry of the equivalence gives that the inverse mapping sends the root to the canonical root.
Русский
Симметрия эквивалентности даёт, что обратное отображение переведёт корень к каноническому корню.
LaTeX
$$$(autAdjoinRootXPowSubCEquiv\\; hζ\\; H)^{\\mathrm{symm}}(α) = \\mathrm{root}$$$
Lean4
/-- The inverse function of `autAdjoinRootXPowSubC` if `K` has all roots of unity.
See `autAdjoinRootXPowSubCEquiv`. -/
noncomputable def AdjoinRootXPowSubCEquivToRootsOfUnity [NeZero n] (σ : K[n√a] ≃ₐ[K] K[n√a]) : rootsOfUnity n K :=
letI := Fact.mk H
letI : IsDomain K[n√a] := inferInstance
letI := Classical.decEq K
(rootsOfUnityEquivOfPrimitiveRoots (n := n) (algebraMap K K[n√a]).injective hζ).symm
(rootsOfUnity.mkOfPowEq (if a = 0 then 1 else σ (root _) / root _)
(by
-- The if is needed in case `n = 1` and `a = 0` and `K[n√a] = K`.
split
· exact one_pow _
rw [div_pow, ← map_pow]
simp only [root_X_pow_sub_C_pow, ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]
rw [div_self]
rwa [Ne, map_eq_zero_iff _ (algebraMap K _).injective]))
