Mackey Character Formula

Abstract

Finite representation theory relates simple modules, characters, conjugation and induction.

Definition 1.1 (Of linear character).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{CommRing}\left(k\right)],[\mathrm{Monoid}\left(G\right)],\forall chi\in \mathrm{MonoidHom}\left(G,\mathrm{Units}\left(k\right)\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{MackeyCharacterFormula}.\mathrm{FDRep}.\mathrm{ofLinearCharacter}\left(chi\right)=(\mathrm{FDRep}.\mathrm{of}\left(((\mathrm{Algebra}.\mathrm{lsmul}\left(k,k,k\right)).\mathrm{toMonoidHom}).\mathrm{comp}\left((\mathrm{Units}.\mathrm{coeHom}\left(k\right)).\mathrm{comp}\left(chi\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/MackeyCharacterFormula.ofLinearCharacter (✓ std3).

Citation. The Tau Ceti contributors; Claude (2026). TauCeti finite representation and character theory. URL: https://github.com/TauCetiProject/TauCeti/tree/a780c7ad6beb23f60a17351a492d177878020ad5.

Commentary.

The formula defines the displayed algebraic construction.

Theorem 1.2 (Finrank of linear character).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Monoid}\left(G\right)],\forall chi\in \mathrm{MonoidHom}\left(G,\mathrm{Units}\left(k\right)\right),(\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{FGModuleCat}.\mathrm{carrier}\left(\mathrm{Action}.V\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{MackeyCharacterFormula}.\mathrm{FDRep}.\mathrm{ofLinearCharacter}\left(chi\right)\right)\right)\right))=(1)$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/MackeyCharacterFormula.finrank_ofLinearCharacter (✓ std3). ∎

Citation. The Tau Ceti contributors; Claude (2026). TauCeti finite representation and character theory. URL: https://github.com/TauCetiProject/TauCeti/tree/a780c7ad6beb23f60a17351a492d177878020ad5.

Commentary.

The displayed conclusion holds under the stated hypotheses.

Theorem 1.3 (Simple ind fdr ep of linear character iff).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],[\mathrm{Finite}\left(G\right)],[\mathrm{IsAlgClosed}\left(k\right)],[\mathrm{CharZero}\left(k\right)],\forall chi\in \mathrm{MonoidHom}\left(\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right),\mathrm{Units}\left(k\right)\right),(\mathrm{CategoryTheory}.\mathrm{Simple}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indFDRep}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{MackeyCharacterFormula}.\mathrm{FDRep}.\mathrm{ofLinearCharacter}\left(chi\right)\right)\right))\iff (\forall s\in G,(\neg (\mathrm{Membership}.\mathrm{mem}\left(N,s\right)))\Rightarrow (\exists x\in \mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right),\mathrm{Ne}\left(\mathrm{DFunLike}.\mathrm{coe}\left(chi,\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MulAut}.\mathrm{conjNormal},s\right),x\right)\right),\mathrm{DFunLike}.\mathrm{coe}\left(chi,x\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/MackeyCharacterFormula.simple_indFDRep_ofLinearCharacter_iff (✓ std3). ∎

Citation. The Tau Ceti contributors; Claude (2026). TauCeti finite representation and character theory. URL: https://github.com/TauCetiProject/TauCeti/tree/a780c7ad6beb23f60a17351a492d177878020ad5.

Commentary.

The displayed conclusion holds under the stated hypotheses.

References

• Truth anchor: D5/S3/FiniteGroups/MackeyCharacterFormula.finrank_ofLinearCharacter
• Truth anchor: D5/S3/FiniteGroups/MackeyCharacterFormula.ofLinearCharacter
• Truth anchor: D5/S3/FiniteGroups/MackeyCharacterFormula.simple_indFDRep_ofLinearCharacter_iff
• Dependency: D5/S3/FiniteGroups/CliffordConstituents
• Dependency: D5/S3/FiniteGroups/CliffordDecomposition
• Dependency: D5/S3/FiniteGroups/FiniteCharacterAlgebra
• Dependency: D5/S3/FiniteGroups/InducedCharacterFormula