Dependencies

Under our identification of the bidual, the map \(\Phi : (z,x,y) \mapsto (z,y,x)\) defines a bijection between \(\mathcal{H}(V)\) and \(\mathcal{H}(V^*)\).

We define the center of \(\mathcal{H}(V)\) by the set \(\mathcal{Z}_{\mathcal{H}(V)}:=\{ (z,0,0)\in \mathcal{H}(V),\ z\in k\} \)

\(\mathbb {K}[\mathcal{Z}_G]\) defines a \(\mathbb {K}[G]\) submodule.

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\).

A character is of course a central function over \(G\). We empacked this definition in Lean.

We define a coercion from elements of \(\mathbb {K}[H]\) to \(\mathbb {K}[G]\) by the map defined in 23.

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\).

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\).

If \(V\) is reflexive, the map \(((x_1,y_1),(x_2,y_2))\mapsto y_1(x_2)-y_2(x_1)\) is a bilinear form on \(V\times V^*\).

We define a bilinear form on \(V^{**}\times V\) by \((x,y)\mapsto - y(x)\).

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\).

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.

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.

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]\).

We define the set \(\Omega _g\) to be the image of \(\mathbb {K}[\mathcal{Z}_G]\) by \(\Gamma _G\).

The map \(\Gamma _g\) defines a \(k\)-linear bijection between \(\Omega _g\) and \(\mathbb {K}[\mathcal{Z}_G]\).

The bijection defined in 41 is indeed a \(\mathbb {K}[\mathcal{Z}_G]\)-linear map.

The multiplication defined in 42 induced an action of \(\mathbb {K}[\mathcal{Z}_G]\) on \(\Omega _g\).

We define a multiplication between \(x\in \mathbb {K}[\mathcal{Z}_G]\) and \(y\in \Omega _g\) by \(x\times y\).

Given \(k\) a field, \(V\) a \(k\) vector space and \(V^*\) its dual vector space, we define the Heisenberg set associated to \(V\) by \(\mathcal{H}(V):=\{ (z,x,y) \in k\times V\times V^*\} \).

We define the multiplciation of elements \(g\in G\) and \(kG\in \mathbb {K}[G]\) in \(\mathbb {K}[G]\) by \(g\times kG\).

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}\)

If \(V\) is reflexive, then the linear map defined in 76 is a bijective linear map from \(V\) to \(V^{**}\).

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 :

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 \).

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 \).

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 \).

The inverse of \((z,x,y)\in \mathcal{H}(V)\) is given by the formula \((-z- y(-x), - x ,- y)\).

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)\).

The map \(\psi :(z,x,y)\mapsto (x,y)\) defines a homomorphism from \(\mathcal{H}(V)\) to \(V\times V^*\).

The map \(\varphi :z\mapsto (z,0,0)\) defines a homomorphism from \((k,+)\) to \(\mathcal{H}(V)\).

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]\).

The map defined in 49 is in fact an isomorphism.

We construct a \(\mathbb {K}[\mathcal{Z}_G]\)-linear map on \(\bigoplus \limits _{g\in \mathcal{S}_{G/\mathcal{Z}_G}}\mathbb {K}[\mathcal{Z}_G]\) by using the images of the element of the basis 47 by the map 48.

We have an isomorphism \(\mathbb {K}[G]\cong \bigoplus \limits _{g\in \mathcal{S}_{G/\mathcal{Z}_G}}g\mathbb {K}[\mathcal{Z}_G]\) which is \(\mathbb {K}[\mathcal{Z}_G]\)-linear.

We define an internal law on Heisenberg by the following formula : \((z_1,x_1,y_1)*(z_2,x_2,y_2) = (z_1+z_2+y_1(x_2),x_1+x_2,y_1+y_2)\) for every \((z_1,x_1,y_1),(z_2,x_2,y_2)\in \mathcal{H}(V)\).

The bilinear form defined in 78 is a nondegeneracy bilinear form.

The pullback of \(\{ 0\} \times V^*\) by \(\psi \) defines a subgroup of \(\mathcal{H}(V)\).

The pullback \(V\times \{ 0\} \) by \(\psi \) defines a subgroup of \(\mathcal{H}(V)\).

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.

We define a multiplication between elements of \(\mathbb {K}[H]\) and elements of \(\mathbb {K}[G]\) by \(kH*kG=\varphi _{kHkG}(kH)\times kG\).

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\).

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 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))\).

The bijection 16 empacked as Sigma type instead of cartesian product. Useful for \(LEAN\).

We define a linear map from \(V\) to \(V^{**}\) by \(v\mapsto (\varphi \mapsto -\varphi (v))\).

We have a short exact sequence \(0\rightarrow k \stackrel{\varphi }{\rightarrow } \mathcal{H}(V) \stackrel{\psi }{\rightarrow } V\times V^* \rightarrow 0\).

Under our identification of the bidual, the map define in 85 is a group antiisomorphism from \(\mathcal{H}(V)\) to \(\mathcal{H}(V^*)\).

\(\mathcal{H}(V)\) is in bijection with \(k\times V\times V^*\).

Let \(x\in \mathbb {K}[\mathcal{Z}_G]\) and \(g\in G\). Then \(g\times x = x \times g\).

The set define in 87 is indeed the center of \(\mathcal{H}(V)\).

