Finite-dimensional representations

This file records how the forgetful functor FDRep R G ⥤ Rep R G preserves module-finiteness, finrank and characters. These facts let results proved for representation carriers transfer back to FDRep, in particular in TauCeti.RepresentationTheory.Induction.FiniteDimensional.Basic. In the same spirit it records that rebundling the representation an object carries returns that object, which is the identification a construction phrased as FDRep.of ρ needs in order to be read as a statement about the object it started from.

FDRep.forget₂Rep supplies the canonical forgetful functor over any ring, extending Mathlib's commutative-ring instance with the same underlying construction.

It also records the character of a trivial representation, the constant finrank, in both the Representation and the FDRep.of spellings in which consumers meet it.

An object of FDRep k G carries a module in the universe of k, so FDRep.of accepts a representation only when its carrier already lies there. A module-finite carrier is however always equivalent to one that does, because it is spanned by finitely many vectors over k; FDRep.ofShrink performs that transport, and the lemmas beside it say that the transport changes neither the dimension nor the character. Only the character transfer needs k to be a field, k being a commutative ring throughout otherwise.

Finally it records the structural properties of the character that Mathlib's RepresentationTheory/Character.lean leaves out beside FDRep.char_iso and FDRep.char_tensor: the character is additive on biproducts (and, unbundled, on products of representations and on complementary subrepresentations), the character of the tensor unit is the constant function 1, and the character is constant on the cosets of its kernel. The first two are what is still missing before the character can be read as a ring homomorphism out of the representation ring, TauCeti.repRingCharacter; the last is the elementary half of the kernel API whose analytic half, over ℂ, is TauCeti/RepresentationTheory/CharacterTable/Kernel.lean. Beside it, and needing no characters at all, the common kernel of a family of representations is registered as a normal subgroup.

Main definitions

• FDRep.ofShrink: a module-finite representation on a carrier in an arbitrary universe, as an object of FDRep k G.

Main statements

• Representation.char_trivial: the character of a trivial representation is the dimension of its carrier, whence FDRep.character_of_trivial for the trivial representation on k itself.
• Representation.char_prod: the character is additive on products of representations, the unbundled counterpart of FDRep.char_biprod.
• Subrepresentation.char_add_eq_of_isCompl: the character is additive on complementary subrepresentations.
• FDRep.character_eq_zero_of_finrank_intertwiningMap_eq_zero: a representation without nonzero equivariant endomorphisms has character zero.
• FDRep.forget₂Rep: forgetting finite generation over any coefficient ring.
• FDRep.moduleFinite_forget₂_obj: the forgotten carrier is module-finite.
• FDRep.finrank_forget₂_obj: forgetting does not change finrank.
• FDRep.character_forget₂_obj: forgetting does not change the character.
• MonoidHom.forget₂_map_actionRes: restriction of intertwiners commutes with forgetting finite-dimensionality.
• FDRep.character_actionRes: restricting an action along a monoid homomorphism pulls back its character.
• FDRep.character_of: bundling a representation with FDRep.of does not change its character.
• FDRep.character_ρ: the character of the carried representation is the character of the object.
• FDRep.forget₂_additive: forgetting is an additive functor, and FDRep.forget₂_obj_tensor: it takes a tensor product to the tensor product of the forgotten objects, on the nose.
• FDRep.of_ρ_eq_self: rebundling the representation carried by an object returns that object.
• FDRep.ofShrinkEquiv: FDRep.ofShrink ρ carries a representation equivalent to ρ, whence FDRep.finrank_ofShrink and FDRep.character_ofShrink.
• FDRep.char_biprod: the character is additive on biproducts.
• FDRep.char_tensorUnit: the character of the tensor unit is the constant function 1.
• FDRep.char_mul_of_mem_ker_left: the character is constant on the cosets of its kernel.
• FDRep.normal_iInf_ker: the common kernel of a family of representations is a normal subgroup.

@[simp]

theorem Representation.char_trivial {k : Type u} {G : Type v} {V : Type w} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (g : G) : (trivial k G V).character g = ↑(Module.finrank k V)

The character of a trivial representation is the dimension of its carrier: every group element acts as the identity, whose trace is that dimension.

@[simp]

theorem Representation.char_prod {k : Type u} {G : Type v} {V : Type u_1} {W : Type u_2} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] [AddCommGroup W] [Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W) (g : G) : (ρ.prod σ).character g = ρ.character g + σ.character g

The character is additive on products of representations. This is the unbundled counterpart of FDRep.char_biprod, and it is what reads a splitting ρ ≃ ρ₁ × ρ₂ -- the shape TauCeti.Subrepresentation.equivProdOfIsCompl produces -- off the two characters.

@[simp]

theorem Subrepresentation.char_add_eq_of_isCompl {k : Type u} {G : Type v} {V : Type w} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] {ρ : Representation k G V} {ρ₁ ρ₂ : Subrepresentation ρ} (h : IsCompl ρ₁ ρ₂) : ρ₁.toRepresentation.character + ρ₂.toRepresentation.character = ρ.character

