Monoid representations

This file introduces monoid representations and their characters and defines a few ways to construct representations.

Main definitions

• Representation
• Representation.directSum
• Representation.prod
• Representation.tprod
• Representation.linHom
• Representation.dual
• Representation.free

Implementation notes

Representations of a monoid G on a k-module V are implemented as homomorphisms G →* (V →ₗ[k] V). We use the abbreviation Representation for this hom space.

The theorem asAlgebraHom_def constructs a module over the group k-algebra of G (implemented as MonoidAlgebra k G) corresponding to a representation. If ρ : Representation k G V, this module can be accessed via ρ.asModule. Conversely, given a MonoidAlgebra k G-module M, M.ofModule is the associociated representation seen as a homomorphism.

@[reducible, inline]

abbrev Representation (k : Type u_1) (G : Type u_2) (V : Type u_3) [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] : Type (max u_2 u_3)

A representation of G on the k-module V is a homomorphism G →* (V →ₗ[k] V).

def Representation.trivial (k : Type u_1) (G : Type u_2) (V : Type u_3) [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] : Representation k G V

The trivial representation of G on a k-module V.

@[simp]

theorem Representation.trivial_apply (k : Type u_1) {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (g : G) (v : V) : ((trivial k G V) g) v = v

class Representation.IsTrivial {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Prop

A predicate for representations that fix every element.

• out (g : G) : ρ g = LinearMap.id

instance Representation.instIsTrivialTrivial {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] : (trivial k G V).IsTrivial

@[simp]

theorem Representation.isTrivial_def {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) [ρ.IsTrivial] (g : G) : ρ g = LinearMap.id

theorem Representation.isTrivial_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) [ρ.IsTrivial] (g : G) (x : V) : (ρ g) x = x

@[simp]

theorem Representation.inv_self_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (x : V) : (ρ g⁻¹) ((ρ g) x) = x

@[simp]

theorem Representation.self_inv_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (x : V) : (ρ g) ((ρ g⁻¹) x) = x

theorem Representation.apply_bijective {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) : Function.Bijective ⇑(ρ g)

noncomputable def Representation.asAlgebraHom {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : MonoidAlgebra k G →ₐ[k] Module.End k V

A k-linear representation of G on V can be thought of as an algebra map from MonoidAlgebra k G into the k-linear endomorphisms of V.

theorem Representation.asAlgebraHom_def {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : ρ.asAlgebraHom = (MonoidAlgebra.lift k G (V →ₗ[k] V)) ρ

@[simp]

theorem Representation.asAlgebraHom_single {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (r : k) : ρ.asAlgebraHom (MonoidAlgebra.single g r) = r • ρ g

theorem Representation.asAlgebraHom_single_one {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) : ρ.asAlgebraHom (MonoidAlgebra.single g 1) = ρ g

theorem Representation.asAlgebraHom_of {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) : ρ.asAlgebraHom ((MonoidAlgebra.of k G) g) = ρ g

def Representation.asModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] : Representation k G V → Type u_3

If ρ : Representation k G V, then ρ.asModule is a type synonym for V, which we equip with an instance Module (MonoidAlgebra k G) ρ.asModule.

You should use asModuleEquiv : ρ.asModule ≃+ V to translate terms.

instance Representation.instAddCommMonoidAsModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : AddCommMonoid ρ.asModule

instance Representation.instInhabitedAsModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Inhabited ρ.asModule

noncomputable instance Representation.instModuleAsModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Module (MonoidAlgebra k G) ρ.asModule

A k-linear representation of G on V can be thought of as a module over MonoidAlgebra k G.

instance Representation.instModuleAsModule_1 {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Module k ρ.asModule

def Representation.asModuleEquiv {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : ρ.asModule ≃ₗ[k] V

The additive equivalence from the Module (MonoidAlgebra k G) to the original vector space of the representative.

This is just the identity, but it is helpful for typechecking and keeping track of instances.

@[simp]

theorem Representation.asModuleEquiv_map_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (r : MonoidAlgebra k G) (x : ρ.asModule) : ρ.asModuleEquiv (r • x) = (ρ.asAlgebraHom r) (ρ.asModuleEquiv x)

theorem Representation.asModuleEquiv_symm_map_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (r : k) (x : V) : ρ.asModuleEquiv.symm (r • x) = (algebraMap k (MonoidAlgebra k G)) r • ρ.asModuleEquiv.symm x

@[simp]

theorem Representation.asModuleEquiv_symm_map_rho {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (x : V) : ρ.asModuleEquiv.symm ((ρ g) x) = (MonoidAlgebra.of k G) g • ρ.asModuleEquiv.symm x

noncomputable def Representation.ofModule' {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_4) [AddCommMonoid M] [Module k M] [Module (MonoidAlgebra k G) M] [IsScalarTower k (MonoidAlgebra k G) M] : Representation k G M

Build a Representation k G M from a [Module (MonoidAlgebra k G) M].

This version is not always what we want, as it relies on an existing [Module k M] instance, along with a [IsScalarTower k (MonoidAlgebra k G) M] instance.

We remedy this below in ofModule (with the tradeoff that the representation is defined only on a type synonym of the original module.)

noncomputable def Representation.ofModule {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_4) [AddCommMonoid M] [Module (MonoidAlgebra k G) M] : Representation k G (RestrictScalars k (MonoidAlgebra k G) M)

Build a Representation from a [Module (MonoidAlgebra k G) M].

Note that the representation is built on restrictScalars k (MonoidAlgebra k G) M, rather than on M itself.

ofModule and asModule are inverses.

This requires a little care in both directions: this is a categorical equivalence, not an isomorphism.

See Rep.equivalenceModuleMonoidAlgebra for the full statement.

Starting with ρ : Representation k G V, converting to a module and back again we have a Representation k G (restrictScalars k (MonoidAlgebra k G) ρ.asModule). To compare these, we use the composition of restrictScalarsAddEquiv and ρ.asModuleEquiv.

Similarly, starting with Module (MonoidAlgebra k G) M, after we convert to a representation and back to a module, we have Module (MonoidAlgebra k G) (restrictScalars k (MonoidAlgebra k G) M).

@[simp]

theorem Representation.ofModule_asAlgebraHom_apply_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_4) [AddCommMonoid M] [Module (MonoidAlgebra k G) M] (r : MonoidAlgebra k G) (m : RestrictScalars k (MonoidAlgebra k G) M) : ((ofModule M).asAlgebraHom r) m = (RestrictScalars.addEquiv k (MonoidAlgebra k G) M).symm (r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) m)

@[simp]

theorem Representation.ofModule_asModule_act {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (x : RestrictScalars k (MonoidAlgebra k G) ρ.asModule) : ((ofModule ρ.asModule) g) x = (RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule).symm (ρ.asModuleEquiv.symm ((ρ g) (ρ.asModuleEquiv ((RestrictScalars.addEquiv k (MonoidAlgebra k G) ρ.asModule) x))))

theorem Representation.smul_ofModule_asModule {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] (M : Type u_4) [AddCommMonoid M] [Module (MonoidAlgebra k G) M] (r : MonoidAlgebra k G) (m : (ofModule M).asModule) : (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((ofModule M).asModuleEquiv (r • m)) = r • (RestrictScalars.addEquiv k (MonoidAlgebra k G) M) ((ofModule M).asModuleEquiv m)

@[simp]

theorem Representation.single_smul {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (t : k) (g : G) (v : ρ.asModule) : MonoidAlgebra.single g t • v = t • (ρ g) (ρ.asModuleEquiv v)

instance Representation.instIsScalarTowerMonoidAlgebraAsModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : IsScalarTower k (MonoidAlgebra k G) ρ.asModule

def Representation.norm {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [Fintype G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : Module.End k V

Given a representation (V, ρ) of a finite group G, norm ρ is the linear map V →ₗ[k] V defined by x ↦ ∑ ρ g x for g in G.

@[simp]

theorem Representation.norm_comp_self {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [Fintype G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) : ρ.norm ∘ₗ ρ g = ρ.norm

@[simp]

theorem Representation.norm_self_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [Fintype G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (x : V) : ρ.norm ((ρ g) x) = ρ.norm x

@[simp]

theorem Representation.self_comp_norm {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [Fintype G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) : ρ g ∘ₗ ρ.norm = ρ.norm

@[simp]

theorem Representation.self_norm_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [Fintype G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) (x : V) : (ρ g) (ρ.norm x) = ρ.norm x

def Representation.subrepresentation {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (W : Submodule k V) (le_comap : ∀ (g : G), W ≤ Submodule.comap (ρ g) W) : Representation k G ↥W

Given a k-linear G-representation (V, ρ), this is the representation defined by restricting ρ to a G-invariant k-submodule of V.

@[simp]

theorem Representation.subrepresentation_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (W : Submodule k V) (le_comap : ∀ (g : G), W ≤ Submodule.comap (ρ g) W) (g : G) : (ρ.subrepresentation W le_comap) g = (ρ g).restrict ⋯

def Representation.quotient {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (W : Submodule k V) (le_comap : ∀ (g : G), W ≤ Submodule.comap (ρ g) W) : Representation k G (V ⧸ W)

Given a k-linear G-representation (V, ρ) and a G-invariant k-submodule W ≤ V, this is the representation induced on V ⧸ W by ρ.

@[simp]

theorem Representation.quotient_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [AddCommGroup V] [Module k V] (ρ : Representation k G V) (W : Submodule k V) (le_comap : ∀ (g : G), W ≤ Submodule.comap (ρ g) W) (g : G) : (ρ.quotient W le_comap) g = W.mapQ W (ρ g) ⋯

theorem Representation.apply_eq_of_coe_eq {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [IsTrivial (MonoidHom.comp ρ S.subtype)] (g h : G) (hgh : ↑g = ↑h) : ρ g = ρ h

def Representation.ofQuotient {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] [IsTrivial (MonoidHom.comp ρ S.subtype)] : Representation k (G ⧸ S) V

Given a normal subgroup S ≤ G, a G-representation ρ which is trivial on S factors through G ⧸ S.

@[simp]

theorem Representation.ofQuotient_coe_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (S : Subgroup G) [S.Normal] [IsTrivial (MonoidHom.comp ρ S.subtype)] (g : G) (x : V) : ((ρ.ofQuotient S) ↑g) x = (ρ g) x

instance Representation.instAddCommGroupAsModule {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [I : AddCommGroup V] [Module k V] (ρ : Representation k G V) : AddCommGroup ρ.asModule

theorem Representation.apply_sub_id_partialSum_eq {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommRing k] [Monoid G] [I : AddCommGroup V] [Module k V] (ρ : Representation k G V) (n : ℕ) (g : G) (x : V) : (ρ g - LinearMap.id) (Fin.partialSum (fun (j : Fin (n + 1)) => (ρ (g ^ ↑j)) x) (Fin.last (n + 1))) = (ρ (g ^ (n + 1))) x - x

noncomputable def Representation.ofMulAction (k : Type u_1) [CommSemiring k] (G : Type u_2) [Monoid G] (H : Type u_3) [MulAction G H] : Representation k G (H →₀ k)

A G-action on H induces a representation G →* End(k[H]) in the natural way.

@[reducible, inline]

noncomputable abbrev Representation.leftRegular (k : Type u_1) [CommSemiring k] (G : Type u_2) [Monoid G] : Representation k G (G →₀ k)

The natural k-linear G-representation on k[G] induced by left multiplication in G.

@[reducible, inline]

noncomputable abbrev Representation.diagonal (k : Type u_1) [CommSemiring k] (G : Type u_2) [Monoid G] (n : ℕ) : Representation k G ((Fin n → G) →₀ k)

The natural k-linear G-representation on k[Gⁿ] induced by left multiplication in G.

theorem Representation.ofMulAction_def {k : Type u_1} [CommSemiring k] {G : Type u_2} [Monoid G] {H : Type u_3} [MulAction G H] (g : G) : (ofMulAction k G H) g = Finsupp.lmapDomain k k fun (x : H) => g • x

@[simp]

theorem Representation.ofMulAction_single {k : Type u_1} [CommSemiring k] {G : Type u_2} [Monoid G] {H : Type u_3} [MulAction G H] (g : G) (x : H) (r : k) : ((ofMulAction k G H) g) (Finsupp.single x r) = Finsupp.single (g • x) r

def Representation.ofDistribMulAction (k : Type u_1) (G : Type u_2) (A : Type u_3) [CommSemiring k] [Monoid G] [AddCommMonoid A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] : Representation k G A

Turns a k-module A with a compatible DistribMulAction of a monoid G into a k-linear G-representation on A.

@[simp]

theorem Representation.ofDistribMulAction_apply_apply {k : Type u_1} {G : Type u_2} {A : Type u_3} [CommSemiring k] [Monoid G] [AddCommMonoid A] [Module k A] [DistribMulAction G A] [SMulCommClass G k A] (g : G) (a : A) : ((ofDistribMulAction k G A) g) a = g • a

@[simp]

theorem Representation.norm_ofDistribMulAction_eq {k : Type u_1} {A : Type u_3} [CommSemiring k] [AddCommMonoid A] [Module k A] {G : Type u_4} [Group G] [Fintype G] [DistribMulAction G A] [SMulCommClass G k A] (x : A) : (ofDistribMulAction k G A).norm x = ∑ g : G, g • x

def Representation.ofMulDistribMulAction (M : Type u_1) (G : Type u_2) [Monoid M] [CommGroup G] [MulDistribMulAction M G] : Representation ℤ M (Additive G)

Turns a CommGroup G with a MulDistribMulAction of a monoid M into a ℤ-linear M-representation on Additive G.

@[simp]

theorem Representation.ofMulDistribMulAction_apply_apply (M : Type u_1) (G : Type u_2) [Monoid M] [CommGroup G] [MulDistribMulAction M G] (g : M) (a : Additive G) : ((ofMulDistribMulAction M G) g) a = Additive.ofMul (g • Additive.toMul a)

@[simp]

theorem Representation.norm_ofMulDistribMulAction_eq {G M : Type} [Group G] [Fintype G] [CommGroup M] [MulDistribMulAction G M] (x : Additive M) : Additive.toMul ((ofMulDistribMulAction G M).norm x) = ∏ g : G, g • Additive.toMul x

@[simp]

theorem Representation.ofMulAction_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] {H : Type u_4} [MulAction G H] (g : G) (f : H →₀ k) (h : H) : (((ofMulAction k G H) g) f) h = f (g⁻¹ • h)

noncomputable instance Representation.instHMulMonoidAlgebraAsModuleFinsuppOfMulAction {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] : HMul (MonoidAlgebra k G) (ofMulAction k G G).asModule (MonoidAlgebra k G)

theorem Representation.ofMulAction_self_smul_eq_mul {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (x : MonoidAlgebra k G) (y : (ofMulAction k G G).asModule) : x • y = x * y

noncomputable def Representation.ofMulActionSelfAsModuleEquiv {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] : (ofMulAction k G G).asModule ≃ₗ[MonoidAlgebra k G] MonoidAlgebra k G

If we equip k[G] with the k-linear G-representation induced by the left regular action of G on itself, the resulting object is isomorphic as a k[G]-module to k[G] with its natural k[G]-module structure.

@[simp]

theorem Representation.ofMulActionSelfAsModuleEquiv_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (a✝ : (ofMulAction k G G).asModule) : ofMulActionSelfAsModuleEquiv a✝ = (ofMulAction k G G).asModuleEquiv.toAddEquiv.toFun a✝

@[simp]

theorem Representation.ofMulActionSelfAsModuleEquiv_symm_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (a✝ : G →₀ k) : ofMulActionSelfAsModuleEquiv.symm a✝ = (ofMulAction k G G).asModuleEquiv.toAddEquiv.invFun a✝

def Representation.asGroupHom {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) : G →* (V →ₗ[k] V)ˣ

When G is a group, a k-linear representation of G on V can be thought of as a group homomorphism from G into the invertible k-linear endomorphisms of V.

theorem Representation.asGroupHom_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρ : Representation k G V) (g : G) : ↑(ρ.asGroupHom g) = ρ g

theorem Representation.leftRegular_norm_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] [Fintype G] : (leftRegular k G).norm = (LinearMap.lsmul k (G →₀ k)).flip ((leftRegular k G).norm (Finsupp.single 1 1)) ∘ₗ Finsupp.linearCombination k fun (x : G) => 1

theorem Representation.leftRegular_norm_eq_zero_iff {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] [Fintype G] (x : G →₀ k) : (leftRegular k G).norm x = 0 ↔ (Finsupp.linearCombination k fun (x : G) => 1) x = 0

theorem Representation.ker_leftRegular_norm_eq {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] [Fintype G] : LinearMap.ker (leftRegular k G).norm = LinearMap.ker (Finsupp.linearCombination k fun (x : G) => 1)

theorem Representation.apply_eq_of_leftRegular_eq_of_generator {k : Type u_1} {G : Type u_2} [CommSemiring k] [Group G] (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (x : G →₀ k) (hx : ((leftRegular k G) g) x = x) (γ : G) : x γ = x g

noncomputable def Representation.directSum {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {ι : Type u_3} {V : ι → Type u_4} [(i : ι) → AddCommMonoid (V i)] [(i : ι) → Module k (V i)] (ρ : (i : ι) → Representation k G (V i)) : Representation k G (DirectSum ι fun (i : ι) => V i)

Given representations of G on a family V i indexed by i, there is a natural representation of G on their direct sum ⨁ i, V i.

@[simp]

theorem Representation.directSum_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {ι : Type u_3} {V : ι → Type u_4} [(i : ι) → AddCommMonoid (V i)] [(i : ι) → Module k (V i)] (ρ : (i : ι) → Representation k G (V i)) (g : G) : (directSum ρ) g = DirectSum.lmap fun (x : ι) => (ρ x) g

noncomputable def Representation.prod {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) : Representation k G (V × W)

Given representations of G on V and W, there is a natural representation of G on their product V × W.

@[simp]

theorem Representation.prod_apply_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) (i : V × W) : ((ρV.prod ρW) g) i = ((ρV g) i.1, (ρW g) i.2)

noncomputable def Representation.tprod {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) : Representation k G (TensorProduct k V W)

Given representations of G on V and W, there is a natural representation of G on their tensor product V ⊗[k] W.

@[simp]

theorem Representation.tprod_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) : (ρV.tprod ρW) g = TensorProduct.map (ρV g) (ρW g)

theorem Representation.smul_tprod_one_asModule {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (r : MonoidAlgebra k G) (x : V) (y : W) : have x' := x; have z := x ⊗ₜ[k] y; r • z = (r • x') ⊗ₜ[k] y

theorem Representation.smul_one_tprod_asModule {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Monoid G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρW : Representation k G W) (r : MonoidAlgebra k G) (x : V) (y : W) : have y' := y; have z := x ⊗ₜ[k] y; r • z = x ⊗ₜ[k] (r • y')

def Representation.linHom {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) : Representation k G (V →ₗ[k] W)

Given representations of G on V and W, there is a natural representation of G on the module V →ₗ[k] W, where G acts by conjugation.

@[simp]

theorem Representation.linHom_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) (f : V →ₗ[k] W) : ((ρV.linHom ρW) g) f = ρW g ∘ₗ f ∘ₗ ρV g⁻¹

def Representation.dual {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρV : Representation k G V) : Representation k G (Module.Dual k V)

The dual of a representation ρ of G on a module V, given by (dual ρ) g f = f ∘ₗ (ρ g⁻¹), where f : Module.Dual k V.

@[simp]

theorem Representation.dual_apply {k : Type u_1} {G : Type u_2} {V : Type u_3} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] (ρV : Representation k G V) (g : G) : ρV.dual g = Module.Dual.transpose (ρV g⁻¹)

theorem Representation.dualTensorHom_comm {k : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring k] [Group G] [AddCommMonoid V] [Module k V] [AddCommMonoid W] [Module k W] (ρV : Representation k G V) (ρW : Representation k G W) (g : G) : dualTensorHom k V W ∘ₗ TensorProduct.map (ρV.dual g) (ρW g) = (ρV.linHom ρW) g ∘ₗ dualTensorHom k V W

Given $k$-modules $V, W$, there is a homomorphism $φ : V^* ⊗ W → Hom_k(V, W)$ (implemented by dualTensorHom in Mathlib/LinearAlgebra/Contraction.lean). Given representations of $G$ on $V$ and $W$,there are representations of $G$ on $V^* ⊗ W$ and on $Hom_k(V, W)$. This lemma says that $φ$ is $G$-linear.

noncomputable def Representation.finsupp {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} [AddCommMonoid A] [Module k A] (ρ : Representation k G A) (α : Type u_6) : Representation k G (α →₀ A)

The representation on α →₀ A defined pointwise by a representation on A.

theorem Representation.finsupp_apply {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {A : Type u_4} [AddCommMonoid A] [Module k A] (ρ : Representation k G A) (α : Type u_6) (g : G) : (ρ.finsupp α) g = (Finsupp.lsum k) fun (i : α) => Finsupp.lsingle i ∘ₗ ρ g

@[simp]

theorem Representation.finsupp_single {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : Type u_3} {A : Type u_4} [AddCommMonoid A] [Module k A] (ρ : Representation k G A) (g : G) (x : α) (a : A) : ((ρ.finsupp α) g) (Finsupp.single x a) = Finsupp.single x ((ρ g) a)

@[reducible, inline]

noncomputable abbrev Representation.free (k : Type u_6) (G : Type u_7) [CommSemiring k] [Monoid G] (α : Type u_8) : Representation k G (α →₀ G →₀ k)

The representation on α →₀ k[G] defined pointwise by the left regular representation.

noncomputable instance Representation.instAddCommGroupAsModuleFinsuppFree (k : Type u_6) (G : Type u_7) [CommRing k] [Monoid G] (α : Type u_8) : AddCommGroup (free k G α).asModule

theorem Representation.free_single_single {k : Type u_1} {G : Type u_2} [CommSemiring k] [Monoid G] {α : Type u_3} (g h : G) (i : α) (r : k) : ((free k G α) g) (Finsupp.single i (Finsupp.single h r)) = Finsupp.single i (Finsupp.single (g * h) r)

noncomputable def Representation.finsuppLEquivFreeAsModule (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : Type u_6) : (α →₀ MonoidAlgebra k G) ≃ₗ[MonoidAlgebra k G] (free k G α).asModule

The free k[G]-module on a type α is isomorphic to the representation free k G α.

noncomputable def Representation.freeAsModuleBasis (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : Type u_6) : Module.Basis α (MonoidAlgebra k G) (free k G α).asModule

α gives a k[G]-basis of the representation free k G α.

theorem Representation.free_asModule_free (k : Type u_1) (G : Type u_2) [CommSemiring k] [Monoid G] (α : Type u_6) : Module.Free (MonoidAlgebra k G) (free k G α).asModule