Restriction is a homomorphism of representation rings

For a monoid homomorphism φ : G →* H over a field k, restricting a finite-dimensional representation of H along φ is Mathlib's CategoryTheory.Action.res (FGModuleCat k) φ, under the definitional identification FDRep k G = Action (FGModuleCat k) G. This file passes that functor to the representation rings of TauCeti/RepresentationTheory/RepresentationRing/Basic.lean:

TauCeti.repRingRes k φ : R(H) →+* R(G).

It is a homomorphism of rings, not merely of additive groups, and for a strong reason: restriction does not merely commute with the tensor product up to a comparison isomorphism, it preserves it on the nose. The action of H on X ⊗ Y is g ↦ X.ρ g ⊗ₘ Y.ρ g, so precomposing with φ is the same as precomposing in each factor, and likewise the restriction of the trivial one-dimensional representation is the trivial one-dimensional representation. That is the content of the monoidal structure on Action.res recorded in TauCeti/CategoryTheory/Action/Monoidal.lean, whose unit and tensorator are identities, and it is what TauCeti.SplitK0.mapRingHom consumes here.

On characters everything is as expected: the character of a restriction is the character precomposed with φ (TauCeti.repRingCharacter_repRingRes), so the square formed by the two character homomorphisms and the two restrictions commutes. Read elementwise, that square is the statement that a virtual character of H pulls back to a virtual character of G, which is TauCeti.comp_mem_virtualCharacters, proved directly on the class functions.

Main definitions

• TauCeti.repRingRes: restriction along a monoid homomorphism, as a ring homomorphism of representation rings.
• TauCeti.repRingResEquiv: restriction along an isomorphism of monoids, as a ring isomorphism.

Main statements

• TauCeti.repRingRes_of: restriction sends the class of a representation to the class of its restriction. For a subgroup S ≤ G, restriction along S.subtype is restriction to S.
• TauCeti.repRingRes_id and TauCeti.repRingRes_comp: restriction is functorial, contravariantly in the homomorphism.
• TauCeti.repRingCharacter_repRingRes and TauCeti.repRingCharacter_repRingRes_apply: the character of a restricted virtual representation is the character precomposed with φ.

Implementation notes

The three monoids are left in three independent universes: nothing here needs them to agree, and the subgroup case S.subtype : S →* G lands in the same universe as G anyway.

Induction in the other direction is not a ring homomorphism -- it is a homomorphism of R(G)-modules, by the projection formula TauCeti.indProjection -- and is not built here.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), Part II, §9.

noncomputable def TauCeti.repRingRes (k : Type u) [Field k] {G : Type v} {H : Type v'} [Monoid G] [Monoid H] (φ : G →* H) : repRing k H →+* repRing k G

Restriction of representations, on the representation ring: the ring homomorphism R(H) →+* R(G) induced by a monoid homomorphism φ : G →* H, sending the class of a representation of H to the class of its restriction along φ.

It is Mathlib's restriction functor CategoryTheory.Action.res fed to TauCeti.SplitK0.mapRingHom, and it is multiplicative because that functor is monoidal (Action.resMonoidal).

Equations

• TauCeti.repRingRes k φ = TauCeti.SplitK0.mapRingHom (Action.res (FGModuleCat k) φ)

@[simp]

theorem TauCeti.repRingRes_of {k : Type u} [Field k] {G : Type v} {H : Type v'} [Monoid G] [Monoid H] (φ : G →* H) (V : FDRep k H) : (repRingRes k φ) (SplitK0.of V) = SplitK0.of ((Action.res (FGModuleCat k) φ).obj V)

Restriction sends the class of a representation to the class of its restriction.

@[simp]

theorem TauCeti.repRingRes_id {k : Type u} [Field k] {G : Type v} [Monoid G] : repRingRes k (MonoidHom.id G) = RingHom.id (repRing k G)

Restricting along the identity does nothing.

@[simp]

theorem TauCeti.repRingRes_comp {k : Type u} [Field k] {G : Type v} {H : Type v'} {K : Type v''} [Monoid G] [Monoid H] [Monoid K] (φ : G →* H) (ψ : H →* K) : repRingRes k (ψ.comp φ) = (repRingRes k φ).comp (repRingRes k ψ)

Restriction is contravariantly functorial: restricting along a composite is restricting twice over. The two functors agree on the nose, so the comparison of classes is the identity isomorphism.

@[simp]

theorem TauCeti.repRingCharacter_repRingRes_apply {k : Type u} [Field k] {G : Type v} {H : Type v'} [Monoid G] [Monoid H] (φ : G →* H) (x : repRing k H) (g : G) : (repRingCharacter k G) ((repRingRes k φ) x) g = (repRingCharacter k H) x (φ g)

The character of a restricted virtual representation, elementwise: it is the character of the original, evaluated at the image of the element.

@[simp]

theorem TauCeti.repRingCharacter_repRingRes {k : Type u} [Field k] {G : Type v} {H : Type v'} [Monoid G] [Monoid H] (φ : G →* H) (x : repRing k H) : (repRingCharacter k G) ((repRingRes k φ) x) = (repRingCharacter k H) x ∘ ⇑φ

The character homomorphism intertwines restriction with precomposition. This is the commuting square relating the two character homomorphisms to restriction on the two sides.

noncomputable def TauCeti.repRingResEquiv {k : Type u} [Field k] {G : Type v} {H : Type v'} [Monoid G] [Monoid H] (e : G ≃* H) : repRing k H ≃+* repRing k G

Restriction along an isomorphism of monoids is an isomorphism of representation rings, with inverse restriction along the inverse isomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.repRingResEquiv_apply {k : Type u} [Field k] {G : Type v} {H : Type v'} [Monoid G] [Monoid H] (e : G ≃* H) (x : repRing k H) : (repRingResEquiv e) x = (repRingRes k e.toMonoidHom) x

TauCeti.repRingResEquiv is restriction along the isomorphism.

@[simp]

theorem TauCeti.repRingResEquiv_symm_apply {k : Type u} [Field k] {G : Type v} {H : Type v'} [Monoid G] [Monoid H] (e : G ≃* H) (x : repRing k G) : (repRingResEquiv e).symm x = (repRingRes k e.symm.toMonoidHom) x

The inverse of TauCeti.repRingResEquiv is restriction along the inverse isomorphism.