Clifford Decomposition

Abstract

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

Theorem 1.1 (Is unit nat card subgroup).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Semiring}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall S\in \mathrm{Subgroup}\left(G\right),(\mathrm{IsUnit}\left(\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Nat}.\mathrm{card}\left(G\right)\right)\right))\Rightarrow (\mathrm{IsUnit}\left(\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Nat}.\mathrm{card}\left(\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right)\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordDecomposition.isUnit_natCard_subgroup (✓ 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 (Trace pi of apply eq).

$$\forall k\in Type\ast ,\forall iota\in Type\ast ,\forall M\in Type\ast ,[\mathrm{CommRing}\left(k\right)],[\mathrm{Fintype}\left(iota\right)],[\mathrm{AddCommGroup}\left(M\right)],[\mathrm{Module}\left(k,M\right)],[\mathrm{Module}.\mathrm{Free}\left(k,M\right)],[\mathrm{Module}.\mathrm{Finite}\left(k,M\right)],\forall T\in \mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(k\right),(iota)\to (M),(iota)\to (M)\right),\forall sigma\in (iota)\to (iota),\forall f\in (iota)\to (\mathrm{LinearMap}\left(\mathrm{RingHom}.\mathrm{id}\left(k\right),M,M\right)),(\forall x\in (iota)\to (M),\forall i\in iota,(\mathrm{DFunLike}.\mathrm{coe}\left(T,x,i\right))=(\mathrm{DFunLike}.\mathrm{coe}\left(f\left(i\right),x\left(sigma\left(i\right)\right)\right)))\Rightarrow ((\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{LinearMap}.\mathrm{trace}\left(k,(iota)\to (M)\right),T\right))=(\mathrm{Finset}.\mathrm{sum}\left(\mathrm{Finset}.\mathrm{univ},\lambda (i:iota)\mapsto (\mathrm{ite}\left((sigma\left(i\right))=(i),\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{LinearMap}.\mathrm{trace}\left(k,M\right),f\left(i\right)\right),0\right))\right)))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordDecomposition.trace_pi_of_apply_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.3 (Clifford sum).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],\forall V\in \mathrm{FDRep}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right),[\mathrm{Finite}\left(\mathrm{HasQuotient}.\mathrm{Quotient}\left(G,\mathrm{MulAction}.\mathrm{stabilizer}\left(G,\mathrm{CategoryTheory}.\mathrm{toSkeleton}\left(V\right)\right)\right)\right)],\forall e\in \mathrm{Nat},D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordDecomposition}.\mathrm{FDRep}.\mathrm{cliffordSum}\left(V,e\right)=(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{FDRep}.\mathrm{ofShrink}\left(\mathrm{Representation}.{\mathrm{ofModule}}^{\prime }\left(\forall q\in \mathrm{HasQuotient}.\mathrm{Quotient}\left(G,\mathrm{MulAction}.\mathrm{stabilizer}\left(G,\mathrm{CategoryTheory}.\mathrm{toSkeleton}\left(V\right)\right)\right),(\mathrm{Fin}\left(e\right))\to (\mathrm{Representation}.\mathrm{asModule}\left(\mathrm{FDRep}.\rho \left(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{conjNormalFDRepFunctor}\left(\mathrm{Quotient}.\mathrm{out}\left(q\right)\right),V\right)\right)\right))\right)\right))$$

