Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-5.6-terra)audited 2026-08-26
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 and coinduction of permutation representations as Kan extensions

Example

Let i:H↪G be a subgroup inclusion, and view H and G as one-object categories (A monoid is a one-object category, and a group is a one-object category in which every morphism is invertible). A functor X:H→Set is then a permutation representation of H.

The left Kan extension of X along i is the induced G-set G×HX, and the right Kan extension is the coinduced G-set Map⁡H(G,X).

Facts & Assumptions

Given: A subgroup inclusion i:H↪G and an H-set X, regarded as a functor X:H→Set.

[L1]

The comma-category colimit and limit formulae compute left and right Kan extensions (Comma-category limit and colimit formulae compute Kan extensions).

[F2]

Every small Set-valued diagram has a colimit given by the quotient of its tagged union by the relations generated by its structure maps, and a limit given by its set of compatible tuples (Set has all small colimits, realized as a quotient of a set-indexed disjoint union, Set has all small limits, realized as compatible tuples in a set-indexed product).

Verification

technique · direct
1.1F1F2L1

In the one-object setting, an object of (i↓∗) is just an element g∈G. A morphism from g to g′ is an element h∈H with g=g′i(h) by the comma-category equation, equivalently g′=g i(h−1). So the indexing category is the action groupoid for the right H-action on G, and the induced diagram on Set sends the arrow g→g i(k) to the map x↦k−1x on X. By [F2], its colimit is the quotient of G×X by (g,x)∼(g i(k),k−1x), equivalently by (g i(h),x)∼(g,hx), namely G×HX. Therefore [L1] identifies the induced representation with the left Kan extension.

2.1F1F2L1∎

Dually, an object of (∗↓i) is again an element of G, and a cone to a set Y is exactly a family of maps indexed by G that is equivariant for the H-action. By [F2], the limit is therefore the set of H-equivariant maps G→X, written Map⁡H(G,X). Hence [L1] identifies the coinduced representation with the right Kan extension.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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