1 Addenda to mathlib
This chapter introduces results that weren’t in mathlib (or that were in it but needed reformulation to stuck to our situation) and that are mandatory for our goal.
1.1 Group theory
In this section, we fix \(G\) group and \(H\) a commutative sugroup of \(G\). We denote by \(\mathcal{Z}_G\) the center of \(G\) and by \(e_G\) the neutral of \(G\).
1.1.1 Two lemmas about the center of a group
If \(h\) is an element of the center of \(G\), it commutes with every element of \(G\).
Trivial, just a reformulation in terms of type instead of memebership, useful for the \(LEAN\) part.
Let \(h\in \mathcal{Z}_G\) such that \(h=ab\) for some \((a,b)\in G^2\). Then, we also have \(h=ba\).
Suppose \(h=ab\). Then \(a=hb^{-1}=b^{-1}h\) because \(h\in \mathcal{Z}_G\). Thus \(ba=h\).
1.1.2 Quotient of a group by its center
We define the system of representatives of \(G/\mathcal{Z}_G\) by picking up exactly one element in every classes. We denote it by \(\mathcal{S}_{G/\mathcal{Z}_G}\) from now on and denote by \(C_s\) the classe of \(s\).
To do that in \(LEAN\), we take the image of \(G\) by the map \(G \rightarrow G/\mathcal{Z}_G\to G\).
If \(G\) is finite, then the system of representatives of \(G/\mathcal{Z}_G\) is finite too.
trivial
Given \(g\) and \(g'\) in the set of representatives of \(G/\mathcal{Z}_G\), if \(g\ne g'\) then the classes of \(g\) and \(g'\) are disjoint.
Suppose that the classes aren’t disjoints. Then there exists \(y\) such that \(y\sim g\) and \(y\sim g'\). Thus \(g \sim g'\) and their classes are equal. But \(g\) and \(g'\) belongs to the set of representatives. Thus \(g=g'\).
We have \(\bigcup \limits _{s\in \mathcal{S}_{G/\mathcal{Z}_G}} C_s= G\).
If \(x\) is in the union, in particular it belongs to \(G\). Let now \(g\) be an element of \(G\) and let show that it belongs to one of the classes. We apply the map defines in 3 to \(g\) and check that \(g\) belongs to the class of this element.
We have a bijection between \(\mathcal{S}_{G/\mathcal{Z}_G}\) and \(\{ \bar{g} \in G/\mathcal{Z}_G\} \) given by the map \(s\to \bar{s}\).
We check it is a bijection.
We define a map \(\varphi _{G\mathcal{S}} : G \rightarrow \mathcal{S}_{G/\mathcal{Z}_G}\) that send every \(g\in G\) to its representative.
For every \(g\in G\) and \(h\in \mathbb {Z}_G\), we have \(\varphi _{G\mathcal{S}}(gh)=\varphi _{G\mathcal{S}} (g)\).
By definition \(g*h\) belongs to the orbit of \(g\), thus they have the same representative.
We define a map \(\psi _{G\mathcal{Z}_G} : G \rightarrow \mathcal{Z}_G\) that send every \(g\in G\) to the corresponding \(h\in \mathcal{Z}_G\) such that \(g=sh\) where \(s\) is the representative of \(g\).
For every \(g\in G\) the following identity holds : \(g=\varphi _{G\mathcal{S}}(g) \psi _{G\mathcal{Z}_G}(g)\).
By definition of \(G/\mathcal{Z}_G\).
For every \(g\in G\) the following identity holds : \(\psi _{G\mathcal{Z}_G}(g)=g\varphi _{G\mathcal{S}}(g)^{-1}\).
Trivial with 11
For every \(g\in \mathcal{S}_{G/\mathcal{Z}_G}\), we have \(\psi _{G\mathcal{Z}_G}(g)=e_G\).
By definition of the map \(\psi _{G\mathcal{Z}_G}\).
For every \(g\in \mathcal{S}_{G/\mathcal{Z}_G}\), we have \(\varphi _{G\mathcal{S}}(g)=g\).
For every \(g\in G\) and \(h\in \mathcal{Z}_G\), we have \(\psi _{G\mathcal{Z}_G}(gh)=h\psi _{G\mathcal{Z}_G}(g)\).
With 12 we have \(\psi _{G\mathcal{Z}_G}(g)=g\varphi _{G\mathcal{S}}(g)^{-1}\) and \(\psi _{G\mathcal{Z}_G}(gh)=gh\varphi _{G\mathcal{S}}(gh)^{-1}\). But with 9, we have \(\varphi _{G\mathcal{S}}(gh)=\varphi _{G\mathcal{S}} (g)\). Thus, \(\psi _{G\mathcal{Z}_G}(gh)=gh\varphi _{G\mathcal{S}}(gh)^{-1}=gh\varphi _{G\mathcal{S}} (g)^{-1}= hg\varphi _{G\mathcal{S}} (g)^{-1}=h\psi _{G\mathcal{Z}_G}(g)\) with the first equality.
We define a bijection from \(G\) to \(\mathcal{Z}_G\times \mathcal{S}_{G/\mathcal{Z}_G}\) by \(g\mapsto (\psi _{G\mathcal{Z}_G}(g),\varphi _{G\mathcal{S}} (g))\).
We check the axioms of a bijection.
The bijection 16 empacked as Sigma type instead of cartesian product. Useful for \(LEAN\).
We have \(G = \{ gh,\ g\in \mathcal{S}_{G/\mathcal{Z}_G},\ h\in \mathcal{Z}_G\} \).
The inclusion \(\{ gh,\ g\in \mathcal{S}_{G/\mathcal{Z}_G},\ h\in \mathcal{Z}_G\} \) is trivial. The converse is given by 12.
1.2 Direct sums and tensor products
1.2.1 Direct sums
If we have two families \((\beta _i)_{i\in I}\) and \((\gamma _i)_{i\in I}\) of additive commutative monoids such that for every \(i\in I\), we have an additive bijection \(\varphi _i\) between \(\beta _i\) and \(\gamma _i\), then we have an additive bijection between \(\bigoplus \limits _{i\in I}\beta _i\) and \(\bigoplus \limits _{i\in I}\gamma _i\).
We send \(\sum \limits _{i\in I}x_i\) on \(\sum \limits _{i\in I}\varphi (x_i)\) and we check that it’s an additive bijection.
Let \(A\) be a semiring. If we have two families \((\beta _i)_{i\in I}\) and \((\gamma _i)_{i\in I}\) of additive commutative monoids such that for every \(i\in I\), \(\beta _i\) and \(\gamma _i\) are \(A-\)module and we have a \(A-\)linear bijection \(\varphi _i\) between \(\beta _i\) and \(\gamma _i\), then we have a \(A\) linear bijection between \(\bigoplus \limits _{i\in I}\beta _i\) and \(\bigoplus \limits _{i\in I}\gamma _i\).
We take the map defined in 19 which became \(A-\)linear by the new properties of the \(\beta _i\) and \(\gamma _i\).
Let \(I\) be a finite set and \((\beta _i)_{i\in I}\) a family of additive commutative monoids. Let \(\Phi \) be the natural map sending \(\beta _{i_0}\) to \(\bigoplus \limits _{i\in I}\beta _i\). Then, for every \(x:=(x_i)_{i\in I}\) such that \(x_i\in \beta _i\) for all \(i\in I\), then for every \(j\in I\), the following equality holds : \(\left(\sum \limits _{i\in I} \Phi (x_i)\right)_j=x_j\).
We obvioulsy have \(\left(\sum \limits _{i\in I} \Phi (x_i)\right)=\sum \limits _{i\in I}x_i\), which immediately gives the result.
1.2.2 Tensor products
Let \(A\) be ring, \(B\) an \(A-\)algebra, \(M\) an \(A-\)module and \(N\) a \(B-\)module. Then, \(\text{Hom}_B((B\otimes _AM),N)\cong \text{Hom}_A(M,N)\).
We consider the map sending \(\varphi \in \text{Hom}_B((B\otimes _AM),N)\) to the \(A-\)linear map \(\Phi _\varphi : M \rightarrow N\) defined by \(\Phi _\varphi (x)=\varphi (1\otimes _A x)\) for every \(x\in M\). It is injective : if \(\Phi _{\varphi _1}=\Phi _{\varphi _2}\), then \(\varphi _1(1\otimes _A x)=\varphi _2(1\otimes _A x)\) for every \(x\in M\). Thus \(\varphi _1=\varphi _2\) by \(B-\)linearity. It is surjective : let \(\varphi \) be a \(A\)-linear map from \(M\) to \(N\). Let consider the \(B-\)linear map \(\psi \) from \(B\otimes _AM\) to \(N\) define by \(\psi (b\otimes _A m) = b \varphi (m)\). We have then \(\Psi _\psi (x)=\psi (1\otimes _A x)= \varphi (x)\).
1.3 Group algebra
A lot of the results in this section wouldn’t really appear in classical mathematics papers, but they are needed to ensure that LEAN understand the operations we will do later.
From now on, \(\mathbb {K}\) is a field, \(G\) is a group and \(H\) is a subgroup of \(G\). We define \(mathcal{Z}_G\) as the center of \(G\).
1.3.1 Setting up operations, coercions and instances in LEAN
Given \(\mathbb {K}\) a field, \(G\) a group and \(H\) a subgroup of \(G\), we have a trivial ring homomorphism \(\varphi _{kHkG}\) from \(\mathbb {K}[H]\) to \(\mathbb {K}[G]\).
Trivial.
Trivial.
We have an equality between \(h\in H\) seen as an element of \(\mathbb {K}[H]\) and \(h\) (seen as an element of \(G\)) seens as an element of \(\mathbb {K}[G]\).
Some LEAN stuff.
Trivial.
We define a coercion from elements of \(\mathbb {K}[H]\) to \(\mathbb {K}[G]\) by the map defined in 23.
Some LEAN stuff.
We define a coercion from sets of elements of \(\mathbb {K}[H]\) to sets of elements of \(\mathbb {K}[G]\) by the map defined in 23.
Some LEAN stuff.
We define a multiplication between elements of \(\mathbb {K}[H]\) and elements of \(\mathbb {K}[G]\) by \(kH*kG=\varphi _{kHkG}(kH)\times kG\).
Some LEAN stuff.
\(\mathbb {K}[G]\) is a \(\mathbb {K}[\mathcal{Z}_G]\) algebra.
We check the axiom of an algebra.
If there exists a morphism from \(H\) to \(\mathcal{Z}_G\), then \(\mathbb {K}[G]\) is a \(\mathbb {K}[H]\) algebra.
We check the axiom of an algebra with the action of \(\mathbb {K}[H]\) on \(\mathbb {K}[G]\) given by the morphism.
Let \(x\in \mathbb {K}[\mathcal{Z}_G]\) and \(g\in G\). Then \(g\times x = x \times g\).
We have \(g\times x = g\times \sum \limits _{h\in \mathcal{Z}_g}a_hh=\sum \limits _{h\in \mathcal{Z}_g}a_hgh =\sum \limits _{h\in \mathcal{Z}_g}a_hhg=\left(\sum \limits _{h\in \mathcal{Z}_g}a_hgh\right)\times g\).
\(\mathbb {K}[\mathcal{Z}_G]\) defines a \(\mathbb {K}[G]\) submodule.
We check the axioms.
We define the multiplciation of elements \(g\in G\) and \(kH\in \mathbb {K}[\mathcal{Z}_G]\) in \(\mathbb {K}[G]\) by \(g\times kH=g\times \varphi _{kHkG}\)
Some LEAN stuff.
We define the multiplciation of elements \(g\in G\) and \(kG\in \mathbb {K}[G]\) in \(\mathbb {K}[G]\) by \(g\times kG\).
Some LEAN stuff.
Elements of \(G\) are distributive over \(\mathbb {K}[\mathcal{Z}_G]\)
Trivial, LEAN stuff.
1.3.2 Splitting of a group algebra as a direct sum
We use the notation of the section 1 concerning \(G/\mathcal{Z}_G\) The main goal of this part is to formalize the following result : \(\mathbb {K}[G] \cong \bigoplus \limits _{g\in \mathcal{S}_{G/\mathcal{Z}_G} } g \mathbb {K}[\mathcal{Z}_G]\).
Let \(g\in G\) be fixed. The morphism \(\varphi _g : \mathcal{Z}_G\rightarrow G\) defined by \(\varphi _G(x)=gx\) induced a \(\mathbb {K}\)-linear map \(\Gamma _g\) from \(\mathbb {K}[\mathcal{Z}_G]\) to \(\mathbb {K}[G]\).
Trivial.
Trivial.
For all \(x\in \mathbb {K}[\mathcal{Z}[G]]\), we have \(\Gamma _g(x)=g\times x\)
LEAN stuff to setup a simp lemma.
We define the set \(\Omega _g\) to be the image of \(\mathbb {K}[\mathcal{Z}_G]\) by \(\Gamma _G\).
Nothing useful mathematically, it’s just simpler for translating LEAN stuff.
The map \(\Gamma _g\) defines a \(k\)-linear bijection between \(\Omega _g\) and \(\mathbb {K}[\mathcal{Z}_G]\).
It’s injective like we saw before, and \(g^{-1}\times x\) is a preimage for \(x\).
We will now put some structure on \(\Omega _g\) to makes it understand by LEAN as a \(\mathbb {K}[\mathcal{Z}_G]\) module.
We define a multiplication between \(x\in \mathbb {K}[\mathcal{Z}_G]\) and \(y\in \Omega _g\) by \(x\times y\).
LEAN stuff.
The multiplication defined in 42 induced an action of \(\mathbb {K}[\mathcal{Z}_G]\) on \(\Omega _g\).
We check the axioms.
We check the axioms.
\(\Omega _g\) is a \(\mathbb {K}[\mathcal{Z}_G]\) module for the action defined in 43.
We check the axioms.
The bijection defined in 41 is indeed a \(\mathbb {K}[\mathcal{Z}_G]\)-linear map.
We check the linearity.
Elements of \(\mathcal{S}_{G/\mathcal{Z}_G}\) seen as elements of \(\mathbb {K}[G]\) defined a basis of \(\mathbb {K}[G]\) as a \(\mathbb {K}[\mathcal{Z}_G]\) algebra.
We show the independence of the family and then that it generates the whole algebra.
We suppose that there exists a family \((a_i)_{i\in \mathcal{S}_{G/\mathcal{Z}_G}}\) of elements of \(\mathbb {K}[\mathcal{Z}_G]\) such that
Using the fact that the family \((h)_{h\in \mathcal{Z}_G}\) seen as a family of elements of \(\mathbb {K}[\mathcal{Z}_G]\) is indeed a basis of \(\mathbb {K}[\mathcal{Z}_G]\) as a \(\mathbb {K}\) vector space we get :
where the \(a_{ih}\) are elements of \(\mathbb {K}\). Those sums are finite, and moreover, the family \((ih)_{(i,h)\in \mathcal{S}_{G/\mathcal{Z}_G}\times \mathcal{Z}_G}\) is a partition of \(G\).
Thus, we get :
which is equal to 0. But \((g)_{g\in G}\) seen as a family of elements of \(\mathbb {K}[G]\) is a basis of \(\mathbb {K}[G]\) as a \(\mathbb {K}\) vector space. Finally, \(\forall g\in G,\ a_g=0\) and the family is independent.
Let shows the family generates the whole algebra. Let \(x\in \mathbb {K}[G]\). Using the natural basis \(G\) of \(\mathbb {K}[G]\) and that \((ih)_{(i,h)\in \mathcal{S}_{G/\mathcal{Z}_G}\times \mathcal{Z}_G}\) is a partition of \(G\), we get :
So it generates the whole algebra and finally we get a basis.
We define a map on \(\mathcal{S}_{G/\mathcal{Z}_G}\) that associates to every elements \(g\in \mathcal{S}_{G/\mathcal{Z}_G}\) the natural element of \(\bigoplus \limits _{s\in \mathcal{S}_{G/\mathcal{Z}_G}}\mathbb {K}[\mathcal{Z}_G]\), that is \(1\) of \(\mathbb {K}[\mathcal{Z}_G]\) on the \(g-\)th component and 0 elsewhere.
The map defined in 49 is in fact an isomorphism.
We give an explicit inverse which is \((x_1,\dots ,x_g)\mapsto \sum \limits _{g\in \mathcal{S}_{G/\mathcal{Z}_G}} x_gg\).
1.4 Representation theory
The main goals of this part is to build the representation induced by the center \(\mathcal{Z}_G\) of a group \(G\) and its basic properties, and to formalize its character.
From now on, \(\mathbb {K}\) is a field and \(G\) is a group. We denote by \(\mathcal{Z}_G\) its center. \(W\) is a \(\mathbb {K}-\)vector space. Finally, \(\theta \) is a representation of \(\mathcal{Z}_G\) in \(W\).
1.4.1 Building the induced representation
Given \(G\) a group, \(\mathbb {K}\) a field, \(W\) a \(k\) vector space and \(\theta \) a representation of \(\mathcal{Z}_G\) on \(W\), we define the tensor product \(V:=\mathbb {K}[G]\otimes _{\mathbb {K}[\mathcal{Z}_G]}V_\theta \), where \(V_\theta \) is the \(\mathbb {K}[\mathcal{Z}_G]\) module associated to \(\theta \).
It comes from the fact that \(\mathbb {K}[G]\) and \(\mathbb {K}[\mathcal{Z}_G]\) are additive commutative monoids.
We do mettre la preuve.
We do mettre la preuve.
The \(V\) defined in 52 defined a representation of \(G\) called the induced representation by \(\mathcal{Z}_G\).
We define the subrepresentation of 56 by \(\mathbb {K}[\mathcal{Z}_G]\otimes _{\mathbb {K}[\mathcal{Z}_G]}V_\theta \), where \(V_\theta \) is the \(\mathbb {K}[\mathcal{Z}_G]\) module associated to \(\theta \).
It comes from general properties of tensor products.
It comes from general properties of tensor products.
The induced representation defined in 56 is a \(\mathbb {K}[\mathcal{Z}_G]\) module.
It comes from general properties of tensor products.
We have an isomorphism between \(\mathbb {K}[\mathcal{Z}_G]\otimes _{\mathbb {K}[\mathcal{Z}_G]}V_\theta \) and \(V_\theta \).
It comes from a special case of a theorem à ajouter.
We have a coercion from element of type \(\mathbb {K}[\mathcal{Z}_G]\otimes _{\mathbb {K}[\mathcal{Z}_G]}V_\theta \) to element of type \(\mathbb {K}[G]\otimes _{\mathbb {K}[\mathcal{Z}_G]}V_\theta \).
It comes from 23.
We have a coercion from element of type \(Set : \mathbb {K}[\mathcal{Z}_G]\otimes _{\mathbb {K}[\mathcal{Z}_G]}V_\theta \) to element of type \(Set : \mathbb {K}[G]\otimes _{\mathbb {K}[\mathcal{Z}_G]}V_\theta \).
It comes from 23.
The set of elements of \(V_\theta \) defines a \(\mathbb {K}[\mathcal{Z}_G]\)-submodule of itself.
Trivial.
The submodule defined in 64 is isomorphic to \(V_\theta \).
Trivial.
Trivial.
The image of \(V_\theta \) by 61 defines a \(\mathbb {K}[\mathcal{Z}_G]\)-submodule of \(\mathbb {K}[G]\otimes _{\mathbb {k}[\mathcal{Z}_G]}V_\theta \), ie \(V_\theta \) is a subrepresentation of the induced.
Compute the axioms.
Let \(E\) be a \(\mathbb {K}[G]\) module. We have an isomorphism \(Hom_{\mathbb {K}[G]} \left(\mathbb {K}[G]\otimes _{\mathbb {K}[\mathcal{Z}_G]}V_\theta ,\ E\right)\simeq Hom_{\mathbb {K}[\mathcal{Z}_G]} \left(\mathbb {K}[\mathcal{Z}_G]\otimes _{\mathbb {K}[\mathcal{Z}_G]}V_\theta ,\ E\right)\).
We use ?? two times.
1.4.2 Character of the induced representation
Given \(G\) a group, a function \(f\) over \(G\) is called central if it is constant on the conjugacy classes of \(G\) : \(f(g^{-1}xg)=f(x)\) for all \(g\in G\) and \(x\in G\).
If \(H\) is a subgroup of \(G\) a finite group, and if \(f\) is a function over \(H\), we define a central function \(f_G\) over \(G\) (called the induced central function on \(f\)) by the formula :
We check the axiom by reordering the sum with the bijection \(x\mapsto g^{-1}x\).
A character is of course a central function over \(G\). We empacked this definition in Lean.
Trivial.
If \(|G|\nmid Char(k)\), then the module defined in 52 is semisimple.
Consequences of .
We define the \(\mathbb {K}[\mathcal{Z}_G]\) module \(W_g:= g\mathbb {K}[\mathcal{Z}_G]\otimes _{\mathbb {K}[\mathcal{Z}_G]}V_\theta \) for \(g\in \mathcal{S}_{G/\mathcal{Z}_G}\).
We have an isomorphism between \(\mathbb {K}[G]\otimes _{\mathbb {K}[\mathcal{Z}_G]}V_\theta \) and \(\bigoplus \limits _{g\in \mathcal{S}_{G/\mathcal{Z}_G}}W_g=\bigoplus \limits _{g\in \mathcal{S}_{G/\mathcal{Z}_G}} g \mathbb {K}[\mathcal{Z}_G] \otimes _{\mathbb {K}[\mathcal{Z}_G]} V_\theta \).
We get the resultat with the isomorphism \(\mathbb {K}[G] \cong \otimes _{\mathbb {K}[\mathcal{Z}_G]} g\mathbb {K}[\mathcal{Z}_G]\) defined in 51.