HeisenbergFinite.lean

1 import PaperXI.HeisenbergGroup
2 import PaperXI.HeisenbergDimension
3 import Mathlib.RingTheory.Finiteness.Cardinality
4 
5 /-! Finiteness and order of the actual Heisenberg group. -/
6 
7 set_option autoImplicit false
8 
9 namespace PaperXI.HeisenbergFinite
10 
11 open PaperXI.Heisenberg
12 
13 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
14 
15 /-- The underlying coordinate equivalence of the actual group. -/
16 def coordinates : Element K X ≃ (X × Module.Dual K X) × K where
17   toFun a := ((a.position, a.frequency), a.central)
18   invFun a := ⟨a.1.1, a.1.2, a.2⟩
19   left_inv a := by cases a; rfl
20   right_inv a := by rcases a with ⟨⟨x, ξ⟩, z⟩; rfl
21 
22 instance instFinite [Finite K] [FiniteDimensional K X] : Finite (Element K X) := by
23   let : Finite X := Module.finite_of_finite K
24   let : Finite (Module.Dual K X) := Module.finite_of_finite K
25   exact Finite.of_injective coordinates coordinates.injective
26 
27 theorem natCard_eq [FiniteDimensional K X] :
28     Nat.card (Element K X) = (Nat.card X) ^ 2 * Nat.card K := by
29   rw [Nat.card_congr (coordinates (K := K) (X := X)), Nat.card_prod,
30     PaperXI.HeisenbergDimension.natCard_symplectic]
31 
32 end PaperXI.HeisenbergFinite

Back to source controls