Addenda to the monoid algebra theory in mathlib

This file adds some properties about monoid algebra theory in mathlib.

Main results

The goal of this file is to add to the monoid algebra theory some preliminary results to construct the character on the induced representation by the center of a finite group. The main theorem proved here is the decomposition of MonoidAlgebra k G as a direct sum of g • MonoidAlgebra k (Subgroup.center G) indexed by elements of a system of representatives of G⧸ (Subgroup.center G) as defined in system_of_repr_center.set.

Contents

• Adds to MonoidAlgebratheory over a group, to create some particular tensor products.
• MonoidAlgebra_MulAction_basis : a system of representatives system_of_repr_center.set G of G⧸ (Subgroup.center G) defines a basis of MonoidAlgebra k G on MonoidAlgebra k (Subgroup.center G).
• MonoidAlgebra_direct_sum_system_of_repr_center.set : given a representative system system_of_repr_center.set G of G⧸ (Subgroup.center G), we have a MonoidAlgebra k (Subgroup.center G) linear bijection between MonoidAlgebra k G and the direct sum of g • (MonoidAlgebra k (Subgroup.center G)) for g : system_of_repr_center.set G.

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

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

Equations

• Fintype_G G = Fintype.ofFinite G

noncomputable def Map_kHkG (k G : Type) [inst1 : Field k] [inst2 : Group G] (H : Subgroup G) : MonoidAlgebra k ↥H →+* MonoidAlgebra k G

The trivial map from MonoidAlgebra k H to MonoidAlgebra k G, ie elements from MonoidAlgebra k H are seen as MonoidAlgebra k G.

Equations

• Map_kHkG k G H = MonoidAlgebra.mapDomainRingHom k H.subtype

@[simp]

theorem Map_kHkG_single_apply (k G : Type) [inst1 : Field k] [inst2 : Group G] (H : Subgroup G) (h : ↥H) (c : k) : (Map_kHkG k G H) (MonoidAlgebra.single h c) = MonoidAlgebra.single (↑h) c

@[simp]

theorem Map_kHkG_k_linear (k G : Type) [inst1 : Field k] [inst2 : Group G] (H : Subgroup G) (c : k) (x : MonoidAlgebra k ↥H) : (Map_kHkG k G H) (c • x) = c • (Map_kHkG k G H) x

Map_kHkG is indeed a k linear map.

noncomputable instance Coe_kH_kG (k G : Type) [inst1 : Field k] [inst2 : Group G] (H : Subgroup G) : CoeOut (MonoidAlgebra k ↥H) (MonoidAlgebra k G)

Coercion from MonoidAlgebra k H to MonoidAlgebra k G when H is a subgroup of G

Equations

• Coe_kH_kG k G H = { coe := ⇑(Map_kHkG k G H) }

noncomputable instance Smul_kHkG (k G : Type) [inst1 : Field k] [inst2 : Group G] (H : Subgroup G) : SMul (MonoidAlgebra k ↥H) (MonoidAlgebra k G)

Scalar multiplication between MonoidAlgebra k H and MonoidAlgebra k G, ie classical mulitplication between an element of MonoidAlgebra k H seen as an element of MonoidAlgebra k G and an element of MonoidAlgebra k G.

Equations

• Smul_kHkG k G H = { smul := fun (h : MonoidAlgebra k ↥H) (g : MonoidAlgebra k G) => (Map_kHkG k G H) h * g }

noncomputable instance kG_is_kCenter_Algebra (k G : Type) [inst1 : Field k] [inst2 : Group G] : Algebra (MonoidAlgebra k ↥(Subgroup.center G)) (MonoidAlgebra k G)

MonoidAlgebra k G is a MonoidAlgebra k (Subgroup.center G) algebra.

Equations

• kG_is_kCenter_Algebra k G = { toSMul := Smul_kHkG k G (Subgroup.center G), algebraMap := Map_kHkG k G (Subgroup.center G), commutes' := ⋯, smul_def' := ⋯ }

noncomputable instance kG_is_kH_Algebra (k G : Type) [inst1 : Field k] [inst2 : Group G] (H : Subgroup G) [instH : IsMulCommutative ↥H] (ϕ : ↥H →* ↥(Subgroup.center G)) : Algebra (MonoidAlgebra k ↥H) (MonoidAlgebra k G)

