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

Relative projectivity mackey intersections for finite modules

Statement

For subgroups A,B≤H of a finite group and a finite-dimensional kB-module V over any field, with Lx=A∩xBx−1, Res⁡AHInd⁡BHV≅⨁x∈A\H/BInd⁡LxA(xRes⁡B∩x−1AxBV). Induction is transitive, induction and restriction preserve direct summands, and relative projectivity is transitive up a subgroup chain. In characteristic p, if a nonzero indecomposable finite-dimensional kH-module M is relatively B-projective, any vertex Q is contained in an H-conjugate of B. An indecomposable direct summand of a finite sum of modules is a summand of one of its terms.

Facts & Assumptions

Given: The finite groups and finite-dimensional modules specified above.

[F1]

Relative projectivity is the direct-summand property for an induced module. (A module is relatively H-projective when it is a direct summand of one induced from H)

[F2]

Higman characterizes relative projectivity by a relative trace of an endomorphism. (Higman's criterion characterizes relative projectivity through the relative trace idempotent test)

[F3]

Nonzero indecomposable modules in characteristic p have vertices and sources; vertices are conjugate. (Vertices exist for indecomposable modules, are conjugate in G, and sources are conjugate by the appropriate normalizer)

[F4]

Finite-dimensional modules decompose uniquely into finitely many indecomposables. (Finite-dimensional kG-modules decompose as finite direct sums of indecomposables uniquely up to order and isomorphism)

Proof

technique · direct
1.1given

For a double-coset representative x, send a⊗v to ax⊗v. For t∈Lx, atx⊗v=ax⊗(x−1tx)v, so this is balanced. The basis of kH partitions into the disjoint double cosets AxB. Representatives a of A/Lx give a right kB-basis ax of k[AxB], because a1xB=a2xB holds exactly when a2−1a1∈Lx. Thus the component map is a bijection between the same copies of V, and the direct sum is the claimed module isomorphism.

1.2F1F2

Transitivity is a⊗(b⊗v)↦ab⊗v, inverse a⊗v↦a⊗(1⊗v); tensor relations make both maps well-defined. Applying either induction or restriction to split inclusion and projection maps preserves their composite identity, hence summands. Higman supplies a finite inducing witness: if idM=Tr⁡BHα, then m↦∑t∈H/Bt⊗α(t−1m) splits the counit h⊗m↦hm. This map is H-linear by reindexing cosets.

1.3F4

Decompose each term of a finite direct sum into indecomposables by [F4]. If an indecomposable M is a summand of that sum, uniqueness of indecomposable decompositions forces it to be isomorphic to a summand of one term.

2.1F1F3step 1.1step 1.2step 1.3∎

Let Q be a vertex of M and suppose M is relatively B-projective. Combining the two counit splittings gives M∣Ind⁡QHRes⁡QHInd⁡BHRes⁡BHM. Steps 1.1–1.2 express the right side as a finite sum induced from Q∩xBx−1. Step 1.3 puts M in one term. This intersection is a p-subgroup of Q; minimality in the definition of vertex forces it to equal Q. Hence Q≤xBx−1, as claimed.

Sources

Webb, A Course in Finite Group Representation Theory, §§5.2, 11.3, 11.6, 12.3–12.5; especially Lemma 12.4.4 and Theorem 12.4.5, pp.240–241. Local argument and conventions as displayed above.

Depends on

Used by

Dependency tree · two levels

15 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