Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-29
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.

For finite-dimensional complex V, the intertwiners VW are exactly the fixed points of VW

Statement

Let G be a finite group, let V and W be finite-dimensional complex representations of G, and let

Φ:VCWHomC(V,W)

be the natural isomorphism of For finite-dimensional V, the canonical map VFWHomF(V,W) is an isomorphism, sending fw to the map vf(v)w. Then Φ is an intertwiner between the diagonal representation on VW and the conjugation representation on HomC(V,W), and it carries the fixed subspace (VW)G bijectively onto HomG(V,W).

Facts & Assumptions

Given: Finite-dimensional complex representations V and W of a finite group G.

[F1]

The dual action is (gf)(v)=f(g1v) (The dual or contragredient complex representation).

[F2]

The diagonal action on the tensor product is g(fw)=(gf)(gw) (The tensor product of two complex representations).

[F3]

The fixed subspace of a representation is the set of vectors fixed by every gG (The fixed subspace VG of a representation).

[F4]

Intertwiners are the linear maps T with T(gv)=gT(v) for all g,v (Intertwiners, the spaces HomG(V,W) and EndG(V), equivalent representations, and faithful representations).

[F5]

The map (f,w)[vf(v)w] induces a natural isomorphism Φ:VCWHomC(V,W) (For finite-dimensional V, the canonical map VFWHomF(V,W) is an isomorphism).

Proof

technique · direct
1.1

For an elementary tensor fw and vV, Φ(g(fw))(v)=Φ((gf)(gw))(v) by [F2], and this equals (gf)(v)(gw)=f(g1v)(gw) by [F1].

F1F2given
2.1

The right-hand side of step 1.1 is g(f(g1v)w)=g(Φ(fw)(g1v)), which is the value at v of the conjugation action on the linear map Φ(fw). Since elementary tensors span the tensor product, Φ is an intertwiner of representations.

F5step 1.1algebra
3.1

An element of VW is fixed by G exactly when its image under Φ is fixed by G, because Φ is a bijective intertwiner of step 2.1; so Φ((VW)G)=HomC(V,W)G by [F3].

F3step 2.1given
4.1

A linear map T is fixed by the conjugation action of every g exactly when gT(g1v)=T(v) for all g,v, i.e. when T(gv)=gT(v); by [F4] this says precisely that THomG(V,W). Hence HomC(V,W)G=HomG(V,W), which combines with step 3.1 into the claim.

F4step 3.1algebra

Depends on

Used by

Dependency tree · two levels

14 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