If we have a homomorphism H →* Subgroup.center G, then we have Algebra (MonoidAlgebra k H) (MonoidAlgebra k G).

Equations

• kG_is_kH_Algebra k G H ϕ = Algebra.compHom (MonoidAlgebra k G) (MonoidAlgebra.mapDomainRingHom k ϕ)

@[simp]

theorem center_commutes_single (k G : Type) [inst1 : Field k] [inst2 : Group G] (x : MonoidAlgebra k ↥(Subgroup.center G)) (g : G) : (Map_kHkG k G (Subgroup.center G)) x * MonoidAlgebra.single g 1 = MonoidAlgebra.single g 1 * (Map_kHkG k G (Subgroup.center G)) x

For every g : G, x : MonoidAlgebra k (Subgroup.center G) commutes with MonoidAlgebra.single g (1:k).

noncomputable instance Set_Coe (k G : Type) [inst1 : Field k] [inst2 : Group G] (H : Subgroup G) : CoeOut (Set (MonoidAlgebra k ↥H)) (Set (MonoidAlgebra k G))

Coercion from Set (MonoidAlgebra k H) to (Set (MonoidAlgebra k G)).

Equations

• Set_Coe k G H = { coe := fun (x : Set (MonoidAlgebra k ↥H)) => let_fun h := Map_kHkG k G H; let xG := {x_1 : MonoidAlgebra k G | ∃ a ∈ x, h a = x_1}; xG }

noncomputable def center_sub_module (k G : Type) [inst1 : Field k] [inst2 : Group G] : Submodule (MonoidAlgebra k ↥(Subgroup.center G)) (MonoidAlgebra k G)

(MonoidAlgebra k (Subgroup.center G)) seen as a subset of MonoidAlgebra k G is a (MonoidAlgebra k (Subgroup.center G)) submodule of (MonoidAlgebra k (Subgroup.center G)).

Equations

