Induced Character Formula

Abstract

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

Theorem 1.1 (Clifford restrict finrank).

$$\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))\wedge ((\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{FGModuleCat}.\mathrm{carrier}\left(\mathrm{Action}.V\left(W\right)\right)\right))=(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(e,\mathrm{Subgroup}.\mathrm{index}\left(\mathrm{MulAction}.\mathrm{stabilizer}\left(G,\mathrm{CategoryTheory}.\mathrm{toSkeleton}\left(V\right)\right)\right)\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/InducedCharacterFormula.clifford_restrict_finrank (✓ 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 (Char eq finrank iff).

$$\forall G\in Type\ast ,\forall V\in Type\ast ,[\mathrm{Monoid}\left(G\right)],[\mathrm{AddCommGroup}\left(V\right)],[\mathrm{Module}\left(\mathrm{Complex},V\right)],[\mathrm{FiniteDimensional}\left(\mathrm{Complex},V\right)],\forall rho\in \mathrm{Representation}\left(\mathrm{Complex},G,V\right),\forall g\in G,(\mathrm{IsOfFinOrder}\left(g\right))\Rightarrow (((\mathrm{Representation}.\mathrm{character}\left(rho,g\right))=(\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Module}.\mathrm{finrank}\left(\mathrm{Complex},V\right)\right)))\iff ((\mathrm{DFunLike}.\mathrm{coe}\left(rho,g\right))=(1)))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/InducedCharacterFormula.char_eq_finrank_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.3 (Stabilizer quotient group mk).

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

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

Theorem 1.4 (Double coset mk eq mk one iff mem).

$$\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall H\in \mathrm{Subgroup}\left(G\right),\forall s\in G,((\mathrm{DoubleCoset}.\mathrm{mk}\left(H,H,s\right))=(\mathrm{DoubleCoset}.\mathrm{mk}\left(H,H,1\right)))\iff (\mathrm{Membership}.\mathrm{mem}\left(H,s\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/InducedCharacterFormula.doubleCosetMk_eq_mk_one_iff_mem (✓ 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.5 (Ind term).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall S\in \mathrm{Subgroup}\left(G\right),[\mathrm{AddCommMonoid}\left(k\right)],\forall f\in (\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right))\to (k),\forall g\in G,\forall x\in G,D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indTerm}\left(f,g,x\right)=(\mathrm{dite}\left(\mathrm{Membership}.\mathrm{mem}\left(S,\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(x\right),g\right),x\right)\right),\mathrm{Function}.\mathrm{const}\left(\mathrm{Membership}.\mathrm{mem}\left(S,\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(x\right),g\right),x\right)\right),f\left(\mathrm{Subtype}.\mathrm{mk}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(x\right),g\right),x\right)\right)\right)\right),\mathrm{Function}.\mathrm{const}\left(\neg (\mathrm{Membership}.\mathrm{mem}\left(S,\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(x\right),g\right),x\right)\right)),0\right)\right))$$

Formalization. D5/S3/FiniteGroups/InducedCharacterFormula.indTerm (✓ 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 (Ind term apply).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall S\in \mathrm{Subgroup}\left(G\right),[\mathrm{AddCommMonoid}\left(k\right)],\forall f\in (\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right))\to (k),\forall g\in G,\forall x\in G,(D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indTerm}\left(f,g,x\right))=(\mathrm{dite}\left(\mathrm{Membership}.\mathrm{mem}\left(S,\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(x\right),g\right),x\right)\right),\mathrm{Function}.\mathrm{const}\left(\mathrm{Membership}.\mathrm{mem}\left(S,\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(x\right),g\right),x\right)\right),f\left(\mathrm{Subtype}.\mathrm{mk}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(x\right),g\right),x\right)\right)\right)\right),\mathrm{Function}.\mathrm{const}\left(\neg (\mathrm{Membership}.\mathrm{mem}\left(S,\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(x\right),g\right),x\right)\right)),0\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/InducedCharacterFormula.indTerm_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.7 (Ind class fun).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],[\mathrm{AddCommMonoid}\left(k\right)],\forall S\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{FiniteIndex}\left(S\right)],\forall f\in (\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right))\to (k),\forall g\in G,D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indClassFun}\left(S,f,g\right)=(\mathrm{Finset}.\mathrm{sum}\left(\mathrm{Finset}.\mathrm{univ},\lambda (t:\mathrm{HasQuotient}.\mathrm{Quotient}\left(G,S\right))\mapsto (D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indTerm}\left(f,g,\mathrm{Quotient}.\mathrm{out}\left(t\right)\right))\right))$$

