The group algebra of the cyclic group of order two

Let C₂ = Multiplicative (ZMod 2), generated by σ = Multiplicative.ofAdd 1. Over a commutative ring R, every element of the group algebra R[C₂] is a + bσ for unique coefficients a, b, and σ² = 1. The two characters of C₂, trivial and sign, assemble into the R-algebra homomorphism R[C₂] → R × R, a + bσ ↦ (a + b, a - b).

• When 2 is invertible in R, this map is an isomorphism R[C₂] ≃ₐ[R] R × R, with inverse (x, y) ↦ ⅟2 (x + y) + ⅟2 (x - y) σ; the two idempotents ⅟2 (1 ± σ) are the preimages of (1, 0) and (0, 1), and they split R[C₂] into the two eigenspaces of the involution σ.
• When R has no zero divisors and 2 is not a unit of R, there is no such splitting: the only idempotents of R[C₂] are 0 and 1.

Main declarations

• TauCeti.cyclicTwoSign: the sign character Multiplicative (ZMod 2) →* R.
• MonoidAlgebra.cyclicTwoToProd: the algebra homomorphism R[C₂] →ₐ[R] R × R.
• MonoidAlgebra.cyclicTwoEquivProd: the isomorphism R[C₂] ≃ₐ[R] R × R when 2 is invertible in R.
• MonoidAlgebra.isIdempotentElem_cyclicTwo_iff: over a ring without zero divisors in which 2 is not a unit, an element of R[C₂] is idempotent if and only if it is 0 or 1.

References

The ring ℤ₂[C₂] is the coefficient ring of the completed group algebra ℤ₂[[C₂ × ℤ₂]] ≅ ℤ₂[C₂][[T]] in which J. Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967), §4, p. 122, treats the even-rank Demushkin groups with q = 2. Labute works integrally over ℤ₂; the splitting after inverting 2 and the absence of an integral splitting recorded here are related facts about that coefficient ring, specialised to ℚ₂ and ℤ₂ in TauCeti.NumberTheory.Padics.GroupAlgebra.CyclicTwo.

def TauCeti.cyclicTwoSign (R : Type u_1) [Monoid R] [HasDistribNeg R] : Multiplicative (ZMod 2) →* R

The sign character of the cyclic group of order two, Multiplicative (ZMod 2) →* R, sending the generator Multiplicative.ofAdd 1 to -1.

Equations

• TauCeti.cyclicTwoSign R = { toFun := fun (g : Multiplicative (ZMod 2)) => (-1) ^ (Multiplicative.toAdd g).val, map_one' := ⋯, map_mul' := ⋯ }

theorem TauCeti.cyclicTwoSign_apply (R : Type u_1) [Monoid R] [HasDistribNeg R] (g : Multiplicative (ZMod 2)) : (cyclicTwoSign R) g = (-1) ^ (Multiplicative.toAdd g).val

@[simp]

theorem TauCeti.cyclicTwoSign_ofAdd_one (R : Type u_1) [Monoid R] [HasDistribNeg R] : (cyclicTwoSign R) (Multiplicative.ofAdd 1) = -1

theorem TauCeti.one_ne_ofAdd_one : 1 ≠ Multiplicative.ofAdd 1

theorem TauCeti.ofAdd_one_mul_ofAdd_one : Multiplicative.ofAdd 1 * Multiplicative.ofAdd 1 = 1

The generator σ = Multiplicative.ofAdd 1 of C₂ squares to 1.

theorem MonoidAlgebra.eq_single_one_add_single_ofAdd_one {R : Type u_1} [Semiring R] (x : MonoidAlgebra R (Multiplicative (ZMod 2))) : x = single 1 (x.coeff 1) + single (Multiplicative.ofAdd 1) (x.coeff (Multiplicative.ofAdd 1))

Every element of R[C₂] is a + bσ, where a and b are its coefficients at 1 and at the generator σ = Multiplicative.ofAdd 1.

theorem MonoidAlgebra.single_one_add_single_ofAdd_one_mul {R : Type u_1} [Semiring R] (a b a' b' : R) : (single 1 a + single (Multiplicative.ofAdd 1) b) * (single 1 a' + single (Multiplicative.ofAdd 1) b') = single 1 (a * a' + b * b') + single (Multiplicative.ofAdd 1) (a * b' + b * a')

