BreakHeisenbergSum.lean

1 import PaperXI.AbstractHeisenberg
2 import PaperXI.CentralProduct
3 import Mathlib.Algebra.BigOperators.GroupWithZero.Finset
4 import Mathlib.Tactic
5 
6 /-! Actual half-form Heisenberg groups of a finite orthogonal sum are the
7 balanced central product of the summand groups. The retained center handles
8 an empty family. The group isomorphism is constructed, not assumed. -/
9 set_option autoImplicit false
10 set_option backward.isDefEq.respectTransparency false
11 noncomputable section
12 namespace PaperXI.BreakHeisenbergSum
13 open AbstractHeisenberg
14 
15 variable {S K : Type*} [Fintype S] [Field K]
16 variable {V : S → Type*} [∀ s, AddCommGroup (V s)] [∀ s, Module K (V s)]
17 
18 /-- The actual bilinear form on the dependent finite product. -/
19 def form (b : ∀ s, LinearMap.BilinForm K (V s)) : LinearMap.BilinForm K (∀ s, V s) where
20   toFun v := {
21     toFun := fun w => ∑ s, b s (v s) (w s)
22     map_add' := by intros; simp [map_add, Finset.sum_add_distrib]
23     map_smul' := by intros; simp [Finset.mul_sum] }
24   map_add' := by intros; ext; simp [map_add, Finset.sum_add_distrib]
25   map_smul' := by intros; ext; simp [Finset.mul_sum]
26 
27 @[simp] theorem form_apply (b : ∀ s, LinearMap.BilinForm K (V s)) (v w : ∀ s, V s) :
28     form b v w = ∑ s, b s (v s) (w s) := rfl
29 
30 theorem form_isAlt (b : ∀ s, LinearMap.BilinForm K (V s)) (hb : ∀ s, (b s).IsAlt) :
31     (form b).IsAlt := by
32   intro v
33   simp [form_apply, fun s => hb s (v s)]
34 
35 /-- The actual ambient product maps to the half-form group by summing central coordinates. -/
36 def fromProduct (b : ∀ s, LinearMap.BilinForm K (V s)) :
37     CentralProduct.Ambient (Z := Multiplicative K) (H := fun s => Element (b s)) →*
38       Element (form b) where
39   toFun x := ⟨fun s => (x.2 s).vector, x.1.toAdd + ∑ s, (x.2 s).central⟩
40   map_one' := by ext <;> simp
41   map_mul' x y := by
42     ext
43     · rfl
44     · simp only [mul_central, form_apply, Prod.fst_mul, Prod.snd_mul,
45         toAdd_mul, Pi.mul_apply]
46       simp only [Finset.sum_add_distrib, Finset.mul_sum]
47       ring
48 
49 @[simp] theorem fromProduct_vector (b : ∀ s, LinearMap.BilinForm K (V s))
50     (x : CentralProduct.Ambient (Z := Multiplicative K) (H := fun s => Element (b s))) (s : S) :
51     (fromProduct b x).vector s = (x.2 s).vector := rfl
52 
53 @[simp] theorem fromProduct_central (b : ∀ s, LinearMap.BilinForm K (V s))
54     (x : CentralProduct.Ambient (Z := Multiplicative K) (H := fun s => Element (b s))) :
55     (fromProduct b x).central = x.1.toAdd + ∑ s, (x.2 s).central := rfl
56 
57 /-- A total group element has the literal coordinate-wise preimage with central sum correction. -/
58 theorem fromProduct_surjective (b : ∀ s, LinearMap.BilinForm K (V s)) :
59     Function.Surjective (fromProduct b) := by
60   intro h
61   refine ⟨(Multiplicative.ofAdd h.central, fun s => ⟨h.vector s, 0⟩), ?_⟩
62   ext <;> simp
63 
64 /-- The actual balancing relation is killed by the orthogonal-sum map. -/
65 theorem fromProduct_balanced (b : ∀ s, LinearMap.BilinForm K (V s)) (w : S → Multiplicative K) :
66     fromProduct b (CentralProduct.balanced (fun s => datum (b s)) w) = 1 := by
67   ext
68   · rfl
69   · simp [fromProduct, CentralProduct.balanced]
70 
71 /-- The induced map from the actual central quotient. -/
72 def sumMap (b : ∀ s, LinearMap.BilinForm K (V s)) :
73     CentralProduct.Group (fun s => datum (b s)) →* Element (form b) :=
74   CentralProduct.descend _ (fromProduct b) (fromProduct_balanced b)
75 
76 @[simp] theorem sumMap_mk (b : ∀ s, LinearMap.BilinForm K (V s))
77     (x : CentralProduct.Ambient (Z := Multiplicative K) (H := fun s => Element (b s))) :
78     sumMap b (CentralProduct.mk _ x) = fromProduct b x := rfl
79 
80 @[simp] theorem sumMap_center (b : ∀ s, LinearMap.BilinForm K (V s)) (z : Multiplicative K) :
81     sumMap b (CentralProduct.center _ z) = (datum (form b)).i z := by
82   ext <;> simp [CentralProduct.center_apply]
83 
84 theorem sumMap_surjective (b : ∀ s, LinearMap.BilinForm K (V s)) :
85     Function.Surjective (sumMap b) := by
86   intro h
87   obtain ⟨x, rfl⟩ := fromProduct_surjective b h
88   exact ⟨CentralProduct.mk _ x, rfl⟩
89 
90 /-- Vanishing of the actual image forces the representative to be a balanced central tuple. -/
91 theorem sumMap_injective (b : ∀ s, LinearMap.BilinForm K (V s)) :
92     Function.Injective (sumMap b) := by
93   apply (MonoidHom.ker_eq_bot_iff _).mp
94   apply le_antisymm
95   · intro x hx
96     change x = 1
97     obtain ⟨⟨z, h⟩, rfl⟩ := CentralProduct.mk_surjective (fun s => datum (b s)) x
98     have hv : ∀ s, (h s).vector = 0 := by
99       intro s
100       exact congrArg (fun x : Element (form b) => x.vector s) hx
101     have hz : z.toAdd + ∑ s, (h s).central = 0 :=
102       congrArg (fun x : Element (form b) => x.central) hx
103     have hh : h = fun s => (datum (b s)).i (Multiplicative.ofAdd (h s).central) := by
104       funext s
105       ext
106       · exact hv s
107       · rfl
108     rw [hh, CentralProduct.mk_centers]
109     have hw : z * ∏ s, Multiplicative.ofAdd (h s).central = 1 := by
110       apply Multiplicative.toAdd.injective
111       simpa using hz
112     rw [hw, map_one]
113   · exact bot_le
114 
115 /-- The central product is the actual Heisenberg group of the orthogonal finite product. -/
116 def sumEquiv (b : ∀ s, LinearMap.BilinForm K (V s)) :
117     CentralProduct.Group (fun s => datum (b s)) ≃* Element (form b) :=
118   MulEquiv.ofBijective (sumMap b) ⟨sumMap_injective b, sumMap_surjective b⟩
119 
120 @[simp] theorem sumEquiv_mk (b : ∀ s, LinearMap.BilinForm K (V s))
121     (x : CentralProduct.Ambient (Z := Multiplicative K) (H := fun s => Element (b s))) :
122     sumEquiv b (CentralProduct.mk _ x) = fromProduct b x := rfl
123 
124 @[simp] theorem sumEquiv_center (b : ∀ s, LinearMap.BilinForm K (V s)) (z : Multiplicative K) :
125     sumEquiv b (CentralProduct.center _ z) = (datum (form b)).i z := sumMap_center b z
126 
127 variable {T : Type*} [AddCommGroup T] [Module K T]
128 
129 /-- Transfer through the actual supplied form-preserving break decomposition. -/
130 def decompositionEquiv (b : ∀ s, LinearMap.BilinForm K (V s))
131     (c : LinearMap.BilinForm K T) (e : (∀ s, V s) ≃ₗ[K] T)
132     (he : ∀ v w, c (e v) (e w) = form b v w) :
133     CentralProduct.Group (fun s => datum (b s)) ≃* Element c :=
134   (sumEquiv b).trans (AbstractHeisenberg.lift (form b) c e he)
135 
136 @[simp] theorem decompositionEquiv_center (b : ∀ s, LinearMap.BilinForm K (V s))
137     (c : LinearMap.BilinForm K T) (e : (∀ s, V s) ≃ₗ[K] T)
138     (he : ∀ v w, c (e v) (e w) = form b v w) (z : Multiplicative K) :
139     decompositionEquiv b c e he (CentralProduct.center _ z) = (datum c).i z := by
140   exact (congrArg (AbstractHeisenberg.lift (form b) c e he) (sumEquiv_center b z)).trans
141     (AbstractHeisenberg.lift_inclusion (form b) c e he z)
142 
143 end PaperXI.BreakHeisenbergSum

Back to source controls