Formalization. D5/S3/FiniteGroups/InducedCharacterFormula.indClassFun (✓ 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 (Ind class fun apply).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall S\in \mathrm{Subgroup}\left(G\right),[\mathrm{AddCommMonoid}\left(k\right)],[\mathrm{Subgroup}.\mathrm{FiniteIndex}\left(S\right)],\forall f\in (\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right))\to (k),\forall g\in G,(D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indClassFun}\left(S,f,g\right))=(\mathrm{Finset}.\mathrm{sum}\left(\mathrm{Finset}.\mathrm{univ},\lambda (t:\mathrm{HasQuotient}.\mathrm{Quotient}\left(G,S\right))\mapsto (\mathrm{dite}\left(\mathrm{Membership}.\mathrm{mem}\left(S,\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(\mathrm{Quotient}.\mathrm{out}\left(t\right)\right),g\right),\mathrm{Quotient}.\mathrm{out}\left(t\right)\right)\right),\mathrm{Function}.\mathrm{const}\left(\mathrm{Membership}.\mathrm{mem}\left(S,\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(\mathrm{Quotient}.\mathrm{out}\left(t\right)\right),g\right),\mathrm{Quotient}.\mathrm{out}\left(t\right)\right)\right),f\left(\mathrm{Subtype}.\mathrm{mk}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(\mathrm{Quotient}.\mathrm{out}\left(t\right)\right),g\right),\mathrm{Quotient}.\mathrm{out}\left(t\right)\right)\right)\right)\right),\mathrm{Function}.\mathrm{const}\left(\neg (\mathrm{Membership}.\mathrm{mem}\left(S,\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Inv}.\mathrm{inv}\left(\mathrm{Quotient}.\mathrm{out}\left(t\right)\right),g\right),\mathrm{Quotient}.\mathrm{out}\left(t\right)\right)\right)),0\right)\right))\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/InducedCharacterFormula.indClassFun_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.9 (Ind term eq of mk eq).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall S\in \mathrm{Subgroup}\left(G\right),[\mathrm{Semiring}\left(k\right)],\forall f\in (\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right))\to (k),(\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right)\right),f\right))\Rightarrow (\forall g\in G,\forall x\in G,\forall y\in G,((\mathrm{QuotientGroup}.\mathrm{mk}\left(x\right))=(\mathrm{QuotientGroup}.\mathrm{mk}\left(y\right)))\Rightarrow ((D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indTerm}\left(f,g,x\right))=(D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indTerm}\left(f,g,y\right))))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/InducedCharacterFormula.indTerm_eq_of_mk_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.10 (Ind).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],[\mathrm{Semiring}\left(k\right)],\forall S\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{FiniteIndex}\left(S\right)],D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{ind}\left(S\right)=(\mathrm{LinearMap}.\mathrm{mk}\left(\mathrm{AddHom}.\mathrm{mk}\left(\lambda (f:\mathrm{Subtype}\left(\lambda (x:(\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right))\to (k))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right)\right),x\right))\right))\mapsto (\mathrm{Subtype}.\mathrm{mk}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indClassFun}\left(S,\mathrm{Subtype}.\mathrm{val}\left(f\right)\right)\right))\right)\right))$$

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

Theorem 1.11 (Ind apply).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall S\in \mathrm{Subgroup}\left(G\right),[\mathrm{Semiring}\left(k\right)],[\mathrm{Subgroup}.\mathrm{FiniteIndex}\left(S\right)],\forall f\in \mathrm{Subtype}\left(\lambda (x:(\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right))\to (k))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right)\right),x\right))\right),\forall g\in G,(\mathrm{Subtype}.\mathrm{val}\left(\mathrm{DFunLike}.\mathrm{coe}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{ind}\left(S\right),f\right),g\right))=(D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indClassFun}\left(S,\mathrm{Subtype}.\mathrm{val}\left(f\right),g\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/InducedCharacterFormula.ind_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.12 (Ind fdr ep).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall S\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{FiniteIndex}\left(S\right)],\forall A\in \mathrm{FDRep}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right)\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indFDRep}\left(A\right)=(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{FDRep}.\mathrm{ofShrink}\left(\mathrm{Rep}.\rho \left(\mathrm{Rep}.\mathrm{ind}\left(\mathrm{Subgroup}.\mathrm{subtype}\left(S\right),\mathrm{CategoryTheory}.\mathrm{Functor}.\mathrm{obj}\left(\mathrm{CategoryTheory}.{\mathrm{forget}}_2\left(\mathrm{FDRep}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right)\right),\mathrm{Rep}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right)\right)\right),A\right)\right)\right)\right))$$

Formalization. D5/S3/FiniteGroups/InducedCharacterFormula.indFDRep (✓ 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.13 (Finrank ind fdr ep).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall S\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{FiniteIndex}\left(S\right)],\forall A\in \mathrm{FDRep}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right)\right),(\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{FGModuleCat}.\mathrm{carrier}\left(\mathrm{Action}.V\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indFDRep}\left(A\right)\right)\right)\right))=(\mathrm{HMul}.\mathrm{hMul}\left(\mathrm{Subgroup}.\mathrm{index}\left(S\right),\mathrm{Module}.\mathrm{finrank}\left(k,\mathrm{FGModuleCat}.\mathrm{carrier}\left(\mathrm{Action}.V\left(A\right)\right)\right)\right))$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/InducedCharacterFormula.finrank_indFDRep (✓ 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.14 (Character pairing ind).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall S\in \mathrm{Subgroup}\left(G\right),[\mathrm{Field}\left(k\right)],[\mathrm{Fintype}\left(G\right)],(\mathrm{IsUnit}\left(\mathrm{Nat}.\mathrm{cast}\left(\mathrm{Nat}.\mathrm{card}\left(G\right)\right)\right))\Rightarrow (\forall f\in \mathrm{Subtype}\left(\lambda (x:(\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right))\to (k))\mapsto (\mathrm{Membership}.\mathrm{mem}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right)\right),x\right))\right),\forall h\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},\mathrm{DFunLike}.\mathrm{coe}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{ind}\left(S\right),f\right)\right),h\right))=(\mathrm{DFunLike}.\mathrm{coe}\left(\mathrm{DFunLike}.\mathrm{coe}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{characterPairing},f\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),h\right)\right)))$$

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

Theorem 1.15 (Finite double coset quotient).

$$\forall G\in Type\ast ,[\mathrm{Group}\left(G\right)],\forall H\in \mathrm{Subgroup}\left(G\right),\forall K\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{FiniteIndex}\left(K\right)],\mathrm{Finite}\left(\mathrm{DoubleCoset}.\mathrm{Quotient}\left(\mathrm{SetLike}.\mathrm{coe}\left(H\right),\mathrm{SetLike}.\mathrm{coe}\left(K\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/FiniteGroups/InducedCharacterFormula.finite_doubleCosetQuotient (✓ 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 (Ind of fdr ep).

$$\forall k\in Type\ast ,\forall G\in Type\ast ,[\mathrm{Field}\left(k\right)],[\mathrm{Group}\left(G\right)],\forall S\in \mathrm{Subgroup}\left(G\right),[\mathrm{Subgroup}.\mathrm{FiniteIndex}\left(S\right)],\forall A\in \mathrm{FDRep}\left(k,\mathrm{Subtype}\left(\lambda (x:G)\mapsto (\mathrm{Membership}.\mathrm{mem}\left(S,x\right))\right)\right),(\mathrm{DFunLike}.\mathrm{coe}\left(D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{ind}\left(S\right),D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{ofCharacter}\left(\mathrm{FDRep}.\rho \left(A\right)\right)\right))=(D5.S3.\mathrm{FiniteGroups}.\mathrm{FiniteCharacterAlgebra}.\mathrm{TauCeti}.\mathrm{ClassFunction}.\mathrm{ofCharacter}\left(\mathrm{FDRep}.\rho \left(D5.S3.\mathrm{FiniteGroups}.\mathrm{InducedCharacterFormula}.\mathrm{TauCeti}.\mathrm{indFDRep}\left(A\right)\right)\right))$$

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

References

• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.char_eq_finrank_iff
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.characterPairing_ind
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.clifford_restrict_finrank
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.doubleCosetMk_eq_mk_one_iff_mem
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.finite_doubleCosetQuotient
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.finrank_indFDRep
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.ind
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.indClassFun
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.indClassFun_apply
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.indFDRep
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.indTerm
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.indTerm_apply
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.indTerm_eq_of_mk_eq
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.ind_apply
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.ind_ofFDRep
• Truth anchor: D5/S3/FiniteGroups/InducedCharacterFormula.stabilizer_quotientGroup_mk
• Dependency: D5/S3/FiniteGroups/CharacterDegreeDivisibility
• Dependency: D5/S3/FiniteGroups/CliffordConstituents
• Dependency: D5/S3/FiniteGroups/CliffordDecomposition
• Dependency: D5/S3/FiniteGroups/FiniteCharacterAlgebra