ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-16

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.

Frobenius reciprocity for group representations without tensor products

Example

Let $H \leq G$ be groups and let $k$ be a field. For a left $k$ -linear $H$ -representation $V$ , define ${Ind}_{H}^{G} (V)$ to be the functions $f : G \to V$ such that

$f (g h) = h^{- 1} \cdot f (g)$

for $g \in G$ and $h \in H$ , and such that the left cosets on which $f$ is nonzero form a finite set. With $(a \cdot f) (g) = f (a^{- 1} g)$ , this is a $G$ -representation and

${Ind}_{H}^{G} ⊣ {Res}_{H}^{G} .$

Facts & Assumptions

Given: A subgroup $H \leq G$ , a field $k$ , an $H$ -representation $V$ , and a $G$ -representation $W$ .

[F1]

A left group action satisfies $e \cdot x = x$ and $(g h) \cdot x = g \cdot (h \cdot x)$ (Left group actions, transitive actions, and faithful actions).

[F2]

A vector space is an abelian group under addition with scalar laws $λ (u + v) = λ u + λ v$ , $(λ + μ) v = λ v + μ v$ , $(λ μ) v = λ (μ v)$ , and $1 v = v$ (Vector space over a field).

[F3]

A map $T : V \to W$ is linear exactly when $T (a u + b v) = a T (u) + b T (v)$ for all scalars and vectors (Linear map between vector spaces over the same field).

[F4]

A subgroup contains the identity and is closed under products and inverses (Subgroup).

[F5]

The left coset of $H$ represented by $g$ is $g H = {g h : h \in H}$ , and the right coset is $H g = {h g : h \in H}$ (Left and right cosets $g H$ and $H g$ of a subgroup).

[F6]

For sets $A, B$ , the functions $A \to B$ form the set $B^{A}$ (The set $B^{A}$ of all functions $A \to B$ ).

[F7]

A set is finite when it is in bijection with some natural number (The cardinality $∣ A ∣$ of a finite set).

[F8]

For a finite set $S$ and a function into a commutative monoid, $\sum_{s \in S} a_{s}$ is the enumeration-independent finite sum, and the sum over the empty set is $0$ (A finite sum in a commutative monoid indexed by an arbitrary finite set).

[F9]

Finite sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the two finite Fubini formulas (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

Verification

technique · direct

1.1

The defining equations cut out a vector subspace of the function set $V^{G}$ from [F6]. Pointwise operations preserve the covariance equation, and finite unions preserve finite coset support.

F2F3F5F6F7algebra

2.1

The formula $(a \cdot f) (g) = f (a^{- 1} g)$ preserves the covariance equation and finite support. The equations in [F1] show that it is a left $G$ -action, and pointwise operations show that the action is linear. Hence ${Ind}_{H}^{G} (V)$ is a $G$ -representation.

step 1.1F1F2F4algebra

2.2

For an $H$ -equivariant linear map $u : V \to {Res}_{H}^{G} (W)$ , set $\hat{u} (f) : = \sum_{g H \in G / H} g \cdot u (f (g))$ , where zero summands are omitted. If $g$ is replaced by $g h$ , the summand becomes $g h \cdot u (h^{- 1} \cdot f (g)) = g \cdot u (f (g))$ , so it depends only on the coset. The nonzero index set is finite, and [F8] makes the empty-support value zero.

step 1.1F1F3F5F7F8algebra

3.1

Define $j_{V} : V \to {Res}_{H}^{G} {Ind}_{H}^{G} (V)$ by $j_{V} (v) (h) = h^{- 1} \cdot v$ for $h \in H$ and $j_{V} (v) (g) = 0$ for $g \notin H$ . The subgroup axioms make this well-defined with support in $H$ , and direct calculation gives $j_{V} (a \cdot v) = a \cdot j_{V} (v)$ for $a \in H$ ; it is linear by [F3].

step 2.1F1F3F4algebra

3.2

Linearity follows termwise from [F3]. Left multiplication bijects the relevant coset sets, so reindexing with [F9] gives $\hat{u} (a \cdot f) = a \cdot \hat{u} (f)$ . Thus $\hat{u}$ is a $G$ -equivariant linear map, naturally in $V$ and $W$ .

step 2.1step 2.2F1F3F9algebra

4.1

Every $f$ has the finite decomposition $f = \sum_{g H} g \cdot j_{V} (f (g))$ : at any $x \in G$ , only the coset $x H$ contributes, and its contribution is $f (x)$ . Therefore a $G$ -map $T$ satisfies $\hat{(T j_{V})} (f) = T (f)$ .

step 2.1step 3.1step 2.2F8F9

5.1

The function $j_{V} (v)$ is supported on the single coset $H$ , and its value at $1$ is $v$ , so $(\hat{u}) j_{V} = u$ . Together with step 4.1, the assignments $u \mapsto \hat{u}$ and $T \mapsto T j_{V}$ are inverse natural bijections, proving ${Ind}_{H}^{G} ⊣ {Res}_{H}^{G}$ .

step 3.1step 2.2step 3.2step 4.1F4F8∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 68 results over 23 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Emily Riehl, Category Theory in Context, 2nd ed., Example 4.1.11 (standard reference, not scraped)