The product of two elements of R[C₂] written as a + bσ: since σ² = 1, (a + bσ)(a' + b'σ) = (aa' + bb') + (ab' + ba')σ.

noncomputable def MonoidAlgebra.cyclicTwoToProd (R : Type u_1) [CommRing R] : MonoidAlgebra R (Multiplicative (ZMod 2)) →ₐ[R] R × R

The R-algebra homomorphism R[C₂] → R × R whose two components are the trivial and the sign character of C₂: it sends a + bσ to (a + b, a - b).

Equations

• MonoidAlgebra.cyclicTwoToProd R = (MonoidAlgebra.lift R (R × R) (Multiplicative (ZMod 2))) (MonoidHom.prod 1 (TauCeti.cyclicTwoSign R))

@[simp]

theorem MonoidAlgebra.cyclicTwoToProd_single (R : Type u_1) [CommRing R] (g : Multiplicative (ZMod 2)) (r : R) : (cyclicTwoToProd R) (single g r) = (r, r * (TauCeti.cyclicTwoSign R) g)

The trivial and sign characters send the monomial r·g to (r, r · sign g).

theorem MonoidAlgebra.cyclicTwoToProd_single_one_add_single_ofAdd_one (R : Type u_1) [CommRing R] (a b : R) : (cyclicTwoToProd R) (single 1 a + single (Multiplicative.ofAdd 1) b) = (a + b, a - b)

The trivial and sign characters send a + bσ to (a + b, a - b), computing cyclicTwoToProd from the coefficients in the basis (1, σ).

theorem MonoidAlgebra.cyclicTwoToProd_apply (R : Type u_1) [CommRing R] (x : MonoidAlgebra R (Multiplicative (ZMod 2))) : (cyclicTwoToProd R) x = (x.coeff 1 + x.coeff (Multiplicative.ofAdd 1), x.coeff 1 - x.coeff (Multiplicative.ofAdd 1))

The trivial and sign characters send an element of R[C₂] to the sum and difference of its coefficients at 1 and at the generator σ = Multiplicative.ofAdd 1.

noncomputable def MonoidAlgebra.cyclicTwoEquivProd (R : Type u_1) [CommRing R] [Invertible 2] : MonoidAlgebra R (Multiplicative (ZMod 2)) ≃ₐ[R] R × R

When 2 is invertible in R, the trivial and the sign character identify R[C₂] with R × R. The inverse sends (x, y) to ⅟2 (x + y) + ⅟2 (x - y) σ; in particular the two idempotents ⅟2 (1 ± σ) are the preimages of (1, 0) and (0, 1).

Equations

• MonoidAlgebra.cyclicTwoEquivProd R = AlgEquiv.ofBijective (MonoidAlgebra.cyclicTwoToProd R) ⋯

@[simp]

theorem MonoidAlgebra.cyclicTwoEquivProd_apply (R : Type u_1) [CommRing R] [Invertible 2] (x : MonoidAlgebra R (Multiplicative (ZMod 2))) : (cyclicTwoEquivProd R) x = (cyclicTwoToProd R) x

@[simp]

theorem MonoidAlgebra.cyclicTwoEquivProd_symm_apply (R : Type u_1) [CommRing R] [Invertible 2] (z : R × R) : (cyclicTwoEquivProd R).symm z = single 1 (⅟2 * (z.1 + z.2)) + single (Multiplicative.ofAdd 1) (⅟2 * (z.1 - z.2))

The inverse sends (x, y) to ⅟2 (x + y) + ⅟2 (x - y) σ, recovering the two coefficients from the trivial and sign character values.

theorem MonoidAlgebra.isIdempotentElem_cyclicTwo_iff (R : Type u_1) [CommRing R] [NoZeroDivisors R] (h₂ : ¬IsUnit 2) {e : MonoidAlgebra R (Multiplicative (ZMod 2))} : IsIdempotentElem e ↔ e = 0 ∨ e = 1

Over a ring R without zero divisors in which 2 is not a unit, the group algebra R[C₂] has no nontrivial idempotents: an element is idempotent if and only if it is 0 or 1. In particular R[C₂] admits no direct-product decomposition, in contrast with cyclicTwoEquivProd when 2 is invertible.