The norm of 1 + x under an action of a group of prime order

Let a finite group G act on a commutative semiring R by semiring automorphisms. Expanding the product ∏_{g ∈ G} (1 + g • x) gives the sum, over all subsets S ⊆ G, of the products ∏_{h ∈ S} h • x. The empty subset contributes 1, the full subset contributes the "norm" ∏_{g} g • x, and G permutes the remaining subsets by translation. When G has prime order, every nonempty proper subset has trivial stabilizer, so the sum over each orbit of subsets is the "trace" ∑_{g} g • z of the product z attached to any one of its members; the singletons form one such orbit, with trace ∑_{g} g • x. Collecting the orbits of the subsets with at least two elements gives

∏_{g} (1 + g • x) = 1 + ∑_{g} g • x + ∑_{g} g • y + ∏_{g} g • x

for an element y of the square of the ideal generated by the orbit of x.

This is the identity behind the computation of the norm on the unit filtration of a cyclic extension of local fields of prime degree (Serre, Local Fields, Chapter V, §3, Lemma 5): there x lies in a power 𝓂^m of the maximal ideal, so y lies in 𝓂^(2m), and the valuations of the two traces are read off from the behaviour of the trace on powers of the maximal ideal.

Main results

• TauCeti.MulSemiringAction.prod_smul_finset_smul: translating a subset of G acts on the attached product of conjugates by the translating element.
• TauCeti.MulSemiringAction.prod_smul_mem_span_orbit_sq_of_one_lt_card: the product attached to a subset with at least two elements lies in the square of the ideal generated by the orbit.
• TauCeti.MulSemiringAction.exists_prod_one_add_smul_eq_of_prime_card: the expansion above.

References

• J.-P. Serre, Local Fields, Chapter V, §3, Lemma 5.

theorem TauCeti.MulSemiringAction.prod_smul_finset_smul {G : Type u_1} {R : Type u_2} [Group G] [CommSemiring R] [MulSemiringAction G R] [DecidableEq G] (g : G) (S : Finset G) (x : R) : ∏ h ∈ g • S, h • x = g • ∏ h ∈ S, h • x

Translating a finite subset S of the acting group by g acts on the product ∏_{h ∈ S} h • x of the corresponding conjugates of x by g.

theorem TauCeti.MulSemiringAction.prod_smul_mem_span_orbit_sq_of_one_lt_card {G : Type u_1} {R : Type u_2} [Group G] [CommSemiring R] [MulSemiringAction G R] {S : Finset G} (hS : 1 < S.card) (x : R) : ∏ h ∈ S, h • x ∈ Ideal.span (MulAction.orbit G x) ^ 2

The product of the conjugates of x indexed by a subset of the acting group with at least two elements lies in the square of the ideal generated by the orbit of x.

theorem TauCeti.MulSemiringAction.exists_prod_one_add_smul_eq_of_prime_card (G : Type u_1) {R : Type u_2} [Group G] [CommSemiring R] [MulSemiringAction G R] [Fintype G] (hG : Nat.Prime (Nat.card G)) (x : R) : ∃ y ∈ Ideal.span (MulAction.orbit G x) ^ 2, ∏ g : G, (1 + g • x) = 1 + ∑ g : G, g • x + ∑ g : G, g • y + ∏ g : G, g • x

The product ∏_{g} (1 + g • x) for a group of prime order. If G is a group of prime order acting on a commutative semiring R by semiring automorphisms, then

∏_{g} (1 + g • x) = 1 + ∑_{g} g • x + ∑_{g} g • y + ∏_{g} g • x

for some y in the square of the ideal generated by the orbit of x. The element y is the sum, over a set of representatives of the translation orbits of the subsets of G with at least two elements other than G itself, of the products of the conjugates of x indexed by the subset.