Clifford Constituents

Abstract

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

Theorem 1.1 (Mem conj smul).

$$\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall s\in G,\forall H\in \mathrm{Subgroup}\left(G\right),\forall x\in G,(\mathrm{Membership}.\mathrm{mem}\left(\mathrm{HSMul}.\mathrm{hSMul}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MulAut}.\mathrm{conj},s\right),H\right),x\right))\iff (\mathrm{Membership}.\mathrm{mem}\left(H,\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(s\right),x\right),s\right)\right))$$

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

Theorem 1.2 (Conj mul smul).

$$\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall s\in G,\forall t\in G,\forall H\in \mathrm{Subgroup}\left(G\right),(\mathrm{HSMul}.\mathrm{hSMul}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MulAut}.\mathrm{conj},\mathrm{HMul}.\mathrm{hMul}\left(s,t\right)\right),H\right))=(\mathrm{HSMul}.\mathrm{hSMul}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MulAut}.\mathrm{conj},s\right),\mathrm{HSMul}.\mathrm{hSMul}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MulAut}.\mathrm{conj},t\right),H\right)\right))$$

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

Theorem 1.3 (Coe conj subgroup equiv apply).

$$\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall s\in G,\forall H\in \mathrm{Subgroup}\left(G\right),\forall x\in \mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{HSMul}.\mathrm{hSMul}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MulAut}.\mathrm{conj},s\right),H\right),x\right))\right),(\mathrm{Subtype}.\mathrm{val}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MulEquiv}.\mathrm{symm}\left(\mathrm{Subgroup}.\mathrm{equivSMul}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MulAut}.\mathrm{conj},s\right),H\right)\right),x\right)\right))=(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(s\right),\mathrm{Subtype}.\mathrm{val}\left(x\right)\right),s\right))$$

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