• center_sub_module k G = { carrier := {x : MonoidAlgebra k G | ∃ a ∈ Set.univ, (Map_kHkG k G (Subgroup.center G)) a = x}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable instance hmul_g_kH_kG (k G : Type) [inst1 : Field k] [inst2 : Group G] : HMul G (MonoidAlgebra k ↥(Subgroup.center G)) (MonoidAlgebra k G)

We define the multiplication of an element g : G by kH : MonoidAlgebra k (Subgroup.center G) by MonoidAlgebra.single g (1:k) * kH.

Equations

• hmul_g_kH_kG k G = { hMul := fun (g : G) (kH : MonoidAlgebra k ↥(Subgroup.center G)) => (MonoidAlgebra.of k G) g * (Map_kHkG k G (Subgroup.center G)) kH }

noncomputable instance hmul_g_kG (k G : Type) [inst1 : Field k] [inst2 : Group G] : HMul G (MonoidAlgebra k G) (MonoidAlgebra k G)

We define the multiplication of an element g: G by kG : MonoidAlgebra k G by MonoidAlgebra.single g (1:k) * kG.

Equations

• hmul_g_kG k G = { hMul := fun (g : G) (kH : MonoidAlgebra k G) => (MonoidAlgebra.of k G) g * kH }

theorem hmul_g_kH_kG_simp (k G : Type) [inst1 : Field k] [inst2 : Group G] (g : G) (kH : MonoidAlgebra k ↥(Subgroup.center G)) : g * kH = MonoidAlgebra.single g 1 * (Map_kHkG k G (Subgroup.center G)) kH

noncomputable def gkH_map (k G : Type) [inst1 : Field k] [inst2 : Group G] (g : G) : MonoidAlgebra k ↥(Subgroup.center G) →ₗ[k] MonoidAlgebra k G

Let g : G. We define a k linear map on MonoidAlgebra k (Subgroup.center G) by x ↦ g*x

Equations

• gkH_map k G g = Finsupp.lmapDomain k k fun (x : ↥(Subgroup.center G)) => g * ↑x

@[simp]

theorem gkH_map_eq (k G : Type) [inst1 : Field k] [inst2 : Group G] (g : G) (x : MonoidAlgebra k ↥(Subgroup.center G)) : (gkH_map k G g) x = g * x

For every x : MonoidAlgebra k (Subgroup.center G), we have gkH_map k G g x = g * x.

noncomputable def gkH_set (k G : Type) [inst1 : Field k] [inst2 : Group G] (g : G) : Submodule k (MonoidAlgebra k G)

The set of the image of gKh_map k G g, or in an equivalent manner the set of elements g*MonoidAlgebra k (Subgroup.center G) for g in G.

Equations

• gkH_set k G g = LinearMap.range (gkH_map k G g)

@[simp]

theorem gkH_map_gkh_set (k G : Type) [inst1 : Field k] [inst2 : Group G] {g : G} (x : ↥(gkH_set k G g)) : (gkH_map k G g) (Exists.choose ⋯) = ↑x

simp lemma for gkH_map.

noncomputable def gkH_set_iso_kH_k (k G : Type) [inst1 : Field k] [inst2 : Group G] (g : G) : ↥(gkH_set k G g) ≃ₗ[k] MonoidAlgebra k ↥(Subgroup.center G)

We have a k linear equivalence between MonoidAlgebra k (Subgroup.center G) and gkH_set k G g given by the map gkH_map.

Equations

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

noncomputable instance gkH_set_SMul (k G : Type) [inst1 : Field k] [inst2 : Group G] {g : G} : SMul (MonoidAlgebra k ↥(Subgroup.center G)) ↥(gkH_set k G g)

Equations

• gkH_set_SMul k G = { smul := fun (x : MonoidAlgebra k ↥(Subgroup.center G)) (h : ↥(gkH_set k G g)) => match h with | ⟨y, hy⟩ => ⟨(Map_kHkG k G (Subgroup.center G)) x * y, ⋯⟩ }

noncomputable instance gkH_set_MulAction (k G : Type) [inst1 : Field k] [inst2 : Group G] {g : G} : MulAction (MonoidAlgebra k ↥(Subgroup.center G)) ↥(gkH_set k G g)

Equations

• gkH_set_MulAction k G = { toSMul := gkH_set_SMul k G, one_smul := ⋯, mul_smul := ⋯ }

noncomputable instance gkH_set_DistribMulAction (k G : Type) [inst1 : Field k] [inst2 : Group G] {g : G} : DistribMulAction (MonoidAlgebra k ↥(Subgroup.center G)) ↥(gkH_set k G g)

Equations

• gkH_set_DistribMulAction k G = { toMulAction := gkH_set_MulAction k G, smul_zero := ⋯, smul_add := ⋯ }

noncomputable instance gkH_set_Module (k G : Type) [inst1 : Field k] [inst2 : Group G] {g : G} : Module (MonoidAlgebra k ↥(Subgroup.center G)) ↥(gkH_set k G g)

gkH_set k G g is a MonoidAlgebra k (Subgroup.center G) module.

Equations

• gkH_set_Module k G = { toDistribMulAction := gkH_set_DistribMulAction k G, add_smul := ⋯, zero_smul := ⋯ }

noncomputable def gkH_set_iso_kH_module (k G : Type) [inst1 : Field k] [inst2 : Group G] (g : G) : ↥(gkH_set k G g) ≃ₗ[MonoidAlgebra k ↥(Subgroup.center G)] MonoidAlgebra k ↥(Subgroup.center G)

We define a MonoidAlgebra k (Subgroup.center G) linear equivalence between gkH_set k G g and MonoidAlgebra k (Subgroup.center G) by $x ↦ g ⬝ x$.

Equations

• gkH_set_iso_kH_module k G g = ((Equiv.ofBijective (fun (x : MonoidAlgebra k ↥(Subgroup.center G)) => ⟨g * x, ⋯⟩) ⋯).toLinearEquiv ⋯).symm

@[simp]

theorem Map_kHkG_single_simp (k G : Type) [inst1 : Field k] [inst2 : Group G] {x : ↥(Subgroup.center G)} : ∀ (x✝ : ↥(Subgroup.center G)), (Map_kHkG k G (Subgroup.center G)) (Finsupp.basisSingleOne x) = Finsupp.single (↑x) 1

Coercion on the natural basis of MonoidAlgebra k G when g : Subgroup.center G.

noncomputable def MonoidAlgebra_MulAction_basis (k G : Type) [inst1 : Field k] [inst2 : Group G] [inst3 : Finite G] : Basis (↑(system_of_repr_center.set G)) (MonoidAlgebra k ↥(Subgroup.center G)) (MonoidAlgebra k G)

A system of representatives system_of_repr_center.set G of G⧸ (Subgroup.center G) defines a basis of MonoidAlgebra k G on MonoidAlgebra k (Subgroup.center G).

Equations

• MonoidAlgebra_MulAction_basis k G = Basis.mk ⋯ ⋯

@[simp]

theorem MonoidAlgebra_single_basis_simp (k G : Type) [inst1 : Field k] [inst2 : Group G] [inst3 : Finite G] {i : ↑(system_of_repr_center.set G)} (x1 : ↑(system_of_repr_center.set G)) : ((MonoidAlgebra_MulAction_basis k G).repr (MonoidAlgebra.single (↑x1) 1)) i = if i = x1 then 1 else 0

Given a representative x1 : system_of_repr_center G, the coefficients of x1 in the basis MonoidAlgebra_MulAction_basis is 0 unless on the vector x1.

noncomputable def G_to_direct_sum (k G : Type) [inst1 : Field k] [inst2 : Group G] : ↑(system_of_repr_center.set G) → DirectSum ↑(system_of_repr_center.set G) fun (x : ↑(system_of_repr_center.set G)) => MonoidAlgebra k ↥(Subgroup.center G)

We define a map between system_of_repr_center.set G and ⨁ (_ : ↑(system_of_repr_center.set G)), MonoidAlgebra k ↥(Subgroup.center G)) given by MonoidAlgebra.single 1 1 on the g-th component and 0 elsewhere.

