The averaging idempotent of a root of one

Let A be a semiring that is a module over a semiring R in which the natural number n is invertible, and let υ : A satisfy υ ^ n = 1. Then (1 + υ + ⋯ + υ ^ (n - 1)) / n is idempotent: it is the averaging idempotent of the cyclic group generated by υ. For n = 3 this is the idempotent (1 + υ + υ²) / 3 of a cube root of one; for n = 2 it is the idempotent (1 + υ) / 2 of a square root of one, which over a commutative ring is TauCeti.halfOneAdd.

No compatibility between the R-action and the multiplication of A is assumed: ⅟n • x is pinned down as the unique y with n • y = x.

Main results

• TauCeti.isIdempotentElem_invOf_smul_geom_sum: (∑ i < n, υ ^ i) / n is idempotent when υ ^ n = 1.

theorem TauCeti.isIdempotentElem_invOf_smul_geom_sum (R : Type u_1) {A : Type u_2} [Semiring R] [Semiring A] [Module R A] {υ : A} {n : ℕ} [Invertible ↑n] (hυ : υ ^ n = 1) : IsIdempotentElem (⅟↑n • ∑ i ∈ Finset.range n, υ ^ i)

(1 + υ + ⋯ + υ ^ (n - 1)) / n is idempotent when υ ^ n = 1 and n is invertible: it is the averaging idempotent of the cyclic group generated by υ. Over a commutative ring, the case n = 2 is also TauCeti.isIdempotentElem_halfOneAdd.