Definition 1.4 (Conj normal fdr ep functor).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],[\mathrm{Ring}\left(k\right)],\forall g\in G,D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{conjNormalFDRepFunctor}\left(g\right)=(\mathrm{Action}.\mathrm{res}\left(\mathrm{FGModuleCat}\left(k\right),\mathrm{MulEquiv}.\mathrm{toMonoidHom}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MulAut}.\mathrm{conjNormal},\mathrm{Inv}.\mathrm{inv}\left(g\right)\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.conjNormalFDRepFunctor (✓ 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.5 (Conj normal fdr ep equiv).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],[\mathrm{Ring}\left(k\right)],\forall g\in G,D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{conjNormalFDRepEquiv}\left(g\right)=(\mathrm{Action}.\mathrm{resEquiv}\left(\mathrm{FGModuleCat}\left(k\right),\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MulAut}.\mathrm{conjNormal},\mathrm{Inv}.\mathrm{inv}\left(g\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.conjNormalFDRepEquiv (✓ 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.6 (Conj normal fdr ep equiv functor).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],[\mathrm{Ring}\left(k\right)],\forall g\in G,(\mathrm{CategoryTheory}.\mathrm{Equivalence}.\mathrm{functor}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{conjNormalFDRepEquiv}\left(g\right)\right))=(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{conjNormalFDRepFunctor}\left(g\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.conjNormalFDRepEquiv_functor (✓ 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.7 (Conj normal fdr ep skeleton sm ul).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],[\mathrm{Ring}\left(k\right)],D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{conjNormalFDRepSkeletonSMul}=(\mathrm{SMul}.\mathrm{mk}\left(\lambda (g:G)\mapsto (\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{mapSkeleton}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{conjNormalFDRepFunctor}\left(g\right)\right)\right))\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.conjNormalFDRepSkeletonSMul (✓ 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.8 (Smul to skeleton).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],[\mathrm{Ring}\left(k\right)],\forall g\in G,\forall A\in \mathrm{FDRep}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right),(\mathrm{HSMul}.\mathrm{hSMul}\left(g,\mathrm{CategoryTheory}.\mathrm{toSkeleton}\left(A\right)\right))=(\mathrm{CategoryTheory}.\mathrm{toSkeleton}\left(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{conjNormalFDRepFunctor}\left(g\right),A\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.smul_toSkeleton (✓ 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.9 (Conj normal fdr ep skeleton mul action).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],[\mathrm{Ring}\left(k\right)],D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{conjNormalFDRepSkeletonMulAction}=(\mathrm{MulAction}.\mathrm{mk}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{conjNormalFDRepSkeletonSMul}\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.conjNormalFDRepSkeletonMulAction (✓ 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.10 (Char conj normal fdr ep).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],[\mathrm{Field}\left(k\right)],\forall g\in G,\forall A\in \mathrm{FDRep}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right),\forall x\in \mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right),(\mathrm{FDRep}.\mathrm{character}\left(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{conjNormalFDRepFunctor}\left(g\right),A\right),x\right))=(\mathrm{FDRep}.\mathrm{character}\left(A,\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{MulAut}.\mathrm{conjNormal},\mathrm{Inv}.\mathrm{inv}\left(g\right)\right),x\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.char_conjNormalFDRep (✓ 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.11 (Conj subrep).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Semiring}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{AddCommMonoid}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),\forall g\in G,\forall sigma\in \mathrm{Subrepresentation}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{Representation}.\mathrm{conjSubrep}\left(rho,g,sigma\right)=(\mathrm{Subrepresentation}.\mathrm{mk}\left(\mathrm{Submodule}.\mathrm{map}\left(\mathrm{DFunLike}.\mathrm{coe}\left(rho,g\right),\mathrm{Subrepresentation}.\mathrm{toSubmodule}\left(sigma\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.conjSubrep (✓ 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.12 (Is atom conj subrep iff).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Semiring}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{AddCommMonoid}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),\forall g\in G,\forall sigma\in \mathrm{Subrepresentation}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right),(\mathrm{IsAtom}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{Representation}.\mathrm{conjSubrep}\left(rho,g,sigma\right)\right))\iff (\mathrm{IsAtom}\left(sigma\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.isAtom_conjSubrep_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.13 (Conj subrep equiv).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Semiring}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{AddCommMonoid}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),\forall g\in G,\forall sigma\in \mathrm{Subrepresentation}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{Representation}.\mathrm{conjSubrepEquiv}\left(rho,g,sigma\right)=(\mathrm{Representation}.\mathrm{Equiv}.\mathrm{mk}\left(\mathrm{Submodule}.\mathrm{equivMapOfInjective}\left(\mathrm{DFunLike}.\mathrm{coe}\left(rho,g\right),\mathrm{Subrepresentation}.\mathrm{toSubmodule}\left(sigma\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.conjSubrepEquiv (✓ 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 (Is semisimple representation comp subtype).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),[\mathrm{Representation}.\mathrm{IsIrreducible}\left(rho\right)],[\mathrm{FiniteDimensional}\left(k,V\right)],\mathrm{Representation}.\mathrm{IsSemisimpleRepresentation}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.isSemisimpleRepresentation_comp_subtype (✓ 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 (Exists nonempty linear equiv as submodule conj subrep).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),[\mathrm{Representation}.\mathrm{IsIrreducible}\left(rho\right)],\forall sigma\in \mathrm{Subrepresentation}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right),(\mathrm{IsAtom}\left(sigma\right))\Rightarrow (\forall T\in \mathrm{Submodule}\left(\mathrm{MonoidAlgebra}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right),\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right)\right),[\mathrm{IsSimpleModule}\left(\mathrm{MonoidAlgebra}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right),\mathrm{Subtype}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(T,x\right))\right)\right)],\exists g\in G,\mathrm{Nonempty}\left(\mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(\mathrm{MonoidAlgebra}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right)\right),\mathrm{Subtype}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(T,x\right))\right),\mathrm{Subtype}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subrepresentation}.\mathrm{asSubmodule}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{Representation}.\mathrm{conjSubrep}\left(rho,g,sigma\right)\right),x\right))\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.exists_nonempty_linearEquiv_asSubmodule_conjSubrep (✓ 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.16 (Exists is atom forall nonempty linear equiv conj subrep).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),[\mathrm{Representation}.\mathrm{IsIrreducible}\left(rho\right)],[\mathrm{FiniteDimensional}\left(k,V\right)],\exists sigma\in \mathrm{Subrepresentation}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right),(\mathrm{IsAtom}\left(sigma\right))\wedge (\forall tau\in \mathrm{Subrepresentation}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right),(\mathrm{IsAtom}\left(tau\right))\Rightarrow (\exists g\in G,\mathrm{Nonempty}\left(\mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(\mathrm{MonoidAlgebra}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right)\right),\mathrm{Subtype}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subrepresentation}.\mathrm{asSubmodule}\left(tau\right),x\right))\right),\mathrm{Subtype}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subrepresentation}.\mathrm{asSubmodule}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{Representation}.\mathrm{conjSubrep}\left(rho,g,sigma\right)\right),x\right))\right)\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.exists_isAtom_forall_nonempty_linearEquiv_conjSubrep (✓ 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.17 (Conj subrep isotypic component).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),[\mathrm{Representation}.\mathrm{IsIrreducible}\left(rho\right)],\forall sigma\in \mathrm{Subrepresentation}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right),\forall hsigma\in \mathrm{IsAtom}\left(sigma\right),\forall g\in G,D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{Representation}.\mathrm{conjSubrepIsotypicComponent}\left(rho,sigma,hsigma,g\right)=(\mathrm{Subtype}.\mathrm{mk}\left(\mathrm{isotypicComponent}\left(\mathrm{MonoidAlgebra}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right),\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right),\mathrm{Subtype}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subrepresentation}.\mathrm{asSubmodule}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{Representation}.\mathrm{conjSubrep}\left(rho,g,sigma\right)\right),x\right))\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.conjSubrepIsotypicComponent (✓ 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.18 (Coe conj subrep isotypic component).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),[\mathrm{Representation}.\mathrm{IsIrreducible}\left(rho\right)],\forall sigma\in \mathrm{Subrepresentation}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right),(\mathrm{IsAtom}\left(sigma\right))\Rightarrow (\forall g\in G,(\mathrm{Subtype}.\mathrm{val}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{Representation}.\mathrm{conjSubrepIsotypicComponent}\left(rho,sigma,g\right)\right))=(\mathrm{isotypicComponent}\left(\mathrm{MonoidAlgebra}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right),\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right),\mathrm{Subtype}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subrepresentation}.\mathrm{asSubmodule}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{Representation}.\mathrm{conjSubrep}\left(rho,g,sigma\right)\right),x\right))\right)\right)))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.coe_conjSubrepIsotypicComponent (✓ 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.19 (Simple submodule classes).

$$\forall R\in Type\ast ,[\mathrm{Ring}\left(R\right)],\forall M\in Type\ast ,[\mathrm{AddCommGroup}\left(M\right)],[\mathrm{Module}\left(R,M\right)],D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{SimpleSubmoduleClasses}\left(R,M\right)=(\mathrm{Quot}\left(\lambda (N:\mathrm{Subtype}\left(\lambda (N:\mathrm{Submodule}\left(R,M\right))\mapsto (\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right))\right))\mapsto (\lambda (NPrime:\mathrm{Subtype}\left(\lambda (N:\mathrm{Submodule}\left(R,M\right))\mapsto (\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right))\right))\mapsto (\mathrm{Nonempty}\left(\mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(R\right),\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subtype}.\mathrm{val}\left(N\right),x\right))\right),\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subtype}.\mathrm{val}\left(NPrime\right),x\right))\right)\right)\right)))\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.SimpleSubmoduleClasses (✓ 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.20 (Mk).

$$\forall R\in Type\ast ,[\mathrm{Ring}\left(R\right)],\forall M\in Type\ast ,[\mathrm{AddCommGroup}\left(M\right)],[\mathrm{Module}\left(R,M\right)],\forall N\in \mathrm{Submodule}\left(R,M\right),[\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right)],D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{SimpleSubmoduleClasses}.\mathrm{mk}\left(N\right)=(\mathrm{Quot}.\mathrm{mk}\left(\lambda (N:\mathrm{Subtype}\left(\lambda (N:\mathrm{Submodule}\left(R,M\right))\mapsto (\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right))\right))\mapsto (\lambda (NPrime:\mathrm{Subtype}\left(\lambda (N:\mathrm{Submodule}\left(R,M\right))\mapsto (\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right))\right))\mapsto (\mathrm{Nonempty}\left(\mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(R\right),\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subtype}.\mathrm{val}\left(N\right),x\right))\right),\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subtype}.\mathrm{val}\left(NPrime\right),x\right))\right)\right)\right))),\mathrm{Subtype}.\mathrm{mk}\left(N\right)\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.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 formula defines the displayed algebraic construction.

