Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-30
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 left adjoint to restriction for finite-group modules over a commutative ring

Statement

Let R be a commutative ring, let G be a finite group, let HG, let W be an R-linear H-module, and let V be an R-linear G-module. Then there is a natural isomorphism

HomG(IndHGW,V)HomH(W,ResHGV).

Facts & Assumptions

Given: A commutative ring R, a finite group G, a subgroup HG, an R-linear H-module W, and an R-linear G-module V.

[F1]

The induced module consists of the functions f:GW satisfying f(gh)=h1f(g), with G acting by (xf)(g)=f(x1g) (The induced R-linear G-module IndHGW as H-covariant functions on G).

[F2]

For modules, Hom is an abelian group under pointwise addition, with maps induced by composition (The abelian group HomR(M,N) and maps induced by pre- and postcomposition).

[F3]

G-equivariant maps are exactly the R[G]-module maps, and likewise for H (For a commutative ring R, R-linear G-actions are exactly the compatible left R[G]-module structures).

Proof

technique · constructive
1.1

For wW, define ηw:GW by ηw(h):=h1w for hH and ηw(g):=0 for gH. If xH, then xhH for every hH, so ηw(xh)=0=h10; if xH, then ηw(xh)=h1x1w=h1ηw(x). Thus ηwIndHGW.

F1givenconstruct
1.2

Choose a left transversal T for G/H with eT. If ψ:WResHGV is H-equivariant, define β(ψ)(f):=tTtψ(f(t)). The sum is finite because T is finite.

F1F2givenchooseconstruct
2.1

If Φ:IndHGWV is G-equivariant, define α(Φ)(w):=Φ(ηw). For hH, one has ηhw=hηw by the action formula in [F1], so α(Φ)(hw)=Φ(hηw)=hΦ(ηw)=hα(Φ)(w). Hence α(Φ)HomH(W,ResHGV).

F1F2step 1.1construct
2.2

The map β(ψ) is G-equivariant. Indeed, for xG and each tT, write x1t=th with tT and hH. Then tψ((xf)(t))=tψ(f(x1t))=tψ(f(th))=tψ(h1f(t))=th1ψ(f(t))=xtψ(f(t)), using the covariance from [F1] and the H-equivariance of ψ. Reindexing the finite sum by t shows β(ψ)(xf)=xβ(ψ)(f).

F1F2step 1.2algebra
3.1

For ψHomH(W,ResHGV), β(ψ)(ηw)=ψ(w) because ηw(t)=0 for te and ηw(e)=w. Hence α(β(ψ))=ψ.

step 1.1step 2.1step 1.2algebra
3.2

For ΦHomG(IndHGW,V) and fIndHGW, one has β(α(Φ))(f)=tTtα(Φ)(f(t))=tTtΦ(ηf(t))=Φ(tTtηf(t)). The function inside Φ equals f, because at a point th it takes the value h1f(t)=f(th) by covariance. So β(α(Φ))=Φ.

F1step 2.1step 1.2algebra
4.1

Steps 3.1 and 3.2 show that α and β are inverse group isomorphisms, giving the stated adjunction. Via [F3], this is equally the usual R[G]-module adjunction.

F3step 3.1step 3.2discharge-construct

Depends on

Used by

Dependency tree · two levels

12 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