Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07
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.

Gallagher correspondence for an extendible type

Statement

Let G be finite, NG, θIrr(N), and I=IG(θ). Assume that a representation S affording θ has a fixed extension S~ to I. Then Irr(I/N)Irr(Iθ),ηχS~InfI/NIη is a bijection. Composing it with induction to G gives a bijection onto Irr(Gθ), and the corresponding G-character has ramification index η(1) over θ.

Facts & Assumptions

Given: The groups, modules, characters, and hypotheses in the statement. All representations here are finite-dimensional complex left representations.

[F1]

An extension retains the space and the given N-action, is an actual group representation, and is automatically irreducible. (An extension of a normal subgroup representation).

[F2]

For a finite θ-isotypical N-module U, evaluation SHomN(S,U)U is an isomorphism; submodules correspond to unique multiplicity subspaces, and maps to linear maps of those spaces. (Isotypical evaluation and multiplicity subspaces).

[F3]

An action with N in its kernel descends uniquely to I/N, preserving irreducibility in both directions. (A representation with kernel containing a normal subgroup factors through the quotient, and irreducibility is unchanged by inflation).

[F4]

An irreducible inertia module lying over its invariant type θ restricts to copies of that type, by the one-orbit restriction result applied to I. (Normal restriction has one orbit of constituents).

[F5]

Induction bijects the irreducible inertia modules above θ with the irreducible G-modules above θ, with inverse the θ-component. (Clifford correspondence).

[F6]

Ramification is the dimension of HomN(S,V), equivalently the multiplicity of θ. (Clifford ramification index).

[F7]

The character of a tensor product of finite-dimensional complex representations of a finite group is the product of the characters. (Characters add on direct sums, multiply on tensor products, and conjugate on duals).

Proof

technique · direct
1.1

Write ρ(i) for the fixed extension on S. For any θ-isotypical I-module U, put M=HomN(S,U) and define (if)(s)=if(ρ(i)1s). For nN, one has ρ(i)1ρ(n)=ρ(i1ni)ρ(i)1, so (if)(ρ(n)s)=n(if)(s). Thus the formula stays in M.

F1givenalgebra
2.1

The action law holds because i(jf)(s)=ijf(ρ(j)1ρ(i)1s)=((ij)f)(s), and the identity acts identically. For nN, nf(ρ(n)1s)=f(s) by N-linearity. Hence N acts trivially on M and this is a representation of I/N.

F3step 1.1algebra
3.1

The evaluation isomorphism is I-equivariant for the diagonal action on SM: EU(ρ(i)s(if))=if(s). Every N-submodule is EU(SM0) for a unique M0M. Since ρ(i) is invertible, its translate is EU(SiM0). Uniqueness shows that this submodule is I-stable exactly when M0 is stable under I/N. For nonzero U, the multiplicity space is nonzero, so U is irreducible if and only if M is irreducible.

F2step 2.1algebra
4.1

Conversely start with a quotient module M and form S~InfM. The map mfm, where fm(s)=sm, is an isomorphism MHomN(S,S~M) by the evaluation lemma and scalar-coordinate identification. The action constructed above satisfies ifm=fim. Therefore this recovers the quotient module, and step 3.1 proves irreducibility for every irreducible parameter. An isomorphism of I-modules induces an isomorphism of their Hom spaces by composition, respecting the quotient action; thus distinct quotient parameters cannot give isomorphic I-modules.

F2step 1.1step 3.1
5.1

Every irreducible I-module above θ is θ-isotypical, so steps 1.1–3.1 apply and its evaluation isomorphism supplies the required tensor form. This proves exhaustivity as well as injectivity. Taking tensor-product characters yields the stated character map.

F4F7step 3.1step 4.1
6.1

Clifford correspondence now supplies the bijection after induction. Its inverse identifies the θ-component with the inducing tensor module, whose restriction to N is dimM=η(1) copies of S. Thus its ramification index is η(1). If I=N, the quotient is trivial and only S occurs; if I=G, induction is identity. An extension was assumed throughout, not obtained merely from invariance.

F5F6step 5.1algebra

Depends on

Used by

Dependency tree · two levels

28 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