Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)audited 2026-10-08
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Induction is invariant under conjugation of the subgroup and the representation

Statement

Let G be a finite group, H≤G, s∈G, and K:=sHs−1. Let W be a finite-dimensional complex H-module with character χ, and let sW be the conjugate K-module with (shs−1)⋅w:=h⋅w and character sχ (Conjugate representations and conjugate characters on conjugate subgroups, Subgroup, A finite-dimensional representation ρ:G→GL⁡(V) over a field, and its degree). Then

Φ:Ind⁡HGW⟶Ind⁡KG(sW),Φ(f)(x):=f(xs)

is an isomorphism of complex G-modules with inverse Ψ(φ)(x):=φ(xs−1) (The induced R-linear G-module Ind⁡HGW as H-covariant functions on G). In particular, Ind⁡KG(sχ)=Ind⁡HGχ in R(G) (The induced character Ind⁡HGχ of a complex character, Virtual characters and the character ring R(G) of a finite group). No choice principle is used.

Facts & Assumptions

Given: A finite group G, a subgroup H≤G, an element s∈G, and a finite-dimensional complex H-module W with character χ.

[F1]

Induced functions satisfy f(gh)=h−1⋅f(g) and the left action is (x⋅f)(g)=f(x−1g) (The induced R-linear G-module Ind⁡HGW as H-covariant functions on G).

[F2]

The conjugate module sW is a representation of K=sHs−1 with (shs−1)⋅w=h⋅w; its character satisfies sχ(shs−1)=χ(h) (Conjugate representations and conjugate characters on conjugate subgroups).

[F3]

The induced character of a finite-dimensional representation is the character of the induced module (The induced character Ind⁡HGχ of a complex character).

[F4]

K=sHs−1 is a subgroup of G (Subgroup).

[F5]

The character ring R(G) is the integral span of the honest complex characters (Virtual characters and the character ring R(G) of a finite group).

Proof

technique · direct
1.1F1F2F4given

For k=shs−1∈K, covariance gives Φ(f)(xk)=f(xks)=f(xsh)=h−1⋅f(xs)=k−1⋅Φ(f)(x), where the last action is that of sW by [F2]. Thus Φ(f) is K-covariant and belongs to Ind⁡KG(sW).

1.2F1F2given

Define Ψ(φ)(x):=φ(xs−1). For h∈H, Ψ(φ)(xh)=φ(xhs−1)=φ((xs−1)(shs−1))=h−1⋅φ(xs−1)=h−1⋅Ψ(φ)(x) by K-covariance and [F2]. Hence Ψ(φ)∈Ind⁡HGW.

2.1F1step 1.1givenalgebra

For x0,x∈G, Φ(x0⋅f)(x)=f(x0−1xs)=Φ(f)(x0−1x)=(x0⋅Φ(f))(x), so Φ is G-equivariant. It is complex-linear by the pointwise module operations.

2.2F1step 1.2givenalgebra

For x0,x∈G, Ψ(x0⋅φ)(x)=φ(x0−1xs−1)=Ψ(φ)(x0−1x)=(x0⋅Ψ(φ))(x), so Ψ is G-equivariant. It is complex-linear by the pointwise operations.

3.1step 1.1step 2.1step 1.2step 2.2algebra

Substitution gives Ψ(Φ(f))(x)=f(xs−1s)=f(x) and Φ(Ψ(φ))(x)=φ(xss−1)=φ(x) for every x∈G. Thus Φ and Ψ are inverse G-module isomorphisms.

4.1F3F5step 3.1∎

The induced modules in step 3.1 are isomorphic, so their characters are equal by [F3]. Both honest characters lie in R(G) by [F5], giving Ind⁡KG(sχ)=Ind⁡HGχ there. The formulas use no choice principle.

Depends on

Used by

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources