English
For a primitive root μ and a ring automorphism g, the automorphism-to-power map equals the cyclotomic character: hμ.autToPow R g = χ₀ n g.
Русский
Для примитивного корня μ и кольцевого автоморфизма g отображение автоморфизм→степень равняется циклотомическому символу: hμ.autToPow = χ₀.
LaTeX
$$$h_{\\mu}.autToPow(R,g) = χ_{0}(n,g)$$$
Lean4
/-- The relationship between `IsPrimitiveRoot.autToPow` and
`modularCyclotomicCharacter`. Note that `IsPrimitiveRoot.autToPow`
needs an explicit root of unity, and also an auxiliary "base ring" `R`. -/
theorem autToPow_eq_modularCyclotomicCharacter (n : ℕ) [NeZero n] (R : Type*) [CommRing R] [Algebra R L] {μ : L}
(hμ : IsPrimitiveRoot μ n) (g : L ≃ₐ[R] L) :
hμ.autToPow R g = modularCyclotomicCharacter L hμ.card_rootsOfUnity g :=
by
ext
apply ZMod.val_injective
apply hμ.pow_inj (ZMod.val_lt _) (ZMod.val_lt _)
simpa only [autToPow_spec R hμ g, modularCyclotomicCharacter, RingEquiv.toMulEquiv_eq_coe,
MulEquiv.toMonoidHom_eq_coe, modularCyclotomicCharacter', MonoidHom.coe_comp, MonoidHom.coe_coe,
Function.comp_apply, Units.coe_mapEquiv, MonoidHom.coe_toHomUnits, MonoidHom.coe_mk, OneHom.coe_mk,
RingEquiv.coe_toMulEquiv, ZMod.ringEquivCongr_val, AlgEquiv.coe_ringEquiv] using
modularCyclotomicCharacter.toFun_spec'' g hμ
