English
For NeZero n, and an automorphism f, the image of autToPow under f equals the chosen root of unity image of μ.
Русский
Для не нуля n и автоморфизма f изображение autToPow при f равно выбранному образу μ в корнях единицы.
LaTeX
$$[NeZero n] (f : S ≃ₐ[R] S) : (autToPow R hμ f : ZMod n).val = (map_rootsOfUnity_eq_pow_self f hμ.toRootsOfUnity).choose$$
Lean4
/-- The `MonoidHom` that takes an automorphism to the power of `μ` that `μ` gets mapped to
under it. -/
noncomputable def autToPow [NeZero n] : (S ≃ₐ[R] S) →* (ZMod n)ˣ :=
let μ' := hμ.toRootsOfUnity
have ho : orderOf μ' = n := by
refine Eq.trans ?_ hμ.eq_orderOf.symm
rw [← hμ.val_toRootsOfUnity_coe, orderOf_units, Subgroup.orderOf_coe]
MonoidHom.toHomUnits
{ toFun := fun σ ↦ (map_rootsOfUnity_eq_pow_self σ.toAlgHom μ').choose
map_one' := by
generalize_proofs h1
have h := h1.choose_spec
replace h : μ' = μ' ^ h1.choose := rootsOfUnity.coe_injective (by simpa only [rootsOfUnity.coe_pow] using h)
nth_rw 1 [← pow_one μ'] at h
convert ho ▸ (ZMod.natCast_eq_natCast_iff ..).mpr (pow_eq_pow_iff_modEq.mp h).symm
exact Nat.cast_one.symm
map_mul' := by
intro x y
generalize_proofs hxy' hx' hy'
have hxy := hxy'.choose_spec
replace hxy : x (((μ' : Sˣ) : S) ^ hy'.choose) = ((μ' : Sˣ) : S) ^ hxy'.choose := hy'.choose_spec ▸ hxy
rw [map_pow] at hxy
replace hxy : (((μ' : Sˣ) : S) ^ hx'.choose) ^ hy'.choose = ((μ' : Sˣ) : S) ^ hxy'.choose :=
hx'.choose_spec ▸ hxy
rw [← pow_mul] at hxy
replace hxy : μ' ^ (hx'.choose * hy'.choose) = μ' ^ hxy'.choose :=
rootsOfUnity.coe_injective (by simpa only [rootsOfUnity.coe_pow] using hxy)
convert ho ▸ (ZMod.natCast_eq_natCast_iff ..).mpr (pow_eq_pow_iff_modEq.mp hxy).symm
exact (Nat.cast_mul ..).symm }
-- We are not using @[simps] in `autToPow` to avoid a timeout.