Formalization. D5/S3/FiniteGroups/CliffordDecomposition.cliffordSum (✓ 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 (Finrank clifford sum).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],\forall V\in \mathrm{FDRep}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right),[\mathrm{Finite}\left(\mathrm{HasQuotient}.\mathrm{Quotient}\left(G,\mathrm{MulAction}.\mathrm{stabilizer}\left(G,\mathrm{CategoryTheory}.\mathrm{toSkeleton}\left(V\right)\right)\right)\right)],\forall e\in \mathrm{Nat},(\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{FGModuleCat}.\mathrm{carrier}\left(\mathrm{Action}.V\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordDecomposition}.\mathrm{FDRep}.\mathrm{cliffordSum}\left(V,e\right)\right)\right)\right))=(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Nat}.\mathrm{card}\left(\mathrm{HasQuotient}.\mathrm{Quotient}\left(G,\mathrm{MulAction}.\mathrm{stabilizer}\left(G,\mathrm{CategoryTheory}.\mathrm{toSkeleton}\left(V\right)\right)\right)\right),e\right),\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{FGModuleCat}.\mathrm{carrier}\left(\mathrm{Action}.V\left(V\right)\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordDecomposition.finrank_cliffordSum (✓ 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 (Character clifford sum).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],\forall V\in \mathrm{FDRep}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right),[\mathrm{Finite}\left(\mathrm{HasQuotient}.\mathrm{Quotient}\left(G,\mathrm{MulAction}.\mathrm{stabilizer}\left(G,\mathrm{CategoryTheory}.\mathrm{toSkeleton}\left(V\right)\right)\right)\right)],\forall e\in \mathrm{Nat},\forall x\in \mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right),(\mathrm{FDRep}.\mathrm{character}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordDecomposition}.\mathrm{FDRep}.\mathrm{cliffordSum}\left(V,e\right),x\right))=(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Nat}.\mathrm{cast}\left(e\right),\mathrm{finsum}\left(\lambda (q:\mathrm{HasQuotient}.\mathrm{Quotient}\left(G,\mathrm{MulAction}.\mathrm{stabilizer}\left(G,\mathrm{CategoryTheory}.\mathrm{toSkeleton}\left(V\right)\right)\right))\mapsto (\mathrm{FDRep}.\mathrm{character}\left(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordConstituents}.\mathrm{TauCeti}.\mathrm{conjNormalFDRepFunctor}\left(\mathrm{Quotient}.\mathrm{out}\left(q\right)\right),V\right),x\right))\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/CliffordDecomposition.character_cliffordSum (✓ 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 (Clifford restrict iso).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall N\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{Normal}\left(N\right)],[\mathrm{IsAlgClosed}\left(k\right)],\forall W\in \mathrm{FDRep}\left(k,G\right),[\mathrm{CategoryTheory}.\mathrm{Simple}\left(W\right)],\exists V\in \mathrm{FDRep}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(N,x\right))\right)\right),\exists [\mathrm{CategoryTheory}.\mathrm{Simple}\left(V\right)],\exists [\mathrm{Finite}\left(\mathrm{HasQuotient}.\mathrm{Quotient}\left(G,\mathrm{MulAction}.\mathrm{stabilizer}\left(G,\mathrm{CategoryTheory}.\mathrm{toSkeleton}\left(V\right)\right)\right)\right)],\exists e\in \mathrm{Nat},(\mathrm{Ne}\left(e,0\right))\wedge (\mathrm{Nonempty}\left(\mathrm{CategoryTheory}.\mathrm{Iso}\left(\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(\mathrm{Action}.\mathrm{res}\left(\mathrm{FGModuleCat}\left(k\right),\mathrm{Subgroup}.\mathrm{subtype}\left(N\right)\right),W\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{CliffordDecomposition}.\mathrm{FDRep}.\mathrm{cliffordSum}\left(V,e\right)\right)\right))$$

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

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

Commentary.

The displayed conclusion holds under the stated hypotheses.

References

• Truth anchor: D5/S3/FiniteGroups/CliffordDecomposition.character_cliffordSum
• Truth anchor: D5/S3/FiniteGroups/CliffordDecomposition.cliffordSum
• Truth anchor: D5/S3/FiniteGroups/CliffordDecomposition.clifford_restrict_iso
• Truth anchor: D5/S3/FiniteGroups/CliffordDecomposition.finrank_cliffordSum
• Truth anchor: D5/S3/FiniteGroups/CliffordDecomposition.isUnit_natCard_subgroup
• Truth anchor: D5/S3/FiniteGroups/CliffordDecomposition.trace_pi_of_apply_eq
• Dependency: D5/S3/FiniteGroups/CliffordConstituents
• Dependency: D5/S3/FiniteGroups/FiniteCharacterAlgebra