Heisenberg's groups over a vector space

This file defines Heisenberg's groups over a vector space and their basic properties.

Mains results

Let kbe a field, V a finite dimensional vector space over k, and Module.Dual k V its dual space. We also take the convention that Vis in bijection with Module.Dual k (Module.Dual k V) by $(x,y)=-(y,x)$. We define the group of Heisenberg, some subgroups, and basic properties of these groups. The main results are :

• Heisenberg.two_step_nilpotent : the Heisenberg group is a two-step nilpotent group.
• Heisenberg.anti_iso_Dual: the Heisenberg group is anti-isomorphic to the Heisenberg group of its dual.

structure Heisenberg (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : Type (max u_1 u_2)

• z : k
• x : V
• y : Module.Dual k V

theorem Heisenberg.ext {V : Type u_1} {k : Type u_2} {inst1 : Field k} {inst2 : AddCommGroup V} {inst3 : Module k V} {x y : Heisenberg V k} (z : x.z = y.z) : x.x = y.x → x.y = y.y → x = y

theorem Heisenberg.ext_iff {V : Type u_1} {k : Type u_2} {inst1 : Field k} {inst2 : AddCommGroup V} {inst3 : Module k V} {x y : Heisenberg V k} : x = y ↔ x.z = y.z ∧ x.x = y.x ∧ x.y = y.y

def Heisenberg.mul {V : Type u_1} {k : Type u_2} [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] (H1 H2 : Heisenberg V k) : Heisenberg V k

Intern law over Heisenberg

Equations

• H1.mul H2 = { z := H1.z + H2.z + H1.y H2.x, x := H1.x + H2.x, y := H1.y + H2.y }

def Heisenberg.inverse {V : Type u_1} {k : Type u_2} [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] (H : Heisenberg V k) : Heisenberg V k

Inverse of an element of Heisenberg by mul

Equations

• H.inverse = { z := -H.z - H.y (-H.x), x := -H.x, y := -H.y }

instance Heisenberg.group {V : Type u_1} {k : Type u_2} [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : Group (Heisenberg V k)

Together with Heisenberg.mul and Heisenberg.inverse, Heisenbergforms a group.

Equations

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

def Heisenberg.center (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : Set (Heisenberg V k)

Center of Heisenberg

Equations

• Heisenberg.center V k = {H : Heisenberg V k | H.x = 0 ∧ H.y = 0}

def Heisenberg.Hom_k_to_H (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : k →+ Additive (Heisenberg V k)

The map $(z,x,y) ↦ (z,0,0)$ defines a homorphism from Heisenberg to its center Heisenberg.center.

Equations

• Heisenberg.Hom_k_to_H V k = AddMonoidHom.mk' (fun (z : k) => { z := z, x := 0, y := 0 }) ⋯

def Heisenberg.Hom_H_to_V_x_Dual (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : Additive (Heisenberg V k) →+ V × Module.Dual k V

The map $(z,x,y)↦(x,y)$ defines a homomorphism from Heisenberg to $V × V^*$.

Equations

• Heisenberg.Hom_H_to_V_x_Dual V k = AddMonoidHom.mk' (fun (H : Additive (Heisenberg V k)) => (H.x, H.y)) ⋯

def Heisenberg.exact_sequence (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : Function.Exact ⇑(Hom_k_to_H V k) ⇑(Hom_H_to_V_x_Dual V k)

We have an exact sequence $0 → k → H(V) → V × V^* → 0$ given by Heisenberg.Hom_k_to_H and Heisenberg.Hom_H_to_V_x_Dual.

Equations

• ⋯ = ⋯

def Heisenberg.Hom_H_to_V_x_Dual_sub_V (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : Subgroup (Heisenberg V k)

The pull-back of $V$ by Heisenberg.Hom_H_to_V_x_Dualis a subgroup.

Equations

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

instance Heisenberg.Hom_H_to_V_x_Dual_sub_V_commutative (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : IsMulCommutative ↥(Hom_H_to_V_x_Dual_sub_V V k)

The subgroup Heisenberg.Hom_H_to_V_x_Dual_sub_V is commutative.

instance Heisenberg.Hom_H_to_V_x_Dual_sub_V_normal (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : (Hom_H_to_V_x_Dual_sub_V V k).Normal

The subgroup Heisenberg.Hom_H_to_V_x_Dual_sub_V is a normal subgroup.

theorem Heisenberg.Hom_H_to_V_x_Dual_sub_V_maximal (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] (Q : Subgroup (Heisenberg V k)) : IsMulCommutative ↥(Hom_H_to_V_x_Dual_sub_V V k) ∧ (Hom_H_to_V_x_Dual_sub_V V k < Q → ¬IsMulCommutative ↥Q)

The subgroup Heisenberg.Hom_H_to_V_x_Dual_sub_V is maximal among the commutative subgroups of Heisenberg

def Heisenberg.Hom_H_to_V_x_Dual_sub_Dual (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : Subgroup (Heisenberg V k)

The pull-back of $V^*$ by Heisenberg.Hom_H_to_V_x_Dualis a subgroup.

Equations

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

instance Heisenberg.Hom_H_to_V_x_Dual_sub_Dual_commutative (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : IsMulCommutative ↥(Hom_H_to_V_x_Dual_sub_Dual V k)

The subgroup Heisenberg.Hom_H_to_V_x_Dual_sub_Dual is commutative.

instance Heisenberg.Hom_H_to_V_x_Dual_sub_Dual_normal (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : (Hom_H_to_V_x_Dual_sub_Dual V k).Normal

The subgroup Heisenberg.Hom_H_to_V_x_Dual_sub_Dual is a normal subgroup.

@[simp]

theorem Heisenberg.commutator_of_elements {V : Type u_1} {k : Type u_2} [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] (H1 H2 : Heisenberg V k) : ⁅H1, H2⁆ = { z := H1.y H2.x - H2.y H1.x, x := 0, y := 0 }

Commutator of two elements of Heisenberg

theorem Heisenberg.commutator_ne_bot (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] [inst4 : FiniteDimensional k V] [inst5 : Nontrivial V] : lowerCentralSeries (Heisenberg V k) 1 ≠ ⊥

The commutator subgroup of Heisenberg is non trivial

theorem Heisenberg.commutator_caracterisation {V : Type u_1} {k : Type u_2} [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] [inst4 : FiniteDimensional k V] (p : Heisenberg V k) : p ∈ commutator (Heisenberg V k) → p.x = 0 ∧ p.y = 0

Caracterisation of elements in the commutator of Heisenberg

theorem Heisenberg.two_step_nilpotent {V : Type u_1} {k : Type u_2} [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] [inst4 : FiniteDimensional k V] [inst5 : Nontrivial V] : lowerCentralSeries (Heisenberg V k) 1 ≠ ⊥ ∧ lowerCentralSeries (Heisenberg V k) 2 = ⊥

Heisenberg is a twostep nilpotent group

noncomputable def Heisenberg.equiv_Dual (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] [inst4 : FiniteDimensional k V] : Heisenberg V k ≃ Heisenberg (Module.Dual k V) k

$H(V)$ is in bijection with $H(V*)$.

Equations

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

noncomputable def Heisenberg.anti_iso_Dual (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] [inst4 : FiniteDimensional k V] : Heisenberg V k ≃* (Heisenberg (Module.Dual k V) k)ᵐᵒᵖ

With the convention $(x,y)=-(y,x)$, $H(V)$ is antiisomorphic to $H(V*)$.

Equations

• Heisenberg.anti_iso_Dual V k = { toEquiv := (Heisenberg.equiv_Dual V k).trans MulOpposite.opEquiv, map_mul' := ⋯ }

theorem Heisenberg.card_H (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] [inst4 : FiniteDimensional k V] [inst6 : Fintype k] : Nat.card (Heisenberg V k) = Nat.card k * Nat.card V ^ 2

Cardinal of Heisenberg when $k$ is a finite field

theorem Heisenberg.card_center (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] : Nat.card ↑(center V k) = Nat.card k

Cardinal of Heisenberg.center

theorem Heisenberg.ord_V (V : Type u_1) (k : Type u_2) [inst1 : Field k] [inst2 : AddCommGroup V] [inst3 : Module k V] [inst4 : FiniteDimensional k V] [inst6 : Fintype k] : (Subgroup.center (Heisenberg V k)).index = Nat.card V ^ 2

The index of the center of Heisenberg is equal to the cardinal of $V$ to the square.