The topology of the Heisenberg group

For a topological ring R, the Heisenberg group HeisenbergGroup R of triples (x, y, z) with (x, y, z) * (x', y', z') = (x + x', y + y', z + z' + x * y') carries the product topology of R × R × R, transported along the coordinate equivalence HeisenbergGroup.equivProd. The group law and the inversion are polynomial in the coordinates, so this makes the Heisenberg group a topological group. Compactness, Hausdorffness and total disconnectedness pass from R to the Heisenberg group through the coordinate homeomorphism.

Over the p-adic integers this is a compact, totally disconnected group of nilpotency class two; it is pro-p by TauCeti.HeisenbergGroup.isProP_padicInt, and it detects the commutators of two generators of a free pro-p group. What makes the detection work is that, over any Hausdorff topological ring, the closed lower central series of the Heisenberg group stops at γ_2 = 1.

Main definitions

• TauCeti.HeisenbergGroup.instTopologicalSpace: the topology induced from R × R × R.
• TauCeti.HeisenbergGroup.homeomorphProd: the coordinate equivalence as a homeomorphism HeisenbergGroup R ≃ₜ R × R × R.

Main results

• TauCeti.HeisenbergGroup.continuous_x, continuous_y, continuous_z: the coordinates are continuous.
• TauCeti.HeisenbergGroup.continuous_iff: a map into the Heisenberg group is continuous exactly when its three coordinates are.
• The instances IsTopologicalGroup, CompactSpace, T2Space, DiscreteTopology and TotallyDisconnectedSpace on HeisenbergGroup R, inherited from R.
• TauCeti.HeisenbergGroup.isClosed_zAxis: over a Hausdorff ring the z-axis is closed.
• TauCeti.HeisenbergGroup.closedLowerCentralSeries_one_le_zAxis, TauCeti.HeisenbergGroup.closedLowerCentralSeries_two_eq_bot: over a Hausdorff topological ring, γ_1 of the closed lower central series lies in the z-axis and γ_2 is trivial.

@[instance_reducible]

instance TauCeti.HeisenbergGroup.instTopologicalSpace {R : Type u_1} [TopologicalSpace R] : TopologicalSpace (HeisenbergGroup R)

The topology on the Heisenberg group over a topological space R: the product topology of R × R × R, pulled back along the coordinate equivalence.

Equations

• TauCeti.HeisenbergGroup.instTopologicalSpace = TauCeti.HeisenbergGroup.equivProd.topologicalSpace

def TauCeti.HeisenbergGroup.homeomorphProd {R : Type u_1} [TopologicalSpace R] : HeisenbergGroup R ≃ₜ R × R × R

The coordinate equivalence HeisenbergGroup R ≃ R × R × R is a homeomorphism.

Equations

• TauCeti.HeisenbergGroup.homeomorphProd = TauCeti.HeisenbergGroup.equivProd.homeomorph

@[simp]

theorem TauCeti.HeisenbergGroup.homeomorphProd_apply {R : Type u_1} [TopologicalSpace R] (a : HeisenbergGroup R) : homeomorphProd a = (a.x, a.y, a.z)

@[simp]

theorem TauCeti.HeisenbergGroup.homeomorphProd_symm_apply {R : Type u_1} [TopologicalSpace R] (a : R × R × R) : homeomorphProd.symm a = { x := a.1, y := a.2.1, z := a.2.2 }

theorem TauCeti.HeisenbergGroup.continuous_x {R : Type u_1} [TopologicalSpace R] : Continuous x

The x coordinate is continuous for the transported product topology.

theorem TauCeti.HeisenbergGroup.continuous_y {R : Type u_1} [TopologicalSpace R] : Continuous y

The y coordinate is continuous for the transported product topology.

theorem TauCeti.HeisenbergGroup.continuous_z {R : Type u_1} [TopologicalSpace R] : Continuous z

The z coordinate is continuous for the transported product topology.

theorem TauCeti.HeisenbergGroup.continuous_iff {R : Type u_1} [TopologicalSpace R] {X : Type u_2} [TopologicalSpace X] {f : X → HeisenbergGroup R} : Continuous f ↔ (Continuous fun (a : X) => (f a).x) ∧ (Continuous fun (a : X) => (f a).y) ∧ Continuous fun (a : X) => (f a).z

A map into the Heisenberg group is continuous exactly when its three coordinates are.

instance TauCeti.HeisenbergGroup.instCompactSpace {R : Type u_1} [TopologicalSpace R] [CompactSpace R] : CompactSpace (HeisenbergGroup R)

instance TauCeti.HeisenbergGroup.instT2Space {R : Type u_1} [TopologicalSpace R] [T2Space R] : T2Space (HeisenbergGroup R)

instance TauCeti.HeisenbergGroup.instDiscreteTopology {R : Type u_1} [TopologicalSpace R] [DiscreteTopology R] : DiscreteTopology (HeisenbergGroup R)

instance TauCeti.HeisenbergGroup.instTotallyDisconnectedSpace {R : Type u_1} [TopologicalSpace R] [TotallyDisconnectedSpace R] : TotallyDisconnectedSpace (HeisenbergGroup R)

instance TauCeti.HeisenbergGroup.instIsTopologicalGroupOfIsTopologicalRing {R : Type u_1} [TopologicalSpace R] [Ring R] [IsTopologicalRing R] : IsTopologicalGroup (HeisenbergGroup R)

Over a topological ring the Heisenberg group is a topological group: its multiplication and inversion are polynomial in the coordinates.

theorem TauCeti.HeisenbergGroup.isClosed_zAxis {R : Type u_1} [TopologicalSpace R] [Ring R] [T2Space R] : IsClosed ↑zAxis

The z-axis of the Heisenberg group over a ring with a Hausdorff topology is closed.

theorem TauCeti.HeisenbergGroup.closedLowerCentralSeries_one_le_zAxis {R : Type u_1} [TopologicalSpace R] [Ring R] [IsTopologicalRing R] [T2Space R] : closedLowerCentralSeries (HeisenbergGroup R) 1 ≤ zAxis

The first term γ_1 of the closed lower central series of the Heisenberg group over a Hausdorff topological ring lies in the z-axis.

theorem TauCeti.HeisenbergGroup.closedLowerCentralSeries_two_eq_bot {R : Type u_1} [TopologicalSpace R] [Ring R] [IsTopologicalRing R] [T2Space R] : closedLowerCentralSeries (HeisenbergGroup R) 2 = ⊥

The closed lower central series of the Heisenberg group over a Hausdorff topological ring stops at γ_2 = 1.