Theorem 1.21 (Mk eq mk iff).

$$\forall R\in Type\ast ,[\mathrm{Ring}\left(R\right)],\forall M\in Type\ast ,[\mathrm{AddCommGroup}\left(M\right)],[\mathrm{Module}\left(R,M\right)],\forall N\in \mathrm{Submodule}\left(R,M\right),\forall NPrime\in \mathrm{Submodule}\left(R,M\right),[\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right)],[\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(NPrime,x\right))\right)\right)],((D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{SimpleSubmoduleClasses}.\mathrm{mk}\left(N\right))=(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{SimpleSubmoduleClasses}.\mathrm{mk}\left(NPrime\right)))\iff (\mathrm{Nonempty}\left(\mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(R\right),\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right),\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(NPrime,x\right))\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.mk_eq_mk_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.22 (Ind).

$$\forall R\in Type\ast ,[\mathrm{Ring}\left(R\right)],\forall M\in Type\ast ,[\mathrm{AddCommGroup}\left(M\right)],[\mathrm{Module}\left(R,M\right)],\forall motive\in (D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{SimpleSubmoduleClasses}\left(R,M\right))\to (Prop),(\forall N\in \mathrm{Submodule}\left(R,M\right),(\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right))\Rightarrow (motive\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{SimpleSubmoduleClasses}.\mathrm{mk}\left(N\right)\right)))\Rightarrow (\forall c\in D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{SimpleSubmoduleClasses}\left(R,M\right),motive\left(c\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.ind (✓ 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 (Lift).

$$\forall R\in Type\ast ,[\mathrm{Ring}\left(R\right)],\forall M\in Type\ast ,[\mathrm{AddCommGroup}\left(M\right)],[\mathrm{Module}\left(R,M\right)],\forall alpha\in Sort\ast ,\forall f\in \left(\forall N\in \mathrm{Submodule}\left(R,M\right),[\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right)],alpha\right),\forall hf\in \left(\forall N\in \mathrm{Submodule}\left(R,M\right),\forall NPrime\in \mathrm{Submodule}\left(R,M\right),[\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right)],[\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(NPrime,x\right))\right)\right)],(\mathrm{Nonempty}\left(\mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(R\right),\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right),\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(NPrime,x\right))\right)\right)\right))\Rightarrow ((f\left(N\right))=(f\left(NPrime\right)))\right),\forall c\in D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{SimpleSubmoduleClasses}\left(R,M\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{SimpleSubmoduleClasses}.\mathrm{lift}\left(f,hf,c\right)=(\mathrm{Quot}.\mathrm{lift}\left(\lambda (N:\mathrm{Subtype}\left(\lambda (N:\mathrm{Submodule}\left(R,M\right))\mapsto (\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right))\right))\mapsto (f\left(\mathrm{Subtype}.\mathrm{val}\left(N\right)\right)),c\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.lift (✓ 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 (Lift mk).

$$\forall R\in Type\ast ,[\mathrm{Ring}\left(R\right)],\forall M\in Type\ast ,[\mathrm{AddCommGroup}\left(M\right)],[\mathrm{Module}\left(R,M\right)],\forall alpha\in Sort\ast ,\forall f\in \left(\forall N\in \mathrm{Submodule}\left(R,M\right),[\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right)],alpha\right),(\forall N\in \mathrm{Submodule}\left(R,M\right),\forall NPrime\in \mathrm{Submodule}\left(R,M\right),[\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right)],[\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(NPrime,x\right))\right)\right)],(\mathrm{Nonempty}\left(\mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(R\right),\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right),\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(NPrime,x\right))\right)\right)\right))\Rightarrow ((f\left(N\right))=(f\left(NPrime\right))))\Rightarrow (\forall N\in \mathrm{Submodule}\left(R,M\right),[\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right)],(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{SimpleSubmoduleClasses}.\mathrm{lift}\left(f,D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{SimpleSubmoduleClasses}.\mathrm{mk}\left(N\right)\right))=(f\left(N\right)))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.lift_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.25 (Simple submodule classes equiv).

