Finite-dimensional induced representations #
This file constructs the finite-dimensional representation induced from a finite-index subgroup.
The main input is a linear equivalence between coinduction and a product indexed by right cosets.
Composing it with Mathlib's finite-index isomorphism from induction to coinduction gives the
dimension formula
finrank k (Ind_S^G A) = S.index * finrank k A.
Induction on finite-dimensional representations is packaged both objectwise, as indFDRep, and
functorially, as indFDRepFunctor, the latter naturally isomorphic to Rep.indFunctor under the
forgetful functor to Rep k G.
That functor is additive (indFDRepMap_add); the general fact it rests on, additivity of induced
intertwiners along an arbitrary group homomorphism, is Rep.indMap_add of
TauCeti.RepresentationTheory.Induction.Basic. Read through the functor, induction sends an
isomorphism of representations to an isomorphism of the induced ones
(nonempty_iso_indFDRep).
The objectwise construction, dimension theorem, and functor on FDRep allow the scalar field and
group to live in separate universes. It uses a small model of Mathlib's induced carrier, compared by
indFDRepForgetEquiv. The comparison isomorphism and natural isomorphism into Mathlib's Rep
category retain a common universe because that category is indexed by one carrier universe. The
corresponding character formula is in TauCeti.RepresentationTheory.Induction.Character.
References #
This implements the first item of Layer 2, “Induction preserves finite-dimensionality, via an
explicit coset model”, in
TauCetiRoadmap/RepresentationTheory/InductionRestriction/README.md.
The coset-representative construction below — rightCosetFactor together with the two rewriting
lemmas rightCoset_mk_mul and rightCosetFactor_mul that make it S-equivariant, and the proof
plan of building an equivariant function from values at the chosen representatives — is adapted
from the proof of the PreservesEpimorphisms instance for Rep.coindFunctor in
Mathlib.RepresentationTheory.Coinduced, where the same factor appears inline as a local
definition γ with auxiliary facts hmk and hγ. Here it is extracted as standalone API and
used to build the coset equivalence rather than a surjectivity witness.
The element of S carrying the chosen representative of the right coset of g to g.
Equations
- TauCeti.Rep.rightCosetFactor g = ⟨g * (Quotient.mk'' g).out⁻¹, ⋯⟩
Instances For
Left multiplication by an element of S does not change a right coset.
The right-coset factor is equivariant under left multiplication by S.
The right-coset factor carries the chosen representative back to the original element.
The right-coset factor of a chosen representative is trivial.
Coinduction from a subgroup is linearly equivalent to a product of copies of the original representation indexed by the right cosets. The forward map evaluates an equivariant function at the chosen representative of each right coset.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The coset model evaluates a coinduced function at the chosen representative.
The inverse coset model extends a value from each representative by S-equivariance.
In the coset model the G-action on coinduction is the coordinate permutation
q ↦ ⟦q.out * g⟧ followed by the action of the coset factor of q.out * g.
Not a simp lemma: Mathlib's @[simps] on Representation.coind rewrites
(Rep.coind φ A).ρ g to its underlying LinearMap, so this left-hand side is not in simp
normal form. Mathlib states its own action lemma Representation.ind_mk the same way.
The underlying vector space of induction from a finite-index subgroup is a product of copies of the original representation indexed by the right cosets.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The coset model of induction transports along Rep.indCoindIso and then evaluates at the
chosen representative of each right coset.
Not a simp lemma: its right-hand side names Rep.indCoindIso, so rewriting with it replaces
the coset model by the comparison isomorphism it is built from. The intended interface is
indSubtypeEquivPi_ρ_apply, which stays inside the coset model.
The inverse coset model of induction extends by S-equivariance and then transports back
along Rep.indCoindIso.
Not a simp lemma, for the same reason as indSubtypeEquivPi_apply: it rewrites the coset
model into the comparison isomorphism.
In the coset model of induction the G-action is the coordinate permutation
q ↦ ⟦q.out * g⟧ followed by the action of the coset factor of q.out * g. This is the form a
trace computation over the coset model consumes.
Not a simp lemma, for the same reason as coindSubtypeEquivPi_ρ_apply: @[simps] on
Representation.ind takes (Rep.ind φ A).ρ g out of simp normal form.
Induction from a finite-index subgroup preserves finite-dimensionality.
The dimension of induction from a finite-index subgroup is the index times the original dimension.
Not a simp lemma: A lives in the universe max w u, and when simp unifies the left-hand side
with a goal it cannot recover w from that universe, so in a universe-polymorphic context the lemma
fires only with its universes given, as simp [finrank_ind.{u, v, w}]. The left-hand side is still
stated through dsimp% only, so that simp [finrank_ind] fires when the universes are concrete.
The finite-dimensional representation induced from a finite-index subgroup.
Equations
Instances For
The small carrier chosen by indFDRep is equivariantly linearly equivalent to Mathlib's
possibly universe-large induced representation.
Instances For
Same-universe categorical wrapper around indFDRepForgetEquiv: forgetting
finite-dimensionality from indFDRep recovers Mathlib's induced representation.
Equations
Instances For
Induction of an intertwiner of finite-dimensional representations, obtained by conjugating Mathlib's induced intertwiner by the small-carrier comparison equivalences.
Equations
Instances For
indFDRepMap applies Mathlib's induced intertwiner between the two small-carrier comparison
equivalences.
After forgetting finite-dimensionality, indFDRepMap is Mathlib's induced intertwiner
transported across the small-carrier comparison isomorphisms.
Induction of intertwiners from a finite-index subgroup is additive,
indFDRepMap (f + g) = indFDRepMap f + indFDRepMap g. This is what makes indFDRepFunctor an
additive functor.
Induction from a finite-index subgroup, as a functor on finite-dimensional representations.
It acts on objects as indFDRep and on intertwiners as indFDRepMap.
Equations
- TauCeti.indFDRepFunctor = { obj := fun (A : FDRep k ↥S) => TauCeti.indFDRep A, map := fun {X Y : FDRep k ↥S} (f : X ⟶ Y) => TauCeti.indFDRepMap f, map_id := ⋯, map_comp := ⋯ }
Instances For
indFDRepFunctor acts on objects by indFDRep.
indFDRepFunctor acts on morphisms by indFDRepMap.
Induction from a finite-index subgroup is an additive functor, which is what lets it be
passed to the split Grothendieck group in
TauCeti.RepresentationTheory.RepresentationRing.Induction.
Under the forgetful functor to Rep k G, indFDRepFunctor is naturally isomorphic to
Mathlib's induction functor, componentwise by indFDRepForgetIso.
Equations
- TauCeti.indFDRepForgetNatIso = CategoryTheory.NatIso.ofComponents (fun (A : FDRep k ↥S) => TauCeti.indFDRepForgetIso A) ⋯
Instances For
The dimension of an induced representation is the subgroup index times the dimension of the original representation.