The group algebra of a finite cyclic group: the powers of σ - 1

Let C be a finite cyclic group with generator σ, and let R be a ring. The powers (σ - 1) ^ i for 0 ≤ i < |C| form an R-basis of the group algebra R[C] (TauCeti.MonoidAlgebra.basisSubOnePow). When R is commutative, the coordinates of the value f(σ - 1) ∈ R[C] of a polynomial f of degree < |C| are the coefficients of f (basisSubOnePow_repr_aeval), so such an f is determined by f(σ - 1); in particular, if f(σ - 1) is a scalar multiple r • y, then r divides every coefficient of f (dvd_coeff_of_aeval_of_sub_one_eq_smul), and if f(σ - 1) = 0 then f = 0 (eq_zero_of_aeval_of_sub_one_eq_zero).

Consequently evaluation at σ - 1 presents the group algebra as a quotient of the polynomial ring: R[X] → R[C], X ↦ σ - 1, is surjective with kernel the principal ideal generated by (1 + X) ^ |C| - 1 (ker_aeval_of_sub_one), the polynomial vanishing at σ - 1 because σ ^ |C| = 1.

These coefficient and divisibility formulas supply the finite-level linear algebra used for the power-series coordinate ℤ_p⟦X⟧ ≅ ℤ_p[[Γ]] of an infinite procyclic profinite pro-p group Γ, and the kernel computation identifies the finite levels ℤ_p[Γ ⧸ U] of that coordinate.

Main declarations

• TauCeti.MonoidAlgebra.basisSubOnePow: the basis (σ - 1) ^ i, i < |C|, of R[C].
• TauCeti.MonoidAlgebra.basisSubOnePow_repr_aeval: the coordinates of f(σ - 1) are the coefficients of f, for deg f < |C|.
• TauCeti.MonoidAlgebra.dvd_coeff_of_aeval_of_sub_one_eq_smul: if f(σ - 1) = r • y with deg f < |C|, then r divides every coefficient of f.
• TauCeti.MonoidAlgebra.eq_zero_of_aeval_of_sub_one_eq_zero: if f(σ - 1) = 0 with deg f < |C|, then f = 0.
• TauCeti.MonoidAlgebra.aeval_of_sub_one_surjective, TauCeti.MonoidAlgebra.ker_aeval_of_sub_one: evaluation at σ - 1 is a surjection R[X] → R[C] with kernel ((1 + X) ^ |C| - 1).

theorem TauCeti.MonoidAlgebra.span_range_of_sub_one_pow_eq_top {R : Type u_1} {C : Type u_2} [Group C] [Finite C] {σ : C} [Ring R] (hσ : ∀ (x : C), x ∈ Subgroup.zpowers σ) : Submodule.span R (Set.range fun (i : Fin (Nat.card C)) => ((MonoidAlgebra.of R C) σ - 1) ^ ↑i) = ⊤

The powers (σ - 1) ^ i for i < |C| of a generator σ of a finite cyclic group C span the group algebra R[C].

theorem TauCeti.MonoidAlgebra.linearIndependent_of_sub_one_pow {R : Type u_1} {C : Type u_2} [Group C] [Finite C] {σ : C} [Ring R] (hσ : ∀ (x : C), x ∈ Subgroup.zpowers σ) : LinearIndependent R fun (i : Fin (Nat.card C)) => ((MonoidAlgebra.of R C) σ - 1) ^ ↑i

The powers (σ - 1) ^ i for i < |C| of a generator σ of a finite cyclic group C are linearly independent in the group algebra R[C].

noncomputable def TauCeti.MonoidAlgebra.basisSubOnePow {R : Type u_1} {C : Type u_2} [Group C] [Finite C] {σ : C} [Ring R] (hσ : ∀ (x : C), x ∈ Subgroup.zpowers σ) : Module.Basis (Fin (Nat.card C)) R (MonoidAlgebra R C)

The basis of powers of σ - 1. For a generator σ of a finite cyclic group C, the powers (σ - 1) ^ i with 0 ≤ i < |C| form an R-basis of the group algebra R[C].

Equations

• TauCeti.MonoidAlgebra.basisSubOnePow hσ = Module.Basis.mk ⋯ ⋯

@[simp]

