Class functions

This file defines functions on a group that are constant on conjugacy classes. It identifies their module with the module of functions on ConjClasses G, computes its finite rank when there are finitely many conjugacy classes, pulls class functions back along a group homomorphism, twists them by a power map, inverts the group element, changes their coefficients along a ring homomorphism, shows that characters of representations are class functions, and evaluates a sum over a finite group one conjugacy class at a time.

Inverting the group element, TauCeti.ClassFunction.invMap, is the involution that turns the character of a representation into the character of its dual (TauCeti.ClassFunction.invMap_ofCharacter). For finite groups, inversion also conjugates the values of finite-dimensional complex characters.

The indicator function of a conjugacy class, TauCeti.ClassFunction.classIndicator, is the class function pulled back from the indicator of a single point of ConjClasses G; pairing a class function against it is how a class function is read off an expansion in a basis of class functions.

These are the indexing foundations for character tables.

The class-function module and its conjugacy-class correspondence are defined over any semiring. The finite-rank formula TauCeti.ClassFunction.finrank_eq_card_conjClasses assumes StrongRankCondition on the coefficients; in particular it applies over fields and over ℤ. The character constructions use Mathlib's Representation.character and FDRep.character.

def TauCeti.ClassFunction (k : Type u) (G : Type v) [Semiring k] [Group G] : Submodule k (G → k)

The submodule of functions on G that are constant under conjugation.

Equations

