Addenda to the representation theory in mathlib

This file adds some properties about representation theory in mathlib.

Main results

The goal of this file is to formalize the induced representation by the center of finite groups and and the Frobenius reciprocity. We also aim to formalize the formula of the character of this induced representation.

Contents

• Induced_rep_center.tensor : the induced representation by Subgroup.center G as a tensor product.
• Induced_rep_center.iso_induced_as_tensor : given E a MonoidAlgebra k G module, the natural isomorphism between MonoidAlgebra k G-linear map from the induced representation tensor to Eand MonoidAlgebra k (Subgroup.center G)-linear map from our θ.asModule seen as tensor product over MonoidAlgebra k (Subgroup;center G)) to E : $Hom_{k[G]}(k[G]⊗_{k[Z(G)]}θ, E) ≃ Hom_{k[H]}(θ,E)$.
• Frobenius_reciprocity.Induced_character_is_character_induced_center : the induced character by Subgroup.center G is equal to the character of the induced representation by Subgroup.center G.

@[reducible, inline]

abbrev Induced_rep_center.tensor (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : Type

Induced representation on G by a representation Representation k (Subgroup.center G) W seen as a tensor product.

Equations

• Induced_rep_center.tensor k G W θ = TensorProduct (MonoidAlgebra k ↥(Subgroup.center G)) (MonoidAlgebra k G) θ.asModule

noncomputable instance Induced_rep_center.tensor_add_comm_mon (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : AddCommMonoid (tensor k G W θ)

tensor k G W θ is an AddCommMonoid.

Equations

• Induced_rep_center.tensor_add_comm_mon k G W θ = ⋯.mpr TensorProduct.addCommMonoid

noncomputable instance Induced_rep_center.tensor_module (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : Module (MonoidAlgebra k G) (tensor k G W θ)

tensor k G W θ is a MonoidAlgebra k G module.

Equations

• Induced_rep_center.tensor_module k G W θ = id TensorProduct.leftModule

noncomputable def Induced_rep_center.as_rep (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : Representation k G (RestrictScalars k (MonoidAlgebra k G) (tensor k G W θ))

Induced representation on G by a representation Representation k (Subgroup.center G) W seen as a representation.

Equations

• Induced_rep_center.as_rep k G W θ = Representation.ofModule (Induced_rep_center.tensor k G W θ)

def Induced_rep_center.module_sub_rep (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : Type

Subrepresentation of tensor as module.

Equations

• Induced_rep_center.module_sub_rep k G W θ = TensorProduct (MonoidAlgebra k ↥(Subgroup.center G)) (MonoidAlgebra k ↥(Subgroup.center G)) θ.asModule

noncomputable instance Induced_rep_center.Coe (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : CoeOut (module_sub_rep k G W θ) (tensor k G W θ)

Coercion from module_sub_rep to tensor.

Equations

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

noncomputable instance Induced_rep_center.module_sub_rep_addcommmon (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : AddCommMonoid (module_sub_rep k G W θ)

module_sub_rep is an additive commutative monoid.

Equations

• Induced_rep_center.module_sub_rep_addcommmon k G W θ = id TensorProduct.addCommMonoid

noncomputable instance Induced_rep_center.module_sub_rep_module (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : Module (MonoidAlgebra k ↥(Subgroup.center G)) (module_sub_rep k G W θ)

module_sub_rep is a MonoidAlgebra k (Subgroup.center G) module.

Equations

• Induced_rep_center.module_sub_rep_module k G W θ = id TensorProduct.instModule

noncomputable def Induced_rep_center.module_sub_rep_iso (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : module_sub_rep k G W θ ≃ₗ[MonoidAlgebra k ↥(Subgroup.center G)] θ.asModule

The tensor product module_sub_rep is lineary equivalent to θ.asModule (which is a specialization of a more specific theorem that I should implement : a ⨂ₐ M ≃ M)

Equations

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

noncomputable instance Induced_rep_center.tensor_module_sub (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : Module (MonoidAlgebra k ↥(Subgroup.center G)) (tensor k G W θ)

tensor k G W θ is a MonoidAlgebra k ↥(Subgroup.center G) module.

Equations

• Induced_rep_center.tensor_module_sub k G W θ = id { toDistribMulAction := TensorProduct.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

noncomputable def Induced_rep_center.subrep_sub_module (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : Submodule (MonoidAlgebra k ↥(Subgroup.center G)) θ.asModule

θ.asModule is a (MonoidAlgebra k (Subgroup.center G)) submodule over itself.

Equations

• Induced_rep_center.subrep_sub_module k G W θ = { carrier := Set.univ, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable def Induced_rep_center.subrep_sub_module_iso (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : θ.asModule ≃ₗ[MonoidAlgebra k ↥(Subgroup.center G)] ↥(subrep_sub_module k G W θ)

θ.asModule is isomorphic to itself seen as a submodule.

Equations

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

noncomputable def Induced_rep_center.is_sub_rep_submodule_iso (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : Submodule (MonoidAlgebra k ↥(Subgroup.center G)) (tensor k G W θ)

TensorProduct (MonoidAlgebra k (Subgroup.center G)) θ.asModule is a (MonoidAlgebra k (Subgroup.center G)) submodule of tensor k G W θ.

Equations

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

noncomputable def Induced_rep_center.subsubsub (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : Submodule (MonoidAlgebra k ↥(Subgroup.center G)) (tensor k G W θ)

The image of θ.asModule by module_sub_rep_iso is a submodule of tensor k G W θ, ie θ.asModule is a subrepresentation of the induced representation

Equations

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

noncomputable def Induced_rep_center.subrep (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : θ.asModule ≃ₗ[MonoidAlgebra k ↥(Subgroup.center G)] ↥(subsubsub k G W θ)

Equations

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

noncomputable def Induced_rep_center.iso_induced_as_tensor (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) (E : Type u_1) [AddCommMonoid E] [Module (MonoidAlgebra k G) E] [Module (MonoidAlgebra k ↥(Subgroup.center G)) E] [inst6 : IsScalarTower (MonoidAlgebra k ↥(Subgroup.center G)) (MonoidAlgebra k G) E] : (tensor k G W θ →ₗ[MonoidAlgebra k G] E) ≃ₗ[MonoidAlgebra k ↥(Subgroup.center G)] module_sub_rep k G W θ →ₗ[MonoidAlgebra k ↥(Subgroup.center G)] E

Given E a MonoidAlgebra k G module, the natural isomorphism between MonoidAlgebra k G-linear map from the induced representation tensor to Eand MonoidAlgebra k (Subgroup.center G)-linear map from our θ.asModule seen as tensor product over MonoidAlgebra k (Subgroup;center G)) to E : $Hom_{k[G]}(k[G]⊗_{k[Z(G)]}θ, E) ≃ Hom_{k[H]}(θ,E)$.

Equations

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

instance Frobenius_reciprocity.Finite_H (G : Type) [inst2 : Group G] [inst3 : Finite G] (H : Subgroup G) : Finite ↥H

noncomputable instance Frobenius_reciprocity.Fintype_G (G : Type) [inst3 : Finite G] : Fintype G

Equations

• Frobenius_reciprocity.Fintype_G G = Fintype.ofFinite G

class Frobenius_reciprocity.conj_class_fun (G W : Type) [inst2 : Group G] : Type

Definition of a class function : given G a group, a class function is a function $f : G → G$ which is contant over the conjugacy classes of $G$.

• Fun : G → W
• conj_property (x g : G) : Fun (g⁻¹ * x * g) = Fun x

noncomputable def Frobenius_reciprocity.Ind_conj_class_fun (G W : Type) [inst2 : Group G] [inst3 : Finite G] [inst4 : AddCommGroup W] (H : Subgroup G) (f : ↥H → W) : conj_class_fun G W

Definition of the induced class function of a function

Equations

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

noncomputable instance Frobenius_reciprocity.character_as_conj_class_fun (k G : Type) [inst1 : Field k] [inst2 : Group G] (U : FDRep k G) : conj_class_fun G k

The character of a representation seen as a conj_class_fun.

Equations

• Frobenius_reciprocity.character_as_conj_class_fun k G U = { Fun := U.character, conj_property := ⋯ }

@[simp]

theorem Frobenius_reciprocity.character_as_conj_class_fun_is_character (k G : Type) [inst1 : Field k] [inst2 : Group G] (U : FDRep k G) : conj_class_fun.Fun = U.character

noncomputable instance Frobenius_reciprocity.tensor_addcommgroup_restrictscalars (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : AddCommGroup (RestrictScalars k (MonoidAlgebra k G) (Induced_rep_center.tensor k G W θ))

Equations

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

noncomputable instance Frobenius_reciprocity.tensor_module_restrictscalars (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : Module k (RestrictScalars k (MonoidAlgebra k G) (Induced_rep_center.tensor k G W θ))

Equations

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

instance Frobenius_reciprocity.tensor_module_restrictscalars_isfinite (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : Module.Finite k (RestrictScalars k (MonoidAlgebra k G) (Induced_rep_center.tensor k G W θ))

instance Frobenius_reciprocity.tensor_semisimple (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst3 : Finite G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) [h : NeZero ↑(Fintype.card G)] : IsSemisimpleModule (MonoidAlgebra k G) (Induced_rep_center.tensor k G W θ)

tensor is a semisimple module.

@[reducible, inline]

abbrev Frobenius_reciprocity.induced_rep_tensor_direct_sum_component (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) (g : ↑(system_of_repr_center.set G)) : Type

Equations

• Frobenius_reciprocity.induced_rep_tensor_direct_sum_component k G W θ g = TensorProduct (MonoidAlgebra k ↥(Subgroup.center G)) (↥(gkH_set k G ↑g)) θ.asModule

noncomputable instance Frobenius_reciprocity.instModuleMonoidAlgebraSubtypeMemSubgroupCenterInduced_rep_tensor_direct_sum_component (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) (g : ↑(system_of_repr_center.set G)) : Module (MonoidAlgebra k ↥(Subgroup.center G)) (induced_rep_tensor_direct_sum_component k G W θ g)

Equations

• Frobenius_reciprocity.instModuleMonoidAlgebraSubtypeMemSubgroupCenterInduced_rep_tensor_direct_sum_component k G W θ g = TensorProduct.instModule

noncomputable def Frobenius_reciprocity.induced_rep_tensor_iso_direct_sum (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst3 : Finite G] [inst4 : AddCommGroup W] [inst5 : Module k W] (θ : Representation k (↥(Subgroup.center G)) W) : Induced_rep_center.tensor k G W θ ≃ₗ[MonoidAlgebra k ↥(Subgroup.center G)] DirectSum ↑(system_of_repr_center.set G) fun (g : ↑(system_of_repr_center.set G)) => induced_rep_tensor_direct_sum_component k G W θ g

The induced representation Induced_rep_center.tensor k G W θ is isomorphic to a direct sum of induced_rep_tensor_direct_sum_component.

Equations

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

theorem Frobenius_reciprocity.Induced_character_is_character_induced_center (k G W : Type) [inst1 : Field k] [inst2 : Group G] [inst3 : Finite G] [inst4 : AddCommGroup W] [inst5 : Module k W] [inst6 : Module.Finite k W] (θ : Representation k (↥(Subgroup.center G)) W) [h : NeZero ↑(Fintype.card G)] : character_as_conj_class_fun k G (FDRep.of (Induced_rep_center.as_rep k G W θ)) = Ind_conj_class_fun G k (Subgroup.center G) conj_class_fun.Fun

Given the character of a representation θ of Subgroup.center G on k, the character of the induced representation tensor on G is the Ind_conj_class_fun of the character of θ.