Torsion in a character group

The group algebra of a group with torsion cannot be both reduced and connected over a field. For torsion of order equal to the characteristic, the group algebra contains the familiar nonzero nilpotent g - 1. For torsion of order prime to the characteristic, averaging over the finite cyclic subgroup produces a nontrivial idempotent.

Consequently, if the group algebra of a commutative group is reduced and has connected prime spectrum, then the group is torsion-free. This is the algebraic input that distinguishes tori from general groups of multiplicative type.

Both hypotheses are needed. In exponential characteristic p the p-th power map of a monoid algebra indexed by a p-torsion monoid is the p-th power of its counit, so every element differs from a scalar by a p-nilpotent, and over a coefficient ring with connected prime spectrum the monoid algebra again has connected prime spectrum, however much p-torsion the monoid carries. The coordinate Hopf algebra of μ_p in characteristic p is the standard instance: connected, not reduced, and with a character of order p.

Main declarations

• TauCeti.groupAlgebraSubgroupAverage: the normalized sum of a finite subgroup.
• TauCeti.isIdempotentElem_groupAlgebraSubgroupAverage: the subgroup average is idempotent.
• TauCeti.isMulTorsionFree_of_isReduced_monoidAlgebra_of_connectedSpace: reducedness and connectedness of a group algebra force its indexing group to be torsion-free.
• TauCeti.pow_expChar_monoidAlgebra_eq_algebraMap: in exponential characteristic p, the p-th power map of a p-torsion monoid algebra is the p-th power of its counit.
• TauCeti.connectedSpace_primeSpectrum_monoidAlgebra_of_pow_eq_one: over a coefficient ring with connected prime spectrum, a p-torsion monoid algebra in exponential characteristic p again has connected prime spectrum.

References

• J. S. Milne, Algebraic Groups (2017), Definitions 12.14 and 12.17.
• W. C. Waterhouse, Introduction to Affine Group Schemes, Chapter 2.

This is the character-group calculation used in Layer 4, "Tori: split and non-split", of the ReductiveGroups roadmap.

noncomputable def TauCeti.groupAlgebraSubgroupAverage {G : Type u_1} [Group G] (k : Type u_2) [Field k] (P : Subgroup G) [Fintype ↥P] : MonoidAlgebra k G

The normalized sum of a finite subgroup: the character sum of the trivial character, scaled by the inverse of the subgroup order.

Equations

• TauCeti.groupAlgebraSubgroupAverage k P = (↑(Fintype.card ↥P))⁻¹ • TauCeti.subgroupCharSum 1 P

@[simp]

theorem TauCeti.single_mul_groupAlgebraSubgroupAverage {G : Type u_1} [Group G] (k : Type u_2) [Field k] (P : Subgroup G) [Fintype ↥P] (x : ↥P) : MonoidAlgebra.single (↑x) 1 * groupAlgebraSubgroupAverage k P = groupAlgebraSubgroupAverage k P

Left multiplication by a member of a finite subgroup fixes its normalized subgroup average.

theorem TauCeti.isIdempotentElem_groupAlgebraSubgroupAverage {G : Type u_1} [Group G] (k : Type u_2) [Field k] (P : Subgroup G) [Fintype ↥P] (hP : ↑(Fintype.card ↥P) ≠ 0) : IsIdempotentElem (groupAlgebraSubgroupAverage k P)

The normalized sum of a finite subgroup is idempotent when its cardinality is nonzero in the base field.

theorem TauCeti.groupAlgebraSubgroupAverage_ne_zero {G : Type u_1} [Group G] (k : Type u_2) [Field k] (P : Subgroup G) [Fintype ↥P] (hP : ↑(Fintype.card ↥P) ≠ 0) : groupAlgebraSubgroupAverage k P ≠ 0

A finite subgroup average is nonzero when the subgroup cardinality is nonzero in the base field.

theorem TauCeti.groupAlgebraSubgroupAverage_ne_one {G : Type u_1} [Group G] (k : Type u_2) [Field k] (P : Subgroup G) [Fintype ↥P] (x : ↥P) (hx : ↑x ≠ 1) : groupAlgebraSubgroupAverage k P ≠ 1

The average over a nontrivial finite subgroup is not one.

theorem TauCeti.isMulTorsionFree_of_isReduced_monoidAlgebra_of_connectedSpace (k : Type u_3) [Field k] (G : Type u_4) [CommGroup G] [IsReduced (MonoidAlgebra k G)] [ConnectedSpace (PrimeSpectrum (MonoidAlgebra k G))] : IsMulTorsionFree G

If a group algebra over a field is reduced and has connected prime spectrum, then the indexing commutative group is torsion-free.

Connectedness of a p-torsion group algebra in characteristic p

The two hypotheses of isMulTorsionFree_of_isReduced_monoidAlgebra_of_connectedSpace are independent. Connectedness alone does not suffice: over a field of characteristic p, the group algebra of a group killed by p is connected, while not_isReduced_monoidAlgebra shows it is not reduced as soon as the group is nontrivial. The coordinate Hopf algebra of μ_p is the standard instance.

@[simp]

theorem TauCeti.pow_expChar_monoidAlgebra_eq_algebraMap (k : Type u_3) [CommSemiring k] {M : Type u_4} [CommMonoid M] (p : ℕ) [ExpChar k p] (hM : ∀ (m : M), m ^ p = 1) (x : MonoidAlgebra k M) : x ^ p = (algebraMap k (MonoidAlgebra k M)) (CoalgebraStruct.counit x ^ p)

In a monoid algebra over a commutative semiring of exponential characteristic p, indexed by a commutative monoid killed by p, the p-th power map is the p-th power of the counit.

theorem TauCeti.connectedSpace_primeSpectrum_monoidAlgebra_of_pow_eq_one (k : Type u_3) [CommRing k] [ConnectedSpace (PrimeSpectrum k)] {M : Type u_4} [CommMonoid M] (p : ℕ) [ExpChar k p] (hM : ∀ (m : M), m ^ p = 1) : ConnectedSpace (PrimeSpectrum (MonoidAlgebra k M))

Over a connected commutative ring of exponential characteristic p, the monoid algebra of a commutative monoid killed by p has connected prime spectrum: every element differs from its counit by a p-nilpotent element, so the only idempotents are the two trivial ones.