The character is additive on complementary subrepresentations: if ρ₁ and ρ₂ are complementary subrepresentations of ρ, the characters of the representations they carry add up to the character of ρ. This is Representation.char_prod read through the splitting Subrepresentation.equivProdOfIsCompl.

@[instance_reducible, instance 100]

instance FDRep.forget₂Rep {R : Type u} [Ring R] {G : Type v} [Monoid G] : CategoryTheory.HasForget₂ (FDRep R G) (Rep R G)

Forgetting finite generation of a representation over any ring.

This uses the same construction as Mathlib's FDRep forgetful instance, whose coefficient assumption is currently CommRing. The lower priority keeps that instance selected over commutative rings; the two functors agree definitionally.

Equations

• FDRep.forget₂Rep = { forget₂ := ((CategoryTheory.forget₂ (FGModuleCat R) (ModuleCat R)).mapAction G).comp (Rep.ActionToRep R G), forget_comp := ⋯ }

@[simp]

theorem FDRep.character_of_trivial {k : Type u} {G : Type v} [Field k] [Monoid G] (g : G) : (of (Representation.trivial k G k)).character g = 1

The character of the trivial one-dimensional representation is constantly 1, that dimension being 1. This is the form in which the trivial character enters a pairing or a Frobenius reciprocity computation, both of which are phrased for objects of FDRep k G.

@[simp]

theorem FDRep.character_actionRes {k : Type u} {G : Type v} {H : Type w} [Field k] [Monoid G] [Monoid H] (V : FDRep k G) (phi : H →* G) (h : H) : character ((Action.res (FGModuleCat k) phi).obj V) h = V.character (phi h)

The character of a representation restricted along a monoid homomorphism is the pullback of its character along that homomorphism.

theorem MonoidHom.forget₂_map_actionRes {k : Type u} [Ring k] {H : Type v} {K : Type w} [Monoid H] [Monoid K] (f : H →* K) {A B : FDRep k K} (g : A ⟶ B) : (CategoryTheory.forget₂ (FDRep k H) (Rep k H)).map ((Action.res (FGModuleCat k) f).map g) = (Rep.resFunctor f).map ((CategoryTheory.forget₂ (FDRep k K) (Rep k K)).map g)

Restriction of an intertwiner commutes with forgetting finite generation.

instance FDRep.moduleFinite_forget₂_obj {R : Type u} {G : Type v} [Ring R] [Monoid G] (A : FDRep R G) : Module.Finite R ↑((CategoryTheory.forget₂ (FDRep R G) (Rep R G)).obj A)

Forgetting finite generation keeps the finite-generation instance on the carrier.

@[simp]

theorem FDRep.finrank_forget₂_obj {R : Type u} {G : Type v} [CommRing R] [Monoid G] (A : FDRep R G) : Module.finrank R ↑((CategoryTheory.forget₂ (FDRep R G) (Rep R G)).obj A) = Module.finrank R ↑A.V

Forgetting finite-dimensionality does not change the dimension of the carrier.

@[simp]

theorem FDRep.character_forget₂_obj {k : Type u} {G : Type v} [Field k] [Monoid G] (A : FDRep k G) (g : G) : ((CategoryTheory.forget₂ (FDRep k G) (Rep k G)).obj A).ρ.character g = A.character g

Forgetting finite-dimensionality does not change the character of the carrier.

@[simp]

theorem FDRep.character_ρ {k : Type u} {G : Type v} [Field k] [Monoid G] (A : FDRep k G) (g : G) : Representation.character A.ρ g = A.character g

The character of the representation carried by an object of FDRep k G is the character of that object.

@[simp]

theorem FDRep.character_of {k : Type u} {G : Type v} {V : Type u} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (rho : Representation k G V) : (of rho).character = rho.character

Bundling a finite-dimensional representation with FDRep.of does not change its character.

@[simp]

theorem FDRep.of_ρ_eq_self {R : Type u} {G : Type v} [CommRing R] [Monoid G] (A : FDRep R G) : of A.ρ = A

Rebundling the representation carried by an object of FDRep R G returns that object.

instance FDRep.forget₂_additive {R : Type u} {G : Type v} [CommRing R] [Monoid G] : (CategoryTheory.forget₂ (FDRep R G) (Rep R G)).Additive

Forgetting finite-dimensionality is an additive functor: forget₂ (FDRep R G) (Rep R G) preserves sums of intertwiners. This is what lets an additive construction on Rep R G -- the induction of TauCeti.RepresentationTheory.Induction.FiniteDimensional.Basic, say -- be recognized through the forgetful functor.

theorem FDRep.forget₂_obj_tensor {R : Type u} {G : Type v} [CommRing R] [Monoid G] (X Y : FDRep R G) : (CategoryTheory.forget₂ (FDRep R G) (Rep R G)).obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) = CategoryTheory.MonoidalCategoryStruct.tensorObj ((CategoryTheory.forget₂ (FDRep R G) (Rep R G)).obj X) ((CategoryTheory.forget₂ (FDRep R G) (Rep R G)).obj Y)

