HeisenbergCardinality.lean

1 import PaperXI.HeisenbergForm
2 import PaperXI.HeisenbergGeometry
3 import Mathlib.LinearAlgebra.Dual.Lemmas
4 
5 /-! Dimension and cardinality of a maximal isotropic subspace in the standard
6 Heisenberg symplectic space. No cardinality or self-orthogonality conclusion is
7 assumed as an input. -/
8 
9 set_option autoImplicit false
10 
11 namespace PaperXI.HeisenbergCardinality
12 
13 open Module PaperXI.HeisenbergForm PaperXI.HeisenbergGeometry
14 
15 variable {K X : Type*} [Field K] [AddCommGroup X] [Module K X]
16 
17 theorem form_isAlt : LinearMap.BilinForm.IsAlt (form (K := K) (X := X)) := form_self
18 
19 theorem form_separatingLeft : (form (K := K) (X := X)).SeparatingLeft := by
20   intro v hv
21   apply Prod.ext
22   · apply (Module.forall_dual_apply_eq_zero_iff K v.1).mp
23     intro φ
24     simpa using hv (0, φ)
25   · apply LinearMap.ext
26     intro x
27     simpa using hv (x, 0)
28 
29 theorem form_nondegenerate : (form (K := K) (X := X)).Nondegenerate := by
30   refine ⟨form_separatingLeft, ?_⟩
31   intro v hv
32   apply form_separatingLeft v
33   intro w
34   exact form_isAlt.isRefl _ _ (hv w)
35 
36 /-- Pairing with every vector vanishes precisely at zero. -/
37 theorem form_forall_eq_zero_iff (v : X × Module.Dual K X) :
38     (∀ w, form v w = 0) ↔ v = 0 := by
39   exact ⟨form_separatingLeft v, fun h => by simp [h]⟩
40 
41 theorem maximal_orthogonal_eq (L : Submodule K (X × Module.Dual K X))
42     (hL : IsMaximalIsotropic form L) :
43     LinearMap.BilinForm.orthogonal form L = L :=
44   orthogonal_eq (form (K := K) (X := X)) form_isAlt L hL
45 
46 variable [FiniteDimensional K X]
47 
48 theorem finrank_eq (L : Submodule K (X × Module.Dual K X))
49     (hL : IsMaximalIsotropic form L) : finrank K L = finrank K X := by
50   have h := two_mul_finrank (form (K := K) (X := X)) form_isAlt form_nondegenerate L hL
51   rw [Module.finrank_prod, Subspace.dual_finrank_eq] at h
52   omega
53 
54 theorem natCard_eq_pow (L : Submodule K (X × Module.Dual K X))
55     (hL : IsMaximalIsotropic form L) :
56     Nat.card L = Nat.card K ^ finrank K X := by
57   rw [Module.natCard_eq_pow_finrank (K := K) (V := L), finrank_eq L hL]
58 
59 theorem natCard_eq (L : Submodule K (X × Module.Dual K X))
60     (hL : IsMaximalIsotropic form L) : Nat.card L = Nat.card X := by
61   calc
62     Nat.card L = Nat.card K ^ finrank K X := natCard_eq_pow L hL
63     _ = Nat.card X := (Module.natCard_eq_pow_finrank (K := K) (V := X)).symm
64 
65 end PaperXI.HeisenbergCardinality

Back to source controls