The center of Heisenberg \(\mathcal{Z}_{\mathcal{H}(V)}\) is a subgroup of \(\mathcal{H}(V)\).

If \(h\) is an element of the center of \(G\), it commutes with every element of \(G\).

Let \(h\in \mathcal{Z}_G\) such that \(h=ab\) for some \((a,b)\in G^2\). Then, we also have \(h=ba\).

The image of the map sending 33 and 65 to their tensor product defines a \(\mathbb {K}[\mathcal{Z}_G]\)-submodule of \(\mathbb {K}[G]\otimes _{\mathbb {k}[\mathcal{Z}_G]}V_\theta \).

If \(h:=(z,x,y)\) belongs to the commutator subgroup, then \(x=0\) and \(y=0\).

If \(V\) isn’t trivial, the subgroup of \(\mathcal{H}(V)\) generates by commutators isn’t trivial too.

Let \(H_1:=(z_1,x_1,y_1)\) and \(H_2:=(z_2,x_2,y_2)\) be two elements of \(\mathcal{H}(V)\). The commutator of \([H_1,H_2]\) is \((y_1(x_2)-y_2(x_1),0,0)\).

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\).

For every \(g\in G\) and \(h\in \mathbb {Z}_G\), we have \(\varphi _{G\mathcal{S}}(gh)=\varphi _{G\mathcal{S}} (g)\).

For all \(x\in \mathbb {K}[\mathcal{Z}[G]]\), we have \(\Gamma _g(x)=g\times x\)

The map \(\Gamma _g\) defined in 37 is injective.

The action defined in 43 is indeed distributive.

\(\Omega _g\) is a \(\mathbb {K}[\mathcal{Z}_G]\) module for the action defined in 43.

Heisenberg is a group for the the internal law defined in 82.

If \(k\) is a finite field, then \(|\mathcal{H}(V)|=|k|\times |V|^2\).

If \(k\) is a finite field, then \(|\mathcal{Z}_{\mathcal{H}(V)}|=|k|\).

Elements of \(G\) are distributive over \(\mathbb {K}[\mathcal{Z}_G]\)

The \(V\) defined in 52 is an additive commutative monoid.

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 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 \).

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 \).

The induced representation defined in 56 is a \(\mathbb {K}[\mathcal{Z}_G]\) module.

The homomorphism defined in 94 is injective.

\(\mathbb {K}[G]\) is a \(\mathbb {K}[\mathcal{Z}_G]\) algebra.

If there exists a morphism from \(H\) to \(\mathcal{Z}_G\), then \(\mathbb {K}[G]\) is a \(\mathbb {K}[H]\) algebra.

The map defined in 23 is injective.

The map defined in 23 is \(k\) linear.

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]\).

We have an isomorphism between \(\mathbb {K}[\mathcal{Z}_G]\otimes _{\mathbb {K}[\mathcal{Z}_G]}V_\theta \) and \(V_\theta \).

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.

The subgroup defined in 103 is commutative.

The subgroup defined in 103 is maximal among the commutative subgroups of \(\mathcal{H}(V)\).

The subgroup defined in 103 is ai normal subgroup of Heisenberg. .

The subgroup defined in 99 is commutative.

The subgroup defined in 99 is maximal among the commutative subgroups of \(\mathcal{H}(V)\).

The subgroup defined in 99 is a normal subgroup of Heisenberg.

The tensor product defined in 57 is an additive commutative monoid.

The tensor product defined in 57 is a \(\mathbb {K}[\mathcal{Z}_G]\) module.

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.

The homomorphism defined in 96 is surjective.

For every \(g\in G\) the following identity holds : \(\psi _{G\mathcal{Z}_G}(g)=g\varphi _{G\mathcal{S}}(g)^{-1}\).

For every \(g\in G\) the following identity holds : \(g=\varphi _{G\mathcal{S}}(g) \psi _{G\mathcal{Z}_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)\).

For every \(g\in \mathcal{S}_{G/\mathcal{Z}_G}\), we have \(\psi _{G\mathcal{Z}_G}(g)=e_G\).

For every \(g\in \mathcal{S}_{G/\mathcal{Z}_G}\), we have \(\varphi _{G\mathcal{S}}(g)=g\).

We have \(G = \{ gh,\ g\in \mathcal{S}_{G/\mathcal{Z}_G},\ h\in \mathcal{Z}_G\} \).

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.

If \(G\) is finite, then the system of representatives of \(G/\mathcal{Z}_G\) is finite too.

We have \(\bigcup \limits _{s\in \mathcal{S}_{G/\mathcal{Z}_G}} C_s= G\).

The \(V\) defined in 52 is a \(\mathbb {K}[G]\) module.

The \(V\) defined in 52 is a \(\mathbb {K}[\mathcal{Z}_G]\) module.

If \(|G|\nmid Char(k)\), then the module defined in 52 is semisimple.

The set of elements of \(V_\theta \) defines a \(\mathbb {K}[\mathcal{Z}_G]\)-submodule of itself.

The submodule defined in 64 is isomorphic to \(V_\theta \).

If \(k\) is a finite field, then \([\mathcal{H}(V):\mathcal{Z}_{\mathcal{H}(V)}]=|V|^2\).

If \(V\) isn’t trivial, \(\mathcal{H}(V)\) is a two step nilpotent group.