Finite Character Algebra

Abstract

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

Theorem 1.1 (To submodule bot).

$$\forall A\in Type\ast ,\forall G\in Type\ast ,\forall W\in Type\ast ,[\mathrm{Semiring}\left(A\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommMonoid}\left(W\right)],[\mathrm{Module}\left(A,W\right)],\forall rho\in \mathrm{Representation}\left(A,G,W\right),(\mathrm{Subrepresentation}.\mathrm{toSubmodule}\left((\mathrm{Bot}.\mathrm{bot}:\mathrm{Subrepresentation}\left(rho\right))\right))=((\mathrm{Bot}.\mathrm{bot}:\mathrm{Submodule}\left(A,W\right)))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.toSubmodule_bot (✓ 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.2 (To submodule top).

$$\forall A\in Type\ast ,\forall G\in Type\ast ,\forall W\in Type\ast ,[\mathrm{Semiring}\left(A\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommMonoid}\left(W\right)],[\mathrm{Module}\left(A,W\right)],\forall rho\in \mathrm{Representation}\left(A,G,W\right),(\mathrm{Subrepresentation}.\mathrm{toSubmodule}\left((\mathrm{Top}.\mathrm{top}:\mathrm{Subrepresentation}\left(rho\right))\right))=((\mathrm{Top}.\mathrm{top}:\mathrm{Submodule}\left(A,W\right)))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.toSubmodule_top (✓ 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.

Definition 1.3 (As module equiv as submodule).

$$\forall A\in Type\ast ,\forall G\in Type\ast ,\forall W\in Type\ast ,[\mathrm{CommSemiring}\left(A\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommMonoid}\left(W\right)],[\mathrm{Module}\left(A,W\right)],\forall rho\in \mathrm{Representation}\left(A,G,W\right),\forall sigma\in \mathrm{Subrepresentation}\left(rho\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{Subrepresentation}.\mathrm{asModuleEquivAsSubmodule}\left(sigma\right)=(\mathrm{LinearEquiv}.\mathrm{mk}\left(\mathrm{LinearMap}.\mathrm{mk}\left(\mathrm{AddHom}.\mathrm{mk}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{Subrepresentation}.\mathrm{toRepresentation}\left(sigma\right)\right))\mapsto (\mathrm{Subtype}.\mathrm{mk}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{LinearEquiv}.\mathrm{symm}\left(\mathrm{Representation}.\mathrm{asModuleEquiv}\left(rho\right)\right),\mathrm{Subtype}.\mathrm{val}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{Representation}.\mathrm{asModuleEquiv}\left(\mathrm{Subrepresentation}.\mathrm{toRepresentation}\left(sigma\right)\right),x\right)\right)\right)\right))\right)\right),\lambda (x:\mathrm{Subtype}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(rho\right))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subrepresentation}.\mathrm{asSubmodule}\left(sigma\right),x\right))\right))\mapsto (\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{LinearEquiv}.\mathrm{symm}\left(\mathrm{Representation}.\mathrm{asModuleEquiv}\left(\mathrm{Subrepresentation}.\mathrm{toRepresentation}\left(sigma\right)\right)\right),\mathrm{Subtype}.\mathrm{mk}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{Representation}.\mathrm{asModuleEquiv}\left(rho\right),\mathrm{Subtype}.\mathrm{val}\left(x\right)\right)\right)\right))\right))$$

