English
The symmetric action on the root under σ corresponds to multiplying the root by the eigenvalue in Kˣ.
Русский
Симметричное действие на корень под σ соответствует умножению корня на собственное значение в Kˣ.
LaTeX
$$$\\text{symm smul relation for root}$$$
Lean4
/-- The equivalence between the roots of unity of `K` and `Gal(K[ⁿ√a]/K)`. -/
noncomputable def autAdjoinRootXPowSubCEquiv [NeZero n] : rootsOfUnity n K ≃* (K[n√a] ≃ₐ[K] K[n√a])
where
__ := autAdjoinRootXPowSubC n a
invFun := AdjoinRootXPowSubCEquivToRootsOfUnity hζ H
left_inv := by
intro η
have := Fact.mk H
have : IsDomain K[n√a] := inferInstance
letI : Algebra K K[n√a] := inferInstance
apply (rootsOfUnityEquivOfPrimitiveRoots (algebraMap K K[n√a]).injective hζ).injective
ext
simp only [AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, autAdjoinRootXPowSubC_root,
Algebra.smul_def, MulEquiv.apply_symm_apply, rootsOfUnity.val_mkOfPowEq_coe,
val_rootsOfUnityEquivOfPrimitiveRoots_apply_coe, AdjoinRootXPowSubCEquivToRootsOfUnity]
split_ifs with h
· obtain rfl := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) h
have : (η : Kˣ) = 1 := (pow_one _).symm.trans η.prop
simp only [this, Units.val_one, map_one]
· exact mul_div_cancel_right₀ _ (root_X_pow_sub_C_ne_zero' (NeZero.pos n) h)
right_inv := by
intro e
have := Fact.mk H
letI : Algebra K K[n√a] := inferInstance
apply AlgEquiv.coe_algHom_injective
apply AdjoinRoot.algHom_ext
simp only [AdjoinRootXPowSubCEquivToRootsOfUnity, AdjoinRoot.algebraMap_eq, OneHom.toFun_eq_coe,
MonoidHom.toOneHom_coe, AlgHom.coe_coe, autAdjoinRootXPowSubC_root, Algebra.smul_def]
rw [rootsOfUnityEquivOfPrimitiveRoots_symm_apply, rootsOfUnity.val_mkOfPowEq_coe]
split_ifs with h
· obtain rfl := not_imp_not.mp (fun hn ↦ ne_zero_of_irreducible_X_pow_sub_C' hn H) h
rw [(pow_one _).symm.trans (root_X_pow_sub_C_pow 1 a), one_mul, ← AdjoinRoot.algebraMap_eq, AlgEquiv.commutes]
· refine div_mul_cancel₀ _ (root_X_pow_sub_C_ne_zero' (NeZero.pos n) h)
