The roots of unity are preserved by an action by monoid endomorphisms

A monoid G acting on Mˣ by monoid endomorphisms preserves ζ ^ n = 1, so the subgroup rootsOfUnity n M is G-stable and inherits the action. This file records that stability and installs the inherited MulDistribMulAction.

The intended instance is the absolute Galois group acting on μₙ ⊆ (Kˢ)ˣ, where the action is in general nontrivial and is exactly what the Kummer isomorphism depends on; the statement needs nothing about fields, so it is proved for an arbitrary action by monoid endomorphisms.

Main results

• TauCeti.smul_mem_rootsOfUnity: rootsOfUnity n M is stable under the action.
• TauCeti.rootsOfUnity.mulDistribMulAction: the inherited action on rootsOfUnity n M.

theorem TauCeti.smul_mem_rootsOfUnity {G : Type u_1} {M : Type u_2} [Monoid G] [CommMonoid M] [MulDistribMulAction G Mˣ] {n : ℕ} (g : G) {ζ : Mˣ} (hζ : ζ ∈ rootsOfUnity n M) : g • ζ ∈ rootsOfUnity n M

An action by monoid endomorphisms preserves the n-th roots of unity.

@[instance_reducible]

instance TauCeti.rootsOfUnity.mulDistribMulAction {G : Type u_1} {M : Type u_2} [Monoid G] [CommMonoid M] [MulDistribMulAction G Mˣ] (n : ℕ) : MulDistribMulAction G ↥(rootsOfUnity n M)

The action of G on rootsOfUnity n M inherited from its action on Mˣ.

Equations

• TauCeti.rootsOfUnity.mulDistribMulAction n = { smul := fun (g : G) (ζ : ↥(rootsOfUnity n M)) => ⟨g • ↑ζ, ⋯⟩, mul_smul := ⋯, one_smul := ⋯, smul_one := ⋯, smul_mul := ⋯ }

@[simp]

theorem TauCeti.rootsOfUnity.coe_smul {G : Type u_1} {M : Type u_2} [Monoid G] [CommMonoid M] [MulDistribMulAction G Mˣ] (n : ℕ) (g : G) (ζ : ↥(rootsOfUnity n M)) : ↑(g • ζ) = g • ↑ζ