Formalization. D5/S3/FiniteGroups/FiniteCharacterAlgebra.asModuleEquivAsSubmodule (✓ 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.4 (Is simple module as submodule iff).

$$\forall A\in Type\ast ,\forall G\in Type\ast ,\forall W\in Type\ast ,[\mathrm{CommRing}\left(A\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommGroup}\left(W\right)],[\mathrm{Module}\left(A,W\right)],\forall rho\in \mathrm{Representation}\left(A,G,W\right),\forall sigma\in \mathrm{Subrepresentation}\left(rho\right),(\mathrm{IsSimpleModule}\left(\mathrm{MonoidAlgebra}\left(A,G\right),\mathrm{Subtype}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(rho\right))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subrepresentation}.\mathrm{asSubmodule}\left(sigma\right),x\right))\right)\right))\iff (\mathrm{IsAtom}\left(sigma\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.isSimpleModule_asSubmodule_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.

Theorem 1.5 (Simple of is irreducible).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Monoid}\left(G\right)],\forall X\in \mathrm{FDRep}\left(k,G\right),[\mathrm{Representation}.\mathrm{IsIrreducible}\left(\mathrm{FDRep}.\rho \left(X\right)\right)],\mathrm{CategoryTheory}.\mathrm{Simple}\left(X\right)$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.simple_of_isIrreducible (✓ 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.6 (Is irreducible of simple).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Monoid}\left(G\right)],\forall X\in \mathrm{FDRep}\left(k,G\right),[\mathrm{CategoryTheory}.\mathrm{Simple}\left(X\right)],\mathrm{Representation}.\mathrm{IsIrreducible}\left(\mathrm{FDRep}.\rho \left(X\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.isIrreducible_of_simple (✓ 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.7 (Character action res).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall H\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{Monoid}\left(H\right)],\forall V\in \mathrm{FDRep}\left(k,G\right),\forall phi\in \mathrm{MonoidHom}\left(H,G\right),\forall h\in H,(\mathrm{FDRep}.\mathrm{character}\left(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(\mathrm{Action}.\mathrm{res}\left(\mathrm{FGModuleCat}\left(k\right),phi\right),V\right),h\right))=(\mathrm{FDRep}.\mathrm{character}\left(V,\mathrm{DFunLike}.\mathrm{coe}\left(phi,h\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.character_actionRes (✓ 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.8 (Module finite forget object).

$$\forall R\in Type\ast ,\forall G\in Type\ast ,[\mathrm{CommRing}\left(R\right)],[\mathrm{Monoid}\left(G\right)],\forall A\in \mathrm{FDRep}\left(R,G\right),\mathrm{Module}.\mathrm{Finite}\left(R,\mathrm{Rep}.V\left(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(\mathrm{CategoryTheory}.{\mathrm{forget}}_2\left(\mathrm{FDRep}\left(R,G\right),\mathrm{Rep}\left(R,G\right)\right),A\right)\right)\right)$$

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

Source. Repository-derived.

Acknowledgement. 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.9 (Finrank forget object).

$$\forall R\in Type\ast ,\forall G\in Type\ast ,[\mathrm{CommRing}\left(R\right)],[\mathrm{Monoid}\left(G\right)],\forall A\in \mathrm{FDRep}\left(R,G\right),(\mathrm{Module}.\mathrm{finrank}\left(R,\mathrm{Rep}.V\left(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(\mathrm{CategoryTheory}.{\mathrm{forget}}_2\left(\mathrm{FDRep}\left(R,G\right),\mathrm{Rep}\left(R,G\right)\right),A\right)\right)\right))=(\mathrm{Module}.\mathrm{finrank}\left(R,\mathrm{FGModuleCat}.\mathrm{carrier}\left(\mathrm{Action}.V\left(A\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.finrankForgetObject (✓ 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.10 (Character forget object).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Monoid}\left(G\right)],\forall A\in \mathrm{FDRep}\left(k,G\right),\forall g\in G,(\mathrm{Representation}.\mathrm{character}\left(\mathrm{Rep}.\rho \left(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(\mathrm{CategoryTheory}.{\mathrm{forget}}_2\left(\mathrm{FDRep}\left(k,G\right),\mathrm{Rep}\left(k,G\right)\right),A\right)\right),g\right))=(\mathrm{FDRep}.\mathrm{character}\left(A,g\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.characterForgetObject (✓ 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.11 (Of eq self).

$$\forall R\in Type\ast ,\forall G\in Type\ast ,[\mathrm{CommRing}\left(R\right)],[\mathrm{Monoid}\left(G\right)],\forall A\in \mathrm{FDRep}\left(R,G\right),(\mathrm{FDRep}.\mathrm{of}\left(\mathrm{FDRep}.\rho \left(A\right)\right))=(A)$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.of_ρ_eq_self (✓ 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.

Definition 1.12 (Of shrink).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{CommRing}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],[\mathrm{Module}.\mathrm{Finite}\left(k,V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{FDRep}.\mathrm{ofShrink}\left(rho\right)=(\mathrm{FDRep}.\mathrm{of}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(\mathrm{RingEquiv}.\mathrm{toMonoidHom}\left(\mathrm{LinearEquiv}.\mathrm{conjRingEquiv}\left(\mathrm{LinearEquiv}.\mathrm{symm}\left(\mathrm{Shrink}.\mathrm{linearEquiv}\left(k,V\right)\right)\right)\right),rho\right)\right))$$

Formalization. D5/S3/FiniteGroups/FiniteCharacterAlgebra.ofShrink (✓ 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.

Definition 1.13 (Of shrink equiv).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{CommRing}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],[\mathrm{Module}.\mathrm{Finite}\left(k,V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{FDRep}.\mathrm{ofShrinkEquiv}\left(rho\right)=(\mathrm{Representation}.\mathrm{Equiv}.\mathrm{mk}\left(\mathrm{Shrink}.\mathrm{linearEquiv}\left(k,V\right)\right))$$

Formalization. D5/S3/FiniteGroups/FiniteCharacterAlgebra.ofShrinkEquiv (✓ 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.14 (Finrank of shrink).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{CommRing}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],[\mathrm{Module}.\mathrm{Finite}\left(k,V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),(\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{FGModuleCat}.\mathrm{carrier}\left(\mathrm{Action}.V\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{FDRep}.\mathrm{ofShrink}\left(rho\right)\right)\right)\right))=(\mathrm{Module}.\mathrm{finrank}\left(k,V\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.finrank_ofShrink (✓ 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.15 (Character of shrink).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],[\mathrm{FiniteDimensional}\left(k,V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),\forall g\in G,(\mathrm{FDRep}.\mathrm{character}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{FDRep}.\mathrm{ofShrink}\left(rho\right),g\right))=(\mathrm{Representation}.\mathrm{character}\left(rho,g\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.character_ofShrink (✓ 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.

Definition 1.16 (Class function).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Semiring}\left(k\right)],[\mathrm{Group}\left(G\right)],D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,G\right)=(\mathrm{Submodule}.\mathrm{mk}\left(\mathrm{AddSubmonoid}.\mathrm{mk}\left(\mathrm{AddSubsemigroup}.\mathrm{mk}\left(\mathrm{Set}.\mathrm{ofPred}\left(\lambda (f:(G)\to (k))\mapsto (\forall g\in G,\forall h\in G,(f\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(h,g\right),\mathrm{Inv}.\mathrm{inv}\left(h\right)\right)\right))=(f\left(g\right)))\right)\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/FiniteCharacterAlgebra.ClassFunction (✓ 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.17 (Mem iff).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Semiring}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall f\in (G)\to (k),(\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,G\right),f\right))\iff (\forall g\in G,\forall h\in G,(f\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(h,g\right),\mathrm{Inv}.\mathrm{inv}\left(h\right)\right)\right))=(f\left(g\right)))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.mem_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.

Definition 1.18 (To conj classes).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Semiring}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall f\in \mathrm{Subtype}\left(\lambda (x:(G)\to (k))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,G\right),x\right))\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{toConjClasses}\left(f\right)=(\mathrm{Quotient}.\mathrm{lift}\left(\mathrm{Subtype}.\mathrm{val}\left(f\right)\right))$$

Formalization. D5/S3/FiniteGroups/FiniteCharacterAlgebra.toConjClasses (✓ 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.19 (To conj classes mk).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Semiring}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall f\in \mathrm{Subtype}\left(\lambda (x:(G)\to (k))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,G\right),x\right))\right),\forall g\in G,(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{toConjClasses}\left(f,\mathrm{ConjClasses}.\mathrm{mk}\left(g\right)\right))=(\mathrm{Subtype}.\mathrm{val}\left(f,g\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.toConjClasses_mk (✓ 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.

Definition 1.20 (Comap).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Semiring}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall H\in Type\ast ,[\mathrm{Group}\left(H\right)],\forall phi\in \mathrm{MonoidHom}\left(H,G\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{comap}\left(phi\right)=(\mathrm{LinearMap}.\mathrm{mk}\left(\mathrm{AddHom}.\mathrm{mk}\left(\lambda (f:\mathrm{Subtype}\left(\lambda (x:(G)\to (k))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,G\right),x\right))\right))\mapsto (\mathrm{Subtype}.\mathrm{mk}\left(\lambda (x:H)\mapsto (\mathrm{Subtype}.\mathrm{val}\left(f,\mathrm{DFunLike}.\mathrm{coe}\left(phi,x\right)\right))\right))\right)\right))$$

Formalization. D5/S3/FiniteGroups/FiniteCharacterAlgebra.comap (✓ 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.21 (Comap apply).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Semiring}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall H\in Type\ast ,[\mathrm{Group}\left(H\right)],\forall phi\in \mathrm{MonoidHom}\left(H,G\right),\forall f\in \mathrm{Subtype}\left(\lambda (x:(G)\to (k))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,G\right),x\right))\right),\forall x\in H,(\mathrm{Subtype}.\mathrm{val}\left(\mathrm{DFunLike}.\mathrm{coe}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{comap}\left(phi\right),f\right),x\right))=(\mathrm{Subtype}.\mathrm{val}\left(f,\mathrm{DFunLike}.\mathrm{coe}\left(phi,x\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.comap_apply (✓ 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.22 (Sum eq sum conj classes).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Semiring}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{Fintype}\left(G\right)],[\mathrm{Fintype}\left(\mathrm{ConjClasses}\left(G\right)\right)],\forall f\in \mathrm{Subtype}\left(\lambda (x:(G)\to (k))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,G\right),x\right))\right),(\mathrm{Finset}.\mathrm{sum}\left(\mathrm{Finset}.\mathrm{univ},\lambda (g:G)\mapsto (\mathrm{Subtype}.\mathrm{val}\left(f,g\right))\right))=(\mathrm{Finset}.\mathrm{sum}\left(\mathrm{Finset}.\mathrm{univ},\lambda (C:\mathrm{ConjClasses}\left(G\right))\mapsto (\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Nat}.\mathrm{card}\left(\mathrm{Set}.\mathrm{Elem}\left(\mathrm{ConjClasses}.\mathrm{carrier}\left(C\right)\right)\right)\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{toConjClasses}\left(f,C\right)\right))\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.sum_eq_sum_conjClasses (✓ 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.

Definition 1.23 (Of character).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall V\in Type\ast ,[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{ofCharacter}\left(rho\right)=(\mathrm{Subtype}.\mathrm{mk}\left(\mathrm{Representation}.\mathrm{character}\left(rho\right)\right))$$

Formalization. D5/S3/FiniteGroups/FiniteCharacterAlgebra.ofCharacter (✓ 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.24 (Of character apply).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall V\in Type\ast ,[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),\forall g\in G,(\mathrm{Subtype}.\mathrm{val}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{ofCharacter}\left(rho\right),g\right))=(\mathrm{Representation}.\mathrm{character}\left(rho,g\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.ofCharacter_apply (✓ 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.25 (Action res comp).

$$\forall H\in Type\ast ,\forall K\in Type\ast ,\forall L\in Type\ast ,[\mathrm{Monoid}\left(H\right)],[\mathrm{Monoid}\left(K\right)],[\mathrm{Monoid}\left(L\right)],\forall V\in Type\ast ,[\mathrm{CategoryTheory}.\mathrm{Category}\left(V\right)],\forall phi\in \mathrm{MonoidHom}\left(K,L\right),\forall psi\in \mathrm{MonoidHom}\left(H,K\right),(\mathrm{Action}.\mathrm{res}\left(V,\mathrm{MonoidHom}.\mathrm{comp}\left(phi,psi\right)\right))=(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{comp}\left(\mathrm{Action}.\mathrm{res}\left(V,phi\right),\mathrm{Action}.\mathrm{res}\left(V,psi\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.actionRes_comp (✓ 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.26 (Finrank hom res mul equiv).

$$\forall k\in Type\ast ,[\mathrm{Field}\left(k\right)],\forall M\in Type\ast ,\forall MPrime\in Type\ast ,[\mathrm{Group}\left(M\right)],[\mathrm{Group}\left(MPrime\right)],\forall e\in \mathrm{MulEquiv}\left(M,MPrime\right),\forall X\in \mathrm{FDRep}\left(k,MPrime\right),\forall Y\in \mathrm{FDRep}\left(k,MPrime\right),(\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{Quiver}.\mathrm{Hom}\left(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(\mathrm{Action}.\mathrm{res}\left(\mathrm{FGModuleCat}\left(k\right),\mathrm{MonoidHom}.\mathrm{ofClass}\left(e\right)\right),X\right),\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(\mathrm{Action}.\mathrm{res}\left(\mathrm{FGModuleCat}\left(k\right),\mathrm{MonoidHom}.\mathrm{ofClass}\left(e\right)\right),Y\right)\right)\right))=(\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{Quiver}.\mathrm{Hom}\left(X,Y\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.finrank_hom_res_mulEquiv (✓ 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.27 (Is irreducible comp surjective iff).

$$\forall k\in Type\ast ,[\mathrm{Field}\left(k\right)],\forall H\in Type\ast ,\forall K\in Type\ast ,[\mathrm{Monoid}\left(H\right)],[\mathrm{Monoid}\left(K\right)],\forall V\in Type\ast ,[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall f\in \mathrm{MonoidHom}\left(H,K\right),(\mathrm{Function}.\mathrm{Surjective}\left(\mathrm{DFunLike}.\mathrm{coe}\left(f\right)\right))\Rightarrow (\forall rho\in \mathrm{Representation}\left(k,K,V\right),(\mathrm{Representation}.\mathrm{IsIrreducible}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,f\right)\right))\iff (\mathrm{Representation}.\mathrm{IsIrreducible}\left(rho\right)))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.isIrreducible_comp_surjective_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.

Theorem 1.28 (Comap subtype of fdr ep).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],[\mathrm{Field}\left(k\right)],\forall S\in \mathrm{Subgroup}\left(G\right),\forall B\in \mathrm{FDRep}\left(k,G\right),(\mathrm{DFunLike}.\mathrm{coe}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{comap}\left(\mathrm{Subgroup}.\mathrm{subtype}\left(S\right)\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{ofCharacter}\left(\mathrm{FDRep}.\rho \left(B\right)\right)\right))=(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{ofCharacter}\left(\mathrm{FDRep}.\rho \left(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(\mathrm{Action}.\mathrm{res}\left(\mathrm{FGModuleCat}\left(k\right),\mathrm{Subgroup}.\mathrm{subtype}\left(S\right)\right),B\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.comap_subtype_ofFDRep (✓ 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.

Definition 1.29 (Class sum).

$$\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],[\mathrm{Fintype}\left(G\right)],[\mathrm{DecidableEq}\left(G\right)],\forall k\in Type\ast ,[\mathrm{Semiring}\left(k\right)],\forall C\in \mathrm{ConjClasses}\left(G\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{classSum}\left(k,C\right)=(\mathrm{Finset}.\mathrm{sum}\left(\mathrm{Finset}.\mathrm{univ},\lambda (x:\mathrm{Set}.\mathrm{Elem}\left(\mathrm{ConjClasses}.\mathrm{carrier}\left(C\right)\right))\mapsto (\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MonoidAlgebra}.\mathrm{of}\left(k,G\right),\mathrm{Subtype}.\mathrm{val}\left(x\right)\right))\right))$$

Formalization. D5/S3/FiniteGroups/FiniteCharacterAlgebra.classSum (✓ 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.30 (Class sum eq sum).

$$\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],[\mathrm{Fintype}\left(G\right)],[\mathrm{DecidableEq}\left(G\right)],\forall k\in Type\ast ,[\mathrm{Semiring}\left(k\right)],\forall C\in \mathrm{ConjClasses}\left(G\right),(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{classSum}\left(k,C\right))=(\mathrm{Finset}.\mathrm{sum}\left(\mathrm{Finset}.\mathrm{univ},\lambda (x:\mathrm{Set}.\mathrm{Elem}\left(\mathrm{ConjClasses}.\mathrm{carrier}\left(C\right)\right))\mapsto (\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MonoidAlgebra}.\mathrm{of}\left(k,G\right),\mathrm{Subtype}.\mathrm{val}\left(x\right)\right))\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.classSum_eq_sum (✓ 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.

Definition 1.31 (Class sum center).

$$\forall G\in Type\ast ,\forall k\in Type\ast ,[\mathrm{Group}\left(G\right)],[\mathrm{Fintype}\left(G\right)],[\mathrm{DecidableEq}\left(G\right)],[\mathrm{CommSemiring}\left(k\right)],\forall C\in \mathrm{ConjClasses}\left(G\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{classSumCenter}\left(C\right)=(\mathrm{Subtype}.\mathrm{mk}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{classSum}\left(k,C\right)\right))$$

Formalization. D5/S3/FiniteGroups/FiniteCharacterAlgebra.classSumCenter (✓ 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.32 (Class sum center coe).

$$\forall G\in Type\ast ,\forall k\in Type\ast ,[\mathrm{Group}\left(G\right)],[\mathrm{Fintype}\left(G\right)],[\mathrm{DecidableEq}\left(G\right)],[\mathrm{CommSemiring}\left(k\right)],\forall C\in \mathrm{ConjClasses}\left(G\right),(\mathrm{Subtype}.\mathrm{val}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{classSumCenter}\left(C\right)\right))=(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{classSum}\left(k,C\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.classSumCenter_coe (✓ 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.

Definition 1.33 (End alg equiv self of is simple module).

$$\forall k\in Type\ast ,\forall A\in Type\ast ,\forall S\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{IsAlgClosed}\left(k\right)],[\mathrm{Ring}\left(A\right)],[\mathrm{Algebra}\left(k,A\right)],[\mathrm{AddCommGroup}\left(S\right)],[\mathrm{Module}\left(k,S\right)],[\mathrm{Module}\left(A,S\right)],[\mathrm{IsScalarTower}\left(k,A,S\right)],[\mathrm{IsSimpleModule}\left(A,S\right)],[\mathrm{FiniteDimensional}\left(k,S\right)],D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{endAlgEquivSelfOfIsSimpleModule}=(\mathrm{AlgEquiv}.\mathrm{symm}\left(\mathrm{AlgEquiv}.\mathrm{ofBijective}\left(\mathrm{Algebra}.\mathrm{ofId}\left(k,\mathrm{Module}.\mathrm{End}\left(A,S\right)\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/FiniteCharacterAlgebra.endAlgEquivSelfOfIsSimpleModule (✓ 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.34 (End alg equiv self of is simple module smul).

$$\forall k\in Type\ast ,\forall A\in Type\ast ,\forall S\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{IsAlgClosed}\left(k\right)],[\mathrm{Ring}\left(A\right)],[\mathrm{Algebra}\left(k,A\right)],[\mathrm{AddCommGroup}\left(S\right)],[\mathrm{Module}\left(k,S\right)],[\mathrm{Module}\left(A,S\right)],[\mathrm{IsScalarTower}\left(k,A,S\right)],[\mathrm{IsSimpleModule}\left(A,S\right)],[\mathrm{FiniteDimensional}\left(k,S\right)],\forall f\in \mathrm{Module}.\mathrm{End}\left(A,S\right),\forall s\in S,(\mathrm{HSMul}.\mathrm{hSMul}\left(\mathrm{DFunLike}.\mathrm{coe}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{endAlgEquivSelfOfIsSimpleModule},f\right),s\right))=(\mathrm{DFunLike}.\mathrm{coe}\left(f,s\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.endAlgEquivSelfOfIsSimpleModule_smul (✓ 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.

Definition 1.35 (Hom congr right).

$$\forall k\in Type\ast ,\forall A\in Type\ast ,[\mathrm{CommSemiring}\left(k\right)],[\mathrm{Semiring}\left(A\right)],[\mathrm{Algebra}\left(k,A\right)],\forall S\in Type\ast ,[\mathrm{AddCommMonoid}\left(S\right)],[\mathrm{Module}\left(A,S\right)],\forall N\in Type\ast ,[\mathrm{AddCommMonoid}\left(N\right)],[\mathrm{Module}\left(A,N\right)],[\mathrm{Module}\left(k,N\right)],[\mathrm{IsScalarTower}\left(k,A,N\right)],\forall P\in Type\ast ,[\mathrm{AddCommMonoid}\left(P\right)],[\mathrm{Module}\left(A,P\right)],[\mathrm{Module}\left(k,P\right)],[\mathrm{IsScalarTower}\left(k,A,P\right)],\forall e\in \mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(A\right),N,P\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{homCongrRight}\left(k,e\right)=(\mathrm{LinearEquiv}.\mathrm{mk}\left(\mathrm{LinearMap}.\mathrm{mk}\left(\mathrm{AddHom}.\mathrm{mk}\left(\mathrm{Equiv}.\mathrm{toFun}\left(\mathrm{AddEquiv}.\mathrm{toEquiv}\left(\mathrm{LinearEquiv}.\mathrm{arrowCongrAddEquiv}\left(\mathrm{LinearEquiv}.\mathrm{refl}\left(A,S\right),e\right)\right)\right)\right)\right),\mathrm{Equiv}.\mathrm{invFun}\left(\mathrm{AddEquiv}.\mathrm{toEquiv}\left(\mathrm{LinearEquiv}.\mathrm{arrowCongrAddEquiv}\left(\mathrm{LinearEquiv}.\mathrm{refl}\left(A,S\right),e\right)\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/FiniteCharacterAlgebra.homCongrRight (✓ 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.36 (Finrank linear map eq zero of is empty linear equiv).

$$\forall k\in Type\ast ,\forall A\in Type\ast ,\forall S\in Type\ast ,\forall N\in Type\ast ,[\mathrm{CommSemiring}\left(k\right)],[\mathrm{Nontrivial}\left(k\right)],[\mathrm{Ring}\left(A\right)],[\mathrm{Algebra}\left(k,A\right)],[\mathrm{AddCommGroup}\left(S\right)],[\mathrm{Module}\left(A,S\right)],[\mathrm{IsSimpleModule}\left(A,S\right)],[\mathrm{AddCommGroup}\left(N\right)],[\mathrm{Module}\left(k,N\right)],[\mathrm{Module}\left(A,N\right)],[\mathrm{IsScalarTower}\left(k,A,N\right)],[\mathrm{IsSimpleModule}\left(A,N\right)],(\mathrm{IsEmpty}\left(\mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(A\right),S,N\right)\right))\Rightarrow ((\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(A\right),S,N\right)\right))=(0))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.finrank_linearMap_eq_zero_of_isEmpty_linearEquiv (✓ 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.37 (Finrank linear map eq one of nonempty linear equiv).

$$\forall k\in Type\ast ,\forall A\in Type\ast ,\forall S\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{IsAlgClosed}\left(k\right)],[\mathrm{Ring}\left(A\right)],[\mathrm{Algebra}\left(k,A\right)],[\mathrm{AddCommGroup}\left(S\right)],[\mathrm{Module}\left(k,S\right)],[\mathrm{Module}\left(A,S\right)],[\mathrm{IsScalarTower}\left(k,A,S\right)],[\mathrm{IsSimpleModule}\left(A,S\right)],[\mathrm{FiniteDimensional}\left(k,S\right)],\forall N\in Type\ast ,[\mathrm{AddCommGroup}\left(N\right)],[\mathrm{Module}\left(k,N\right)],[\mathrm{Module}\left(A,N\right)],[\mathrm{IsScalarTower}\left(k,A,N\right)],(\mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(A\right),S,N\right))\to ((\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(A\right),S,N\right)\right))=(1))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.finrank_linearMap_eq_one_of_nonempty_linearEquiv (✓ 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.38 (Finite dimensional linear map of is simple module).

$$\forall k\in Type\ast ,\forall A\in Type\ast ,\forall S\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{IsAlgClosed}\left(k\right)],[\mathrm{Ring}\left(A\right)],[\mathrm{Algebra}\left(k,A\right)],[\mathrm{AddCommGroup}\left(S\right)],[\mathrm{Module}\left(k,S\right)],[\mathrm{Module}\left(A,S\right)],[\mathrm{IsScalarTower}\left(k,A,S\right)],[\mathrm{IsSimpleModule}\left(A,S\right)],[\mathrm{FiniteDimensional}\left(k,S\right)],\forall N\in Type\ast ,[\mathrm{AddCommGroup}\left(N\right)],[\mathrm{Module}\left(k,N\right)],[\mathrm{Module}\left(A,N\right)],[\mathrm{IsScalarTower}\left(k,A,N\right)],[\mathrm{IsSimpleModule}\left(A,N\right)],\mathrm{FiniteDimensional}\left(k,\mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(A\right),S,N\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.finiteDimensional_linearMap_of_isSimpleModule (✓ 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.39 (Nontrivial).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),(\mathrm{Representation}.\mathrm{IsIrreducible}\left(rho\right))\Rightarrow (\mathrm{Nontrivial}\left(V\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.nontrivial (✓ 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.40 (Finrank pos).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],[\mathrm{FiniteDimensional}\left(k,V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),(\mathrm{Representation}.\mathrm{IsIrreducible}\left(rho\right))\Rightarrow (\mathrm{LT}.\mathrm{lt}\left(0,\mathrm{Module}.\mathrm{finrank}\left(k,V\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.finrank_pos (✓ 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.41 (Is irreducible of finrank eq one).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),((\mathrm{Module}.\mathrm{finrank}\left(k,V\right))=(1))\Rightarrow (\mathrm{Representation}.\mathrm{IsIrreducible}\left(rho\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.isIrreducible_of_finrank_eq_one (✓ 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.42 (Is irreducible to representation of is atom).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),\forall sigma\in \mathrm{Subrepresentation}\left(rho\right),(\mathrm{IsAtom}\left(sigma\right))\Rightarrow (\mathrm{Representation}.\mathrm{IsIrreducible}\left(\mathrm{Subrepresentation}.\mathrm{toRepresentation}\left(sigma\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.isIrreducible_toRepresentation_of_isAtom (✓ 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.43 (As algebra hom surjective of is irreducible).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],[\mathrm{IsAlgClosed}\left(k\right)],[\mathrm{FiniteDimensional}\left(k,V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),(\mathrm{Representation}.\mathrm{IsIrreducible}\left(rho\right))\Rightarrow (\mathrm{Function}.\mathrm{Surjective}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{Representation}.\mathrm{asAlgebraHom}\left(rho\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.asAlgebraHom_surjective_of_isIrreducible (✓ 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.44 (Exists is atom).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{DivisionRing}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],[\mathrm{FiniteDimensional}\left(k,V\right)],[\mathrm{Nontrivial}\left(V\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),\exists sigma\in \mathrm{Subrepresentation}\left(rho\right),\mathrm{IsAtom}\left(sigma\right)$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/FiniteCharacterAlgebra.exists_isAtom (✓ 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.

Definition 1.45 (Character pairing).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{Fintype}\left(G\right)],D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{characterPairing}=(\mathrm{LinearMap}.{\mathrm{mk}}_2\left(k,\lambda (f1:\mathrm{Subtype}\left(\lambda (x:(G)\to (k))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,G\right),x\right))\right))\mapsto (\lambda (f2:\mathrm{Subtype}\left(\lambda (x:(G)\to (k))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,G\right),x\right))\right))\mapsto (\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Nat}.\mathrm{card}\left(G\right)\right)\right),\mathrm{Finset}.\mathrm{sum}\left(\mathrm{Finset}.\mathrm{univ},\lambda (g:G)\mapsto (\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Subtype}.\mathrm{val}\left(f1,g\right),\mathrm{Subtype}.\mathrm{val}\left(f2,\mathrm{Inv}.\mathrm{inv}\left(g\right)\right)\right))\right)\right)))\right))$$

Formalization. D5/S3/FiniteGroups/FiniteCharacterAlgebra.characterPairing (✓ 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.46 (Character pairing apply).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{Fintype}\left(G\right)],\forall f1\in \mathrm{Subtype}\left(\lambda (x:(G)\to (k))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,G\right),x\right))\right),\forall f2\in \mathrm{Subtype}\left(\lambda (x:(G)\to (k))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,G\right),x\right))\right),(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{DFunLike}.\mathrm{coe}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{characterPairing},f1\right),f2\right))=(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Nat}.\mathrm{card}\left(G\right)\right)\right),\mathrm{Finset}.\mathrm{sum}\left(\mathrm{Finset}.\mathrm{univ},\lambda (g:G)\mapsto (\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Subtype}.\mathrm{val}\left(f1,g\right),\mathrm{Subtype}.\mathrm{val}\left(f2,\mathrm{Inv}.\mathrm{inv}\left(g\right)\right)\right))\right)\right))$$