PropositionStatement: 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.

A left transversal identifies ${Ind}_{H}^{G} W$ with a direct sum of $[G : H]$ copies of $W$

Statement

Let $R$ be a commutative ring, let $G$ be a group, let $H \leq G$ , let $W$ be an $R$ -linear $H$ -module, and let $T = {t_{1}, \dots, t_{n}} \subseteq G$ meet each left coset $g H$ in exactly one point. Then evaluation on $T$ defines an $R$ -module isomorphism

${ev}_{T} : {Ind}_{H}^{G} W ⟶ ⨁_{i = 1}^{n} W, f ⟼ (f (t_{1}), \dots, f (t_{n})) .$

In particular $n = [G : H]$ .

Facts & Assumptions

Given: A commutative ring $R$ , a group $G$ , a subgroup $H \leq G$ , an $R$ -linear $H$ -module $W$ , and a left transversal $T = {t_{1}, \dots, t_{n}}$ for $G / H$ .

[F1]

The induced module consists of the functions $f : G \to W$ satisfying $f (g h) = h^{- 1} \cdot f (g)$ , with pointwise $R$ -module structure (The induced $R$ -linear $G$ -module ${Ind}_{H}^{G} W$ as $H$ -covariant functions on $G$ ).

[F2]

The left cosets of $H$ are the subsets $g H = {g h : h \in H}$ of $G$ (Left and right cosets $g H$ and $H g$ of a subgroup).

[F3]

For a finite index set, the direct sum is the module of tuples with coordinatewise operations (The direct sum of an indexed family of modules).

Proof

technique · constructive

1.1

Because $T$ meets each left coset $g H$ in exactly one point, every $g \in G$ can be written uniquely as $g = t_{i} h$ with $t_{i} \in T$ and $h \in H$ .

F2given

1.2

The map ${ev}_{T}$ is $R$ -linear because [F1] and [F3] define both module structures coordinatewise.

F1F3given

2.1

Define $Φ : ⨁_{i = 1}^{n} W ⟶ {Ind}_{H}^{G} W$ by $Φ (w_{1}, \dots, w_{n}) (t_{i} h) : = h^{- 1} \cdot w_{i}$ . Step 1.1 makes this well defined, and the displayed formula satisfies the covariance condition of [F1], so $Φ (w_{1}, \dots, w_{n}) \in {Ind}_{H}^{G} W$ .

F1step 1.1construct

3.1

The map $Φ$ is $R$ -linear because the $H$ -action on $W$ is $R$ -linear and the formula of step 2.1 is coordinatewise in the tuple entries.

F1F3step 2.1algebra

3.2

For $(w_{1}, \dots, w_{n}) \in ⨁_{i} W$ , ${ev}_{T} (Φ (w_{1}, \dots, w_{n})) = (w_{1}, \dots, w_{n})$ because $Φ (w_{1}, \dots, w_{n}) (t_{i}) = w_{i}$ .

step 2.1algebra

3.3

For $f \in {Ind}_{H}^{G} W$ and $g = t_{i} h$ as in step 1.1, one has $Φ ({ev}_{T} (f)) (g) = Φ (f (t_{1}), \dots, f (t_{n})) (t_{i} h) = h^{- 1} \cdot f (t_{i}) = f (t_{i} h) = f (g)$ , where the third equality is the covariance condition from [F1]. Hence $Φ ({ev}_{T} (f)) = f$ .

F1step 1.1step 2.1algebra

4.1

Steps 3.2 and 3.3 show that $Φ$ and ${ev}_{T}$ are inverse $R$ -module isomorphisms. Since $T$ has one element on each left coset, its cardinality is $[G : H]$ .

F2step 3.2step 3.3discharge-construct∎

Depends on

Used by

Dependency tree · two levels

9 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

Peter Webb, A Course in Finite Group Representation Theory, Proposition 4.5.1 (standard reference, not scraped)
Anupam Singh, Representation Theory of Finite Groups, Chapter 17 (standard reference, not scraped)

A left transversal identifies Ind⁡HGWIndHG​W with a direct sum of [G:H][G:H] copies of WW