theorem TauCeti.MonoidAlgebra.coe_basisSubOnePow {R : Type u_1} {C : Type u_2} [Group C] [Finite C] {σ : C} [Ring R] (hσ : ∀ (x : C), x ∈ Subgroup.zpowers σ) : ⇑(basisSubOnePow hσ) = fun (i : Fin (Nat.card C)) => ((MonoidAlgebra.of R C) σ - 1) ^ ↑i

theorem TauCeti.MonoidAlgebra.basisSubOnePow_repr_aeval {R : Type u_1} {C : Type u_2} [Group C] [Finite C] {σ : C} [CommRing R] (hσ : ∀ (x : C), x ∈ Subgroup.zpowers σ) {f : Polynomial R} (hf : f.degree < ↑(Nat.card C)) (i : Fin (Nat.card C)) : ((basisSubOnePow hσ).repr ((Polynomial.aeval ((MonoidAlgebra.of R C) σ - 1)) f)) i = f.coeff ↑i

The coordinates of f(σ - 1) in the basis of powers of σ - 1 are the coefficients of the polynomial f, when f has degree < |C|.

theorem TauCeti.MonoidAlgebra.dvd_coeff_of_aeval_of_sub_one_eq_smul {R : Type u_1} {C : Type u_2} [Group C] [Finite C] {σ : C} [CommRing R] (hσ : ∀ (x : C), x ∈ Subgroup.zpowers σ) {f : Polynomial R} (hf : f.degree < ↑(Nat.card C)) {r : R} {y : MonoidAlgebra R C} (h : (Polynomial.aeval ((MonoidAlgebra.of R C) σ - 1)) f = r • y) (i : ℕ) : r ∣ f.coeff i

If the value f(σ - 1) ∈ R[C] of a polynomial f of degree < |C| at σ - 1 is a scalar multiple r • y, then r divides every coefficient of f.

theorem TauCeti.MonoidAlgebra.eq_zero_of_aeval_of_sub_one_eq_zero {R : Type u_1} {C : Type u_2} [Group C] [Finite C] {σ : C} [CommRing R] (hσ : ∀ (x : C), x ∈ Subgroup.zpowers σ) {f : Polynomial R} (hf : f.degree < ↑(Nat.card C)) (h : (Polynomial.aeval ((MonoidAlgebra.of R C) σ - 1)) f = 0) : f = 0

A polynomial of degree < |C| vanishing at σ - 1 in R[C] is zero, for a generator σ of the finite cyclic group C.

theorem TauCeti.MonoidAlgebra.aeval_of_sub_one_one_add_X_pow_card_sub_one_eq_zero {R : Type u_1} {C : Type u_2} [Group C] [CommRing R] (σ : C) : (Polynomial.aeval ((MonoidAlgebra.of R C) σ - 1)) ((1 + Polynomial.X) ^ Nat.card C - 1) = 0

The polynomial (1 + X) ^ |C| - 1 vanishes at σ - 1 in the group algebra R[C] of a finite group C, because σ ^ |C| = 1.

theorem TauCeti.MonoidAlgebra.aeval_of_sub_one_surjective {R : Type u_1} {C : Type u_2} [Group C] [Finite C] {σ : C} [CommRing R] (hσ : ∀ (x : C), x ∈ Subgroup.zpowers σ) : Function.Surjective ⇑(Polynomial.aeval ((MonoidAlgebra.of R C) σ - 1))

Evaluation at σ - 1 is a surjection R[X] → R[C], for a generator σ of the finite cyclic group C.

theorem TauCeti.MonoidAlgebra.ker_aeval_of_sub_one {R : Type u_1} {C : Type u_2} [Group C] [Finite C] {σ : C} [CommRing R] (hσ : ∀ (x : C), x ∈ Subgroup.zpowers σ) : RingHom.ker (Polynomial.aeval ((MonoidAlgebra.of R C) σ - 1)) = Ideal.span {(1 + Polynomial.X) ^ Nat.card C - 1}

The group algebra of a finite cyclic group as a quotient of the polynomial ring. For a generator σ of the finite cyclic group C, the kernel of evaluation at σ - 1, R[X] → R[C], is the principal ideal generated by (1 + X) ^ |C| - 1.