• TauCeti.ClassFunction k G = { carrier := {f : G → k | ∀ (g h : G), f (h * g * h⁻¹) = f g}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

@[simp]

theorem TauCeti.ClassFunction.mem_iff {k : Type u} {G : Type v} [Semiring k] [Group G] {f : G → k} : f ∈ ClassFunction k G ↔ ∀ (g h : G), f (h * g * h⁻¹) = f g

A function is a class function exactly when it is invariant under conjugation.

theorem TauCeti.ClassFunction.mem_of_isMulCommutative {k : Type u} {G : Type v} [Semiring k] [Group G] [IsMulCommutative G] (f : G → k) : f ∈ ClassFunction k G

On a commutative group every function is a class function: conjugation is the identity.

theorem TauCeti.ClassFunction.eq_of_isConj {k : Type u} {G : Type v} [Semiring k] [Group G] (f : ↥(ClassFunction k G)) {g h : G} (hgh : IsConj g h) : ↑f g = ↑f h

Class functions take the same value on conjugate elements.

noncomputable def TauCeti.ClassFunction.toConjClasses {k : Type u} {G : Type v} [Semiring k] [Group G] (f : ↥(ClassFunction k G)) : ConjClasses G → k

Evaluate a class function on a conjugacy class.

Equations

• TauCeti.ClassFunction.toConjClasses f = Quotient.lift ↑f ⋯

@[simp]

theorem TauCeti.ClassFunction.toConjClasses_mk {k : Type u} {G : Type v} [Semiring k] [Group G] (f : ↥(ClassFunction k G)) (g : G) : toConjClasses f (ConjClasses.mk g) = ↑f g

Evaluating the induced function on the class of g gives the value at g.

def TauCeti.ClassFunction.ofConjClasses {k : Type u} {G : Type v} [Semiring k] [Group G] (f : ConjClasses G → k) : ↥(ClassFunction k G)

Pull a function on conjugacy classes back to a class function on the group.

Equations

• TauCeti.ClassFunction.ofConjClasses f = ⟨fun (g : G) => f (ConjClasses.mk g), ⋯⟩

@[simp]

theorem TauCeti.ClassFunction.ofConjClasses_apply {k : Type u} {G : Type v} [Semiring k] [Group G] (f : ConjClasses G → k) (g : G) : ↑(ofConjClasses f) g = f (ConjClasses.mk g)

Pulling back a function on conjugacy classes evaluates it on the class of g.

@[simp]

theorem TauCeti.ClassFunction.toConjClasses_ofConjClasses {k : Type u} {G : Type v} [Semiring k] [Group G] (f : ConjClasses G → k) : toConjClasses (ofConjClasses f) = f

Pulling a function on conjugacy classes back and evaluating it again returns it.

@[simp]

theorem TauCeti.ClassFunction.ofConjClasses_toConjClasses {k : Type u} {G : Type v} [Semiring k] [Group G] (f : ↥(ClassFunction k G)) : ofConjClasses (toConjClasses f) = f

Evaluating a class function on conjugacy classes and pulling it back returns the original class function.

def TauCeti.ClassFunction.comap {k : Type u} {G : Type v} [Semiring k] [Group G] {H : Type w} [Group H] (φ : H →* G) : ↥(ClassFunction k G) →ₗ[k] ↥(ClassFunction k H)

Pull a class function back along a group homomorphism. Restriction of a class function to a subgroup is the case φ = S.subtype.

Equations

• TauCeti.ClassFunction.comap φ = { toFun := fun (f : ↥(TauCeti.ClassFunction k G)) => ⟨fun (x : H) => ↑f (φ x), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.ClassFunction.comap_apply {k : Type u} {G : Type v} [Semiring k] [Group G] {H : Type w} [Group H] (φ : H →* G) (f : ↥(ClassFunction k G)) (x : H) : ↑((comap φ) f) x = ↑f (φ x)

A pulled-back class function is the composite with the homomorphism.

@[simp]

theorem TauCeti.ClassFunction.comap_id {k : Type u} {G : Type v} [Semiring k] [Group G] : comap (MonoidHom.id G) = LinearMap.id

Pulling back along the identity homomorphism changes nothing.

@[simp]

theorem TauCeti.ClassFunction.comap_comp {k : Type u} {G : Type v} [Semiring k] [Group G] {H : Type w} {J : Type w'} [Group H] [Group J] (φ : H →* G) (ψ : J →* H) : comap (φ.comp ψ) = comap ψ ∘ₗ comap φ

Pullback is contravariantly functorial: pulling back along a composite is pulling back along each factor in turn.

def TauCeti.ClassFunction.powMap {k : Type u} {G : Type v} [Semiring k] [Group G] (j : ℕ) : ↥(ClassFunction k G) →ₗ[k] ↥(ClassFunction k G)

The linear power-map twist f ↦ (g ↦ f (g ^ j)) of a class function. For a finite group, powers coprime to its exponent describe the cyclotomic Galois action on character values.

Equations

• TauCeti.ClassFunction.powMap j = { toFun := fun (f : ↥(TauCeti.ClassFunction k G)) => ⟨fun (g : G) => ↑f (g ^ j), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.ClassFunction.powMap_apply {k : Type u} {G : Type v} [Semiring k] [Group G] (j : ℕ) (f : ↥(ClassFunction k G)) (g : G) : ↑((powMap j) f) g = ↑f (g ^ j)

The power-map twist evaluates the class function at the power of the group element.

@[simp]

theorem TauCeti.ClassFunction.powMap_one {k : Type u} {G : Type v} [Semiring k] [Group G] : powMap 1 = LinearMap.id

Twisting by the first power changes nothing.

@[simp]

theorem TauCeti.ClassFunction.powMap_mul {k : Type u} {G : Type v} [Semiring k] [Group G] (i j : ℕ) : powMap (i * j) = powMap i ∘ₗ powMap j

The power maps compose: twisting by j and then by i is twisting by i * j. This is what makes the twists an action of the multiplicative monoid of exponents.

def TauCeti.ClassFunction.invMap {k : Type u} {G : Type v} [Semiring k] [Group G] : ↥(ClassFunction k G) →ₗ[k] ↥(ClassFunction k G)

The linear inversion twist f ↦ (g ↦ f g⁻¹) of a class function. On characters of finite-dimensional representations, this is passage to the dual representation.

Equations

• TauCeti.ClassFunction.invMap = { toFun := fun (f : ↥(TauCeti.ClassFunction k G)) => ⟨fun (g : G) => ↑f g⁻¹, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.ClassFunction.invMap_apply {k : Type u} {G : Type v} [Semiring k] [Group G] (f : ↥(ClassFunction k G)) (g : G) : ↑(invMap f) g = ↑f g⁻¹

The inversion twist evaluates the class function at the inverse of the group element.

@[simp]

theorem TauCeti.ClassFunction.invMap_invMap {k : Type u} {G : Type v} [Semiring k] [Group G] (f : ↥(ClassFunction k G)) : invMap (invMap f) = f

Inverting the group element twice changes nothing: invMap is an involution.

def TauCeti.ClassFunction.map {k : Type u} {G : Type v} [Semiring k] [Group G] {k' : Type w} [Semiring k'] (σ : k →+* k') : ↥(ClassFunction k G) →ₛₗ[σ] ↥(ClassFunction k' G)

Change of coefficients along a ring homomorphism σ : k →+* k': the class function g ↦ σ (f g). Along algebraMap K L it carries the character of a representation over K to the character of its scalar extension to L (TauCeti.ClassFunction.ofFDRep_baseChange).

Equations

• TauCeti.ClassFunction.map σ = { toFun := fun (f : ↥(TauCeti.ClassFunction k G)) => ⟨fun (g : G) => σ (↑f g), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.ClassFunction.map_apply {k : Type u} {G : Type v} [Semiring k] [Group G] {k' : Type w} [Semiring k'] (σ : k →+* k') (f : ↥(ClassFunction k G)) (g : G) : ↑((map σ) f) g = σ (↑f g)

Changing coefficients applies the ring homomorphism to each value.

@[simp]

theorem TauCeti.ClassFunction.map_id {k : Type u} {G : Type v} [Semiring k] [Group G] (f : ↥(ClassFunction k G)) : (map (RingHom.id k)) f = f

Changing coefficients along the identity changes nothing.

@[simp]

theorem TauCeti.ClassFunction.map_map {k : Type u} {G : Type v} [Semiring k] [Group G] {k' : Type w} {k'' : Type w'} [Semiring k'] [Semiring k''] (σ₁ : k →+* k') (σ₂ : k' →+* k'') (f : ↥(ClassFunction k G)) : (map σ₂) ((map σ₁) f) = (map (σ₂.comp σ₁)) f

Changing coefficients along σ₁ and then along σ₂ is changing them along σ₂.comp σ₁.

noncomputable def TauCeti.ClassFunction.equivConjClasses {k : Type u} {G : Type v} [Semiring k] [Group G] : ↥(ClassFunction k G) ≃ₗ[k] ConjClasses G → k

Class functions on G are linearly equivalent to functions on its conjugacy classes.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ClassFunction.equivConjClasses_apply {k : Type u} {G : Type v} [Semiring k] [Group G] (f : ↥(ClassFunction k G)) : equivConjClasses f = toConjClasses f

The linear equivalence is given by toConjClasses.

@[simp]

theorem TauCeti.ClassFunction.equivConjClasses_symm_apply {k : Type u} {G : Type v} [Semiring k] [Group G] (f : ConjClasses G → k) : equivConjClasses.symm f = ofConjClasses f

The inverse linear equivalence is given by ofConjClasses.

noncomputable def TauCeti.ClassFunction.classIndicator {k : Type u} {G : Type v} [Semiring k] [Group G] (x : G) : ↥(ClassFunction k G)

The indicator class function of the conjugacy class of x: it takes the value 1 on the conjugates of x and 0 elsewhere.

Set.indicator rather than Pi.single so that the definition carries no decidability instance of its own, and TauCeti.ClassFunction.classIndicator_apply can be stated with whichever instance is in scope where it is used.

Equations

• TauCeti.ClassFunction.classIndicator x = TauCeti.ClassFunction.ofConjClasses ({ConjClasses.mk x}.indicator fun (x : ConjClasses G) => 1)

@[simp]

theorem TauCeti.ClassFunction.classIndicator_apply {k : Type u} {G : Type v} [Semiring k] [Group G] [DecidableEq (ConjClasses G)] (x y : G) : ↑(classIndicator x) y = if ConjClasses.mk y = ConjClasses.mk x then 1 else 0

The defining values of TauCeti.ClassFunction.classIndicator.

theorem TauCeti.ClassFunction.sum_eq_sum_conjClasses {k : Type u} {G : Type v} [Semiring k] [Group G] [Fintype G] [Fintype (ConjClasses G)] (f : ↥(ClassFunction k G)) : ∑ g : G, ↑f g = ∑ C : ConjClasses G, ↑(Nat.card ↑C.carrier) * toConjClasses f C

The sum of a class function over a finite group is the sum of its values on conjugacy classes, weighted by the sizes of those classes. This converts group sums into sums over the columns of a character table.

theorem TauCeti.ClassFunction.finrank_eq_card_conjClasses {k : Type u} {G : Type v} [Semiring k] [StrongRankCondition k] [Group G] [Finite (ConjClasses G)] : Module.finrank k ↥(ClassFunction k G) = Nat.card (ConjClasses G)

Over a semiring satisfying the strong rank condition, the finite rank of the class-function module is the number of conjugacy classes, provided there are finitely many.

noncomputable def TauCeti.ClassFunction.ofCharacter {k : Type u} {G : Type v} [Field k] [Group G] {V : Type w} [AddCommGroup V] [Module k V] (ρ : Representation k G V) : ↥(ClassFunction k G)

The character of a representation is a class function.

Equations

• TauCeti.ClassFunction.ofCharacter ρ = ⟨ρ.character, ⋯⟩

@[simp]

theorem TauCeti.ClassFunction.ofCharacter_apply {k : Type u} {G : Type v} [Field k] [Group G] {V : Type w} [AddCommGroup V] [Module k V] (ρ : Representation k G V) (g : G) : ↑(ofCharacter ρ) g = ρ.character g

The class function of a representation evaluates to its character.

@[simp]

theorem TauCeti.ClassFunction.invMap_ofCharacter {k : Type u} {G : Type v} [Field k] [Group G] {V : Type w} [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) : invMap (ofCharacter ρ) = ofCharacter ρ.dual

Inverting the group element in a character gives the character of the dual representation: χ_{ρ*}(g) = χ_ρ(g⁻¹).

noncomputable def TauCeti.ClassFunction.ofFDRep {k : Type u} {G : Type v} [Field k] [Group G] (V : FDRep k G) : ↥(ClassFunction k G)

The character of a finite-dimensional bundled representation is a class function.

Equations

• TauCeti.ClassFunction.ofFDRep V = TauCeti.ClassFunction.ofCharacter V.ρ

@[simp]

theorem TauCeti.ClassFunction.ofFDRep_apply {k : Type u} {G : Type v} [Field k] [Group G] (V : FDRep k G) (g : G) : ↑(ofFDRep V) g = V.character g

The class function of a bundled finite-dimensional representation evaluates to its character.

theorem TauCeti.ClassFunction.ofFDRep_eq_ofCharacter {k : Type u} {G : Type v} [Field k] [Group G] (V : FDRep k G) : ofFDRep V = ofCharacter V.ρ

The class function of a bundled finite-dimensional representation is the class function of the underlying representation: FDRep.character is Representation.character of V.ρ.

theorem MonoidHom.comp_mem_classFunction {k : Type u_1} {G : Type u_2} [Semiring k] [Group G] {M : Type u_3} [CommMonoid M] (χ : G →* M) (f : M → k) : (fun (g : G) => f (χ g)) ∈ TauCeti.ClassFunction k G

A function factoring through a homomorphism into a commutative monoid is a class function, conjugation being invisible there; for instance a linear character χ : G →* kˣ, read in k.