Equations

• G_to_direct_sum k G g = (DirectSum.of (fun (g : ↑(system_of_repr_center.set G)) => MonoidAlgebra k ↥(Subgroup.center G)) g) (MonoidAlgebra.single 1 1)

noncomputable def MonoidAlgebra_direct_sum_linear (k G : Type) [inst1 : Field k] [inst2 : Group G] [inst3 : Finite G] : MonoidAlgebra k G →ₗ[MonoidAlgebra k ↥(Subgroup.center G)] DirectSum ↑(system_of_repr_center.set G) fun (x : ↑(system_of_repr_center.set G)) => MonoidAlgebra k ↥(Subgroup.center G)

We define a MonoidAlgebra k (Subgroup.center G) linear map by extending the map G_to_direct_sum k G which is define on the basis MonoidAlgebra_MulAction_basis k G.

Equations

• MonoidAlgebra_direct_sum_linear k G = ((MonoidAlgebra_MulAction_basis k G).constr k) (G_to_direct_sum k G)

noncomputable def MonoidAlgebra_direct_sum_1 (k G : Type) [inst1 : Field k] [inst2 : Group G] [inst3 : Finite G] : MonoidAlgebra k G ≃ₗ[MonoidAlgebra k ↥(Subgroup.center G)] DirectSum ↑(system_of_repr_center.set G) fun (x : ↑(system_of_repr_center.set G)) => MonoidAlgebra k ↥(Subgroup.center G)

The map MonoidAlgebra_direct_sum_linear k G is in fact a linear bijection.

Equations

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

noncomputable def MonoidAlgebra_direct_sum_system_of_repr_center_set (k G : Type) [inst1 : Field k] [inst2 : Group G] [inst3 : Finite G] : MonoidAlgebra k G ≃ₗ[MonoidAlgebra k ↥(Subgroup.center G)] DirectSum ↑(system_of_repr_center.set G) fun (g : ↑(system_of_repr_center.set G)) => ↥(gkH_set k G ↑g)

Given a representative system system_of_repr_center.set G of G⧸ (Subgroup.center G), we have a MonoidAlgebra k (Subgroup.center G) linear bijection between MonoidAlgebra k G and the direct sum of g • (MonoidAlgebra k (Subgroup.center G)) for g : system_of_repr_center.set G.

Equations

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