HeisenbergGeometry.lean

1 import Mathlib.LinearAlgebra.BilinearForm.Orthogonal
2 import Mathlib.FieldTheory.Finiteness
3 import Mathlib.Tactic
4 
5 /-!
6 # Maximal isotropic subspaces
7 
8 Maximality is by inclusion among subspaces on which the alternating form vanishes.
9 The equality with the orthogonal complement is derived from that hypothesis.
10 -/
11 
12 set_option autoImplicit false
13 
14 namespace PaperXI.HeisenbergGeometry
15 
16 open Module
17 
18 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
19 
20 /-- A subspace on which the form vanishes identically. -/
21 def IsIsotropic (B : LinearMap.BilinForm K V) (L : Submodule K V) : Prop :=
22   ∀ u ∈ L, ∀ v ∈ L, B u v = 0
23 
24 /-- Maximality among isotropic subspaces, ordered by inclusion. -/
25 def IsMaximalIsotropic (B : LinearMap.BilinForm K V) (L : Submodule K V) : Prop :=
26   IsIsotropic B L ∧ ∀ M : Submodule K V, IsIsotropic B M → L ≤ M → M = L
27 
28 theorem isotropic_iff_le_orthogonal (B : LinearMap.BilinForm K V)
29     (L : Submodule K V) : IsIsotropic B L ↔ L ≤ B.orthogonal L := by
30   constructor
31   · intro h v hv u hu
32     exact h u hu v hv
33   · intro h u hu v hv
34     exact h hv u hu
35 
36 /-- Adjoining an orthogonal vector preserves isotropy for an alternating form. -/
37 theorem isotropic_sup_span (B : LinearMap.BilinForm K V) (hB : B.IsAlt)
38     (L : Submodule K V) (hL : IsIsotropic B L) (x : V)
39     (hx : x ∈ B.orthogonal L) : IsIsotropic B (L ⊔ K ∙ x) := by
40   intro u hu v hv
41   obtain ⟨l, hl, z, hz, rfl⟩ := Submodule.mem_sup.mp hu
42   obtain ⟨a, rfl⟩ := Submodule.mem_span_singleton.mp hz
43   obtain ⟨m, hm, w, hw, rfl⟩ := Submodule.mem_sup.mp hv
44   obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.mp hw
45   have hxl : B x m = 0 := hB.isRefl _ _ (hx m hm)
46   simp [map_add, map_smul, LinearMap.add_apply, LinearMap.smul_apply,
47     hL l hl m hm, hx l hl, hxl, hB x]
48 
49 /-- Maximality supplies the reverse inclusion in the orthogonal complement. -/
50 theorem orthogonal_eq (B : LinearMap.BilinForm K V) (hB : B.IsAlt)
51     (L : Submodule K V) (hL : IsMaximalIsotropic B L) : B.orthogonal L = L := by
52   apply le_antisymm
53   · intro x hx
54     have hsup := hL.2 (L ⊔ K ∙ x) (isotropic_sup_span B hB L hL.1 x hx) le_sup_left
55     rw [← hsup]
56     exact (show K ∙ x ≤ L ⊔ K ∙ x from le_sup_right)
57       (Submodule.mem_span_singleton_self x)
58   · exact (isotropic_iff_le_orthogonal B L).mp hL.1
59 
60 theorem maximal_iff_orthogonal_eq (B : LinearMap.BilinForm K V) (hB : B.IsAlt)
61     (L : Submodule K V) : IsMaximalIsotropic B L ↔ B.orthogonal L = L := by
62   refine ⟨orthogonal_eq B hB L, fun h => ?_⟩
63   refine ⟨(isotropic_iff_le_orthogonal B L).mpr h.ge, ?_⟩
64   intro M hM hLM
65   apply le_antisymm _ hLM
66   calc
67     M ≤ B.orthogonal M := (isotropic_iff_le_orthogonal B M).mp hM
68     _ ≤ B.orthogonal L := LinearMap.BilinForm.orthogonal_le hLM
69     _ = L := h
70 
71 /-- Every maximal isotropic subspace has half the dimension of a nondegenerate space. -/
72 theorem two_mul_finrank [FiniteDimensional K V]
73     (B : LinearMap.BilinForm K V) (hB : B.IsAlt) (hnd : B.Nondegenerate)
74     (L : Submodule K V) (hL : IsMaximalIsotropic B L) :
75     2 * finrank K L = finrank K V := by
76   have h := LinearMap.BilinForm.finrank_add_finrank_orthogonal hB.isRefl L
77   rw [orthogonal_eq B hB L hL,
78     LinearMap.BilinForm.orthogonal_top_eq_bot hnd, inf_bot_eq,
79     finrank_bot, add_zero] at h
80   omega
81 
82 end PaperXI.HeisenbergGeometry

Back to source controls