The Heisenberg group over a ring

The Heisenberg group HeisenbergGroup R over a ring R is the group of unipotent upper triangular 3 × 3 matrices over R, written in the coordinates (x, y, z) of the strictly upper triangle, so that

(x, y, z) * (x', y', z') = (x + x', y + y', z + z' + x * y').

It is nilpotent of class at most two: every commutator lies on the z-axis, which is central, and the commutator of (x, y, z) and (x', y', z') is (0, 0, x * y' - x' * y). Over a ring of characteristic p the p-th power of every element lies on the z-axis as well, so the second term of the lower p-central series is trivial. Over 𝔽_p, for a prime p, the group is nonabelian of order p ^ 3, hence the smallest nonabelian p-group, and has p-class exactly two; it detects brackets in the degree-one graded piece of the lower p-series of a free pro-p group.

Main definitions

• TauCeti.HeisenbergGroup: the Heisenberg group over a ring, with its group structure.
• TauCeti.HeisenbergGroup.zAxis: the central subgroup of elements (0, 0, z).

Main results

• TauCeti.HeisenbergGroup.commutatorElement_eq: the commutator formula.
• TauCeti.HeisenbergGroup.pow_eq: the power formula (x, y, z) ^ n = (n • x, n • y, n • z + (n choose 2) • (x * y)).
• TauCeti.HeisenbergGroup.pLowerCentralSeries_top_two_eq_bot: over a ring of characteristic p, the second term of the lower p-central series is trivial.
• TauCeti.HeisenbergGroup.isPGroup_zmod: over ZMod p the Heisenberg group is a p-group.

structure TauCeti.HeisenbergGroup (R : Type u_1) : Type u_1

The Heisenberg group over a ring R: triples (x, y, z) with the multiplication (x, y, z) * (x', y', z') = (x + x', y + y', z + z' + x * y'), the group of unipotent upper triangular 3 × 3 matrices in the coordinates of the strictly upper triangle.

• x : R

  The (1, 2) matrix entry.

• y : R

  The (2, 3) matrix entry.

• z : R

  The (1, 3) matrix entry.

theorem TauCeti.HeisenbergGroup.ext_iff {R : Type u_1} {x y : HeisenbergGroup R} : x = y ↔ x.x = y.x ∧ x.y = y.y ∧ x.z = y.z

theorem TauCeti.HeisenbergGroup.ext {R : Type u_1} {x y : HeisenbergGroup R} : x.x = y.x → x.y = y.y → ∀ (z : x.z = y.z), x = y

def TauCeti.HeisenbergGroup.equivProd {R : Type u_1} : HeisenbergGroup R ≃ R × R × R

The Heisenberg group is the product R × R × R as a type.

Equations

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

@[simp]

theorem TauCeti.HeisenbergGroup.equivProd_apply {R : Type u_1} (a : HeisenbergGroup R) : equivProd a = (a.x, a.y, a.z)

@[simp]

theorem TauCeti.HeisenbergGroup.equivProd_symm_apply {R : Type u_1} (a : R × R × R) : equivProd.symm a = { x := a.1, y := a.2.1, z := a.2.2 }

@[instance_reducible]

instance TauCeti.HeisenbergGroup.instFintype {R : Type u_1} [Fintype R] : Fintype (HeisenbergGroup R)

Equations

• TauCeti.HeisenbergGroup.instFintype = Fintype.ofEquiv (R × R × R) TauCeti.HeisenbergGroup.equivProd.symm

instance TauCeti.HeisenbergGroup.instFinite {R : Type u_1} [Finite R] : Finite (HeisenbergGroup R)

theorem TauCeti.HeisenbergGroup.card_eq {R : Type u_1} : Nat.card (HeisenbergGroup R) = Nat.card R ^ 3

The Heisenberg group over R has cardinality (Nat.card R) ^ 3; over 𝔽_p its order is p ^ 3.

@[instance_reducible]

instance TauCeti.HeisenbergGroup.instMul {R : Type u_1} [Ring R] : Mul (HeisenbergGroup R)

Equations

• TauCeti.HeisenbergGroup.instMul = { mul := fun (a b : TauCeti.HeisenbergGroup R) => { x := a.x + b.x, y := a.y + b.y, z := a.z + b.z + a.x * b.y } }

@[instance_reducible]

instance TauCeti.HeisenbergGroup.instOne {R : Type u_1} [Ring R] : One (HeisenbergGroup R)

Equations

• TauCeti.HeisenbergGroup.instOne = { one := { x := 0, y := 0, z := 0 } }

@[instance_reducible]

instance TauCeti.HeisenbergGroup.instInv {R : Type u_1} [Ring R] : Inv (HeisenbergGroup R)

Equations

• TauCeti.HeisenbergGroup.instInv = { inv := fun (a : TauCeti.HeisenbergGroup R) => { x := -a.x, y := -a.y, z := -a.z + a.x * a.y } }

@[simp]

theorem TauCeti.HeisenbergGroup.mul_x {R : Type u_1} [Ring R] (a b : HeisenbergGroup R) : (a * b).x = a.x + b.x

@[simp]

theorem TauCeti.HeisenbergGroup.mul_y {R : Type u_1} [Ring R] (a b : HeisenbergGroup R) : (a * b).y = a.y + b.y

@[simp]

theorem TauCeti.HeisenbergGroup.mul_z {R : Type u_1} [Ring R] (a b : HeisenbergGroup R) : (a * b).z = a.z + b.z + a.x * b.y

@[simp]

theorem TauCeti.HeisenbergGroup.one_x {R : Type u_1} [Ring R] : x 1 = 0

@[simp]

theorem TauCeti.HeisenbergGroup.one_y {R : Type u_1} [Ring R] : y 1 = 0

@[simp]

theorem TauCeti.HeisenbergGroup.one_z {R : Type u_1} [Ring R] : z 1 = 0

@[simp]

theorem TauCeti.HeisenbergGroup.inv_x {R : Type u_1} [Ring R] (a : HeisenbergGroup R) : a⁻¹.x = -a.x

@[simp]

theorem TauCeti.HeisenbergGroup.inv_y {R : Type u_1} [Ring R] (a : HeisenbergGroup R) : a⁻¹.y = -a.y

@[simp]

theorem TauCeti.HeisenbergGroup.inv_z {R : Type u_1} [Ring R] (a : HeisenbergGroup R) : a⁻¹.z = -a.z + a.x * a.y

@[instance_reducible]

instance TauCeti.HeisenbergGroup.instGroup {R : Type u_1} [Ring R] : Group (HeisenbergGroup R)

Equations

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

theorem TauCeti.HeisenbergGroup.commutatorElement_eq {R : Type u_1} [Ring R] (a b : HeisenbergGroup R) : ⁅a, b⁆ = { x := 0, y := 0, z := a.x * b.y - b.x * a.y }

The commutator formula: ⁅(x, y, z), (x', y', z')⁆ = (0, 0, x * y' - x' * y).

theorem TauCeti.HeisenbergGroup.pow_eq {R : Type u_1} [Ring R] (a : HeisenbergGroup R) (n : ℕ) : a ^ n = { x := n • a.x, y := n • a.y, z := n • a.z + n.choose 2 • (a.x * a.y) }

The power formula: (x, y, z) ^ n = (n • x, n • y, n • z + (n choose 2) • (x * y)).

def TauCeti.HeisenbergGroup.zAxis {R : Type u_1} [Ring R] : Subgroup (HeisenbergGroup R)

The z-axis {(0, 0, z)}, a central subgroup.

Equations

• TauCeti.HeisenbergGroup.zAxis = { carrier := {a : TauCeti.HeisenbergGroup R | a.x = 0 ∧ a.y = 0}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

@[simp]

theorem TauCeti.HeisenbergGroup.mem_zAxis_iff {R : Type u_1} [Ring R] {a : HeisenbergGroup R} : a ∈ zAxis ↔ a.x = 0 ∧ a.y = 0

theorem TauCeti.HeisenbergGroup.zAxis_le_center {R : Type u_1} [Ring R] : zAxis ≤ Subgroup.center (HeisenbergGroup R)

The z-axis is central.

theorem TauCeti.HeisenbergGroup.commutatorElement_mem_zAxis {R : Type u_1} [Ring R] (a b : HeisenbergGroup R) : ⁅a, b⁆ ∈ zAxis

Every commutator lies on the z-axis: the Heisenberg group is nilpotent of class at most two.

theorem TauCeti.HeisenbergGroup.commutatorElement_eq_one_of_mem_zAxis {R : Type u_1} [Ring R] {a : HeisenbergGroup R} (ha : a ∈ zAxis) (b : HeisenbergGroup R) : ⁅a, b⁆ = 1

The commutator of an element of the z-axis with any element is trivial.

theorem TauCeti.HeisenbergGroup.pow_char_mem_zAxis {R : Type u_1} [Ring R] (p : ℕ) [CharP R p] (a : HeisenbergGroup R) : a ^ p ∈ zAxis

In characteristic p, the p-th power of every element lies on the z-axis.

theorem TauCeti.HeisenbergGroup.pow_char_eq_one_of_mem_zAxis {R : Type u_1} [Ring R] (p : ℕ) [CharP R p] {a : HeisenbergGroup R} (ha : a ∈ zAxis) : a ^ p = 1

In characteristic p, the p-th power of an element of the z-axis is trivial.

theorem TauCeti.HeisenbergGroup.pLowerCentralSeries_top_one_le_zAxis {R : Type u_1} [Ring R] (p : ℕ) [CharP R p] : Subgroup.pLowerCentralSeries p ⊤ 1 ≤ zAxis

In characteristic p, the first term of the lower p-central series lies on the z-axis.

theorem TauCeti.HeisenbergGroup.pLowerCentralSeries_top_two_eq_bot {R : Type u_1} [Ring R] (p : ℕ) [CharP R p] : Subgroup.pLowerCentralSeries p ⊤ 2 = ⊥

The Heisenberg group has p-class at most two in characteristic p: the second term of its lower p-central series is trivial.

theorem TauCeti.HeisenbergGroup.isPGroup_zmod (p : ℕ) : IsPGroup p (HeisenbergGroup (ZMod p))

The Heisenberg group over ZMod p is a p-group; for p > 0 it has order p ^ 3.