$$\forall R\in Type\ast ,[\mathrm{Ring}\left(R\right)],\forall M\in Type\ast ,[\mathrm{AddCommGroup}\left(M\right)],[\mathrm{Module}\left(R,M\right)],D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{simpleSubmoduleClassesEquiv}\left(R,M\right)=(\mathrm{Equiv}.\mathrm{ofBijective}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{SimpleSubmoduleClasses}.\mathrm{lift}\left(\lambda (N:\mathrm{Submodule}\left(R,M\right))\mapsto (\mathrm{Function}.\mathrm{const}\left(\mathrm{IsSimpleModule}\left(R,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right),\mathrm{Subtype}.\mathrm{mk}\left(\mathrm{isotypicComponent}\left(R,M,\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right)\right)\right))\right)\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.simpleSubmoduleClassesEquiv (✓ 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.26 (Nonempty linear equiv isotypic component).

$$\forall k\in Type\ast ,\forall A\in Type\ast ,\forall M\in Type\ast ,\forall S\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Ring}\left(A\right)],[\mathrm{Algebra}\left(k,A\right)],[\mathrm{AddCommGroup}\left(M\right)],[\mathrm{Module}\left(k,M\right)],[\mathrm{Module}\left(A,M\right)],[\mathrm{IsScalarTower}\left(k,A,M\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{IsAlgClosed}\left(k\right)],[\mathrm{FiniteDimensional}\left(k,S\right)],[\mathrm{FiniteDimensional}\left(k,M\right)],\mathrm{Nonempty}\left(\mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(A\right),\mathrm{Subtype}\left(\lambda (x:M)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{isotypicComponent}\left(A,M,S\right),x\right))\right),(\mathrm{Fin}\left(\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(A\right),S,M\right)\right)\right))\to (S)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.nonempty_linearEquiv_isotypicComponent (✓ 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 (Exists forall finrank linear map eq).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(k,V\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),[\mathrm{Representation}.\mathrm{IsIrreducible}\left(rho\right)],[\mathrm{FiniteDimensional}\left(k,V\right)],\exists e\in \mathrm{Nat},(\mathrm{LT}.\mathrm{lt}\left(0,e\right))\wedge (\forall sigma\in \mathrm{Subrepresentation}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right),(\mathrm{IsAtom}\left(sigma\right))\Rightarrow ((\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(\mathrm{MonoidAlgebra}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right)\right),\mathrm{Subtype}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subrepresentation}.\mathrm{asSubmodule}\left(sigma\right),x\right))\right),\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{MonoidHom}.\mathrm{comp}\left(rho,\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right)\right)\right)\right))=(e)))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.exists_forall_finrank_linearMap_eq (✓ 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.28 (Equiv of as module linear equiv).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,\forall W\in Type\ast ,[\mathrm{CommSemiring}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommMonoid}\left(V\right)],[\mathrm{Module}\left(k,V\right)],[\mathrm{AddCommMonoid}\left(W\right)],[\mathrm{Module}\left(k,W\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),\forall sigma\in \mathrm{Representation}\left(k,G,W\right),\forall f\in \mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(\mathrm{MonoidAlgebra}\left(k,G\right)\right),\mathrm{Representation}.\mathrm{asModule}\left(rho\right),\mathrm{Representation}.\mathrm{asModule}\left(sigma\right)\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{Representation}.\mathrm{equivOfAsModuleLinearEquiv}\left(f\right)=(\mathrm{Representation}.\mathrm{IntertwiningMap}.\mathrm{ofBijective}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{LinearEquiv}.\mathrm{symm}\left(\mathrm{Representation}.\mathrm{IntertwiningMap}.\mathrm{equivLinearMapAsModule}\left(rho,sigma\right)\right),\mathrm{LinearEquiv}.\mathrm{toLinearMap}\left(f\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.equivOfAsModuleLinearEquiv (✓ 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.29 (As module linear equiv of equiv).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,\forall V\in Type\ast ,\forall W\in Type\ast ,[\mathrm{CommSemiring}\left(k\right)],[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommMonoid}\left(V\right)],[\mathrm{Module}\left(k,V\right)],[\mathrm{AddCommMonoid}\left(W\right)],[\mathrm{Module}\left(k,W\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),\forall sigma\in \mathrm{Representation}\left(k,G,W\right),\forall phi\in \mathrm{Representation}.\mathrm{Equiv}\left(rho,sigma\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{Representation}.\mathrm{asModuleLinearEquivOfEquiv}\left(phi\right)=(\mathrm{LinearEquiv}.\mathrm{ofBijective}\left(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{Representation}.\mathrm{IntertwiningMap}.\mathrm{equivLinearMapAsModule}\left(rho,sigma\right),\mathrm{Representation}.\mathrm{Equiv}.\mathrm{toIntertwiningMap}\left(phi\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.asModuleLinearEquivOfEquiv (✓ 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.30 (Fd rep iso of as module linear equiv).

$$\forall k\in Type\ast ,\forall V\in Type\ast ,\forall W\in Type\ast ,\forall G\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)],[\mathrm{AddCommGroup}\left(W\right)],[\mathrm{Module}\left(k,W\right)],[\mathrm{Module}.\mathrm{Finite}\left(k,W\right)],\forall rho\in \mathrm{Representation}\left(k,G,V\right),\forall sigma\in \mathrm{Representation}\left(k,G,W\right),\forall f\in \mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(\mathrm{MonoidAlgebra}\left(k,G\right)\right),\mathrm{Representation}.\mathrm{asModule}\left(rho\right),\mathrm{Representation}.\mathrm{asModule}\left(sigma\right)\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{fdRepIsoOfAsModuleLinearEquiv}\left(f\right)=(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{preimageIso}\left(\mathrm{CategoryTheory}.{\mathrm{forget}}_2\left(\mathrm{FDRep}\left(k,G\right),\mathrm{Rep}\left(k,G\right)\right),\mathrm{Rep}.\mathrm{mkIso}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{Representation}.\mathrm{equivOfAsModuleLinearEquiv}\left(f\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/CliffordConstituents.fdRepIsoOfAsModuleLinearEquiv (✓ 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.31 (Nonempty fd rep iso iff).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{CommRing}\left(k\right)],[\mathrm{Monoid}\left(G\right)],\forall X\in \mathrm{FDRep}\left(k,G\right),\forall Y\in \mathrm{FDRep}\left(k,G\right),(\mathrm{Nonempty}\left(\mathrm{CategoryTheory}.\mathrm{Iso}\left(X,Y\right)\right))\iff (\mathrm{Nonempty}\left(\mathrm{Representation}.\mathrm{Equiv}\left(\mathrm{FDRep}.\rho \left(X\right),\mathrm{FDRep}.\rho \left(Y\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordConstituents.nonempty_fdRepIso_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.32 (To skeleton fd rep of to representation eq iff).

$$\forall G\in Type\ast ,[\mathrm{Monoid}\left(G\right)],\forall K\in Type\ast ,\forall X\in Type\ast ,[\mathrm{CommRing}\left(K\right)],[\mathrm{AddCommGroup}\left(X\right)],[\mathrm{Module}\left(K,X\right)],\forall pi\in \mathrm{Representation}\left(K,G,X\right),\forall S\in \mathrm{Subrepresentation}\left(pi\right),\forall T\in \mathrm{Subrepresentation}\left(pi\right),[\mathrm{Module}.\mathrm{Finite}\left(K,\mathrm{Subtype}\left(\lambda (x:X)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subrepresentation}.\mathrm{toSubmodule}\left(S\right),x\right))\right)\right)],[\mathrm{Module}.\mathrm{Finite}\left(K,\mathrm{Subtype}\left(\lambda (x:X)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subrepresentation}.\mathrm{toSubmodule}\left(T\right),x\right))\right)\right)],((\mathrm{CategoryTheory}.\mathrm{toSkeleton}\left(\mathrm{FDRep}.\mathrm{of}\left(\mathrm{Subrepresentation}.\mathrm{toRepresentation}\left(S\right)\right)\right))=(\mathrm{CategoryTheory}.\mathrm{toSkeleton}\left(\mathrm{FDRep}.\mathrm{of}\left(\mathrm{Subrepresentation}.\mathrm{toRepresentation}\left(T\right)\right)\right)))\iff (\mathrm{Nonempty}\left(\mathrm{LinearEquiv}\left(\mathrm{RingHom}.\mathrm{id}\left(\mathrm{MonoidAlgebra}\left(K,G\right)\right),\mathrm{Subtype}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(pi\right))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subrepresentation}.\mathrm{asSubmodule}\left(S\right),x\right))\right),\mathrm{Subtype}\left(\lambda (x:\mathrm{Representation}.\mathrm{asModule}\left(pi\right))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(\mathrm{Subrepresentation}.\mathrm{asSubmodule}\left(T\right),x\right))\right)\right)\right))$$