Forgetting finite-dimensionality preserves the tensor product on the nose. The monoidal structure of FDRep R G is that of FGModuleCat R with the diagonal action, and the monoidal structure of FGModuleCat R is that of ModuleCat R on a carrier that happens to be finite, so the two sides are the same object rather than isomorphic ones.

Deliberately not a simp lemma: it is an equation between objects of Rep R G, which has no business in the global simp set. It is used through CategoryTheory.eqToIso, where the definitional equality it records is too deep for the unifier to find on its own.

noncomputable def FDRep.ofShrink {k : Type u} {G : Type v} {V : Type w} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [Module.Finite k V] (ρ : Representation k G V) : FDRep k G

A module-finite representation as an object of FDRep k G, whatever universe its carrier lives in. A module-finite k-module is Small.{u} for k : Type u, so the carrier may be replaced by Shrink V and the action conjugated across; FDRep.ofShrinkEquiv compares the result with ρ.

Equations

• FDRep.ofShrink ρ = FDRep.of ((Shrink.linearEquiv k V).symm.conjRingEquiv.toMonoidHom.comp ρ)

noncomputable def FDRep.ofShrinkEquiv {k : Type u} {G : Type v} {V : Type w} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [Module.Finite k V] (ρ : Representation k G V) : Representation.Equiv (ofShrink ρ).ρ ρ

The representation carried by FDRep.ofShrink ρ is equivalent to ρ: shrinking the carrier loses nothing.

Equations

• FDRep.ofShrinkEquiv ρ = Representation.Equiv.mk (Shrink.linearEquiv k V) ⋯

@[simp]

theorem FDRep.finrank_ofShrink {k : Type u} {G : Type v} {V : Type w} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] [Module.Finite k V] (ρ : Representation k G V) : Module.finrank k ↑(ofShrink ρ).V = Module.finrank k V

Shrinking the carrier does not change the dimension.

@[simp]

theorem FDRep.character_ofShrink {k : Type u} {G : Type v} {V : Type w} [Field k] [Monoid G] [AddCommGroup V] [Module k V] [FiniteDimensional k V] (ρ : Representation k G V) (g : G) : (ofShrink ρ).character g = ρ.character g

Shrinking the carrier does not change the character: the shrunk representation is equivalent to the original one, by FDRep.ofShrinkEquiv.

@[simp]

theorem FDRep.char_biprod {k : Type u} {G : Type v} [Field k] [Monoid G] (X Y : FDRep k G) : (X ⊞ Y).character = X.character + Y.character

The character is additive on biproducts. Together with FDRep.char_iso and FDRep.char_tensor this is what makes the character a ring homomorphism out of the representation ring; see TauCeti.repRingCharacter.

The proof splits the identity of X ⊞ Y as the sum of the two idempotents biprod.inl ∘ biprod.fst and biprod.inr ∘ biprod.snd (CategoryTheory.Limits.biprod.total) and evaluates the trace of ρ g against each summand with FDRep.trace_comp_of_retraction.

@[simp]

theorem FDRep.char_tensorUnit (k : Type u) (G : Type v) [Field k] [Monoid G] : (CategoryTheory.MonoidalCategoryStruct.tensorUnit (FDRep k G)).character = 1

The character of the tensor unit of FDRep k G is the constant function 1, the unit being the trivial representation on k itself. Beside FDRep.char_tensor this is what makes the character multiplicative out of the representation ring, see TauCeti.repRingCharacter.

@[simp]

theorem FDRep.char_mul_of_mem_ker_left {k : Type u} {G : Type v} [Field k] [Group G] (V : FDRep k G) {g : G} (hg : g ∈ V.ρ.ker) (h : G) : V.character (g * h) = V.character h

A character is constant on the cosets of its kernel: an element acting as the identity may be deleted from a character value. This is an algebraic identity, so it holds over any field. The right-handed form is this one composed with FDRep.char_mul_comm.

theorem FDRep.character_eq_zero_of_finrank_intertwiningMap_eq_zero {k : Type u} {G : Type v} [Field k] [Monoid G] (C : FDRep k G) (hC : Module.finrank k (Representation.IntertwiningMap C.ρ C.ρ) = 0) : C.character = 0

A representation of dimension zero, recognised by its zero-dimensional space of equivariant endomorphisms, has character zero.

instance FDRep.normal_iInf_ker {ι : Type u_1} {k : Type u} {G : Type v} [CommRing k] [Group G] (W : ι → FDRep k G) : (⨅ (i : ι), (W i).ρ.ker).Normal

The common kernel of a family of representations is a normal subgroup. Each kernel is normal, and Mathlib's Subgroup.normal_iInf_normal passes that to the infimum; what is added here is the registration as an instance, that lemma taking its hypothesis as an explicit argument, so that the normality of a common kernel is available to instance search. Nothing here is analytic or character-theoretic; over ℂ the common kernel is a locus of character equations by FDRep.coe_iInf_ker (TauCeti/RepresentationTheory/CharacterTable/Kernel.lean).