TameTensorOrbits.lean

1 import Mathlib.Data.ZMod.Basic
2 import Mathlib.Data.Fintype.EquivFin
3 import Mathlib.Tactic
4 
5 /-! Actual simultaneous-translation orbits used in the tame tensor decomposition. -/
6 set_option autoImplicit false
7 noncomputable section
8 namespace PaperXI.TameTensorOrbits
9 
10 variable (n m : ℕ)
11 
12 /-- The diagonal cyclic subgroup has order `lcm n m`. -/
13 def diagonal : ZMod (Nat.lcm n m) →+* ZMod n × ZMod m :=
14   ZMod.castHom (dvd_refl (Nat.lcm n m)) _
15 
16 theorem diagonal_injective : Function.Injective (diagonal n m) :=
17   ZMod.castHom_injective _
18 
19 @[simp] theorem diagonal_intCast (k : ℤ) :
20     diagonal n m (k : ZMod (Nat.lcm n m)) = ((k : ZMod n), (k : ZMod m)) := by
21   rw [map_intCast]
22   rfl
23 
24 @[simp] theorem diagonal_natCast (k : ℕ) :
25     diagonal n m (k : ZMod (Nat.lcm n m)) = ((k : ZMod n), (k : ZMod m)) := by
26   rw [map_natCast]
27   rfl
28 
29 /-- The difference of the coordinates modulo the gcd. -/
30 def difference (x : ZMod n × ZMod m) : ZMod (Nat.gcd n m) :=
31   ZMod.castHom (Nat.gcd_dvd_right n m) _ x.2 -
32     ZMod.castHom (Nat.gcd_dvd_left n m) _ x.1
33 
34 theorem difference_diagonal (t : ZMod (Nat.lcm n m)) :
35     difference n m (diagonal n m t) = 0 := by
36   obtain ⟨k, rfl⟩ := ZMod.intCast_surjective t
37   simp [difference, diagonal]
38 
39 theorem difference_add (x y : ZMod n × ZMod m) :
40     difference n m (x + y) = difference n m x + difference n m y := by
41   simp only [difference, Prod.fst_add, Prod.snd_add, map_add]
42   abel
43 
44 /-- Orbit coordinates, with representative `(0,i)` and positive simultaneous translation. -/
45 def orbitMap (x : Fin (Nat.gcd n m) × ZMod (Nat.lcm n m)) : ZMod n × ZMod m :=
46   diagonal n m x.2 + (0, (x.1.val : ZMod m))
47 
48 theorem orbitMap_apply (i : Fin (Nat.gcd n m)) (t : ZMod (Nat.lcm n m)) :
49     orbitMap n m (i,t) =
50       ((ZMod.cast t : ZMod n), (ZMod.cast t : ZMod m) + (i.val : ZMod m)) := by
51   ext <;> simp [orbitMap, diagonal]
52 
53 @[simp] theorem orbitMap_zero (i : Fin (Nat.gcd n m)) :
54     orbitMap n m (i,0) = (0, (i.val : ZMod m)) := by
55   simp [orbitMap]
56 
57 @[simp] theorem difference_orbitMap (x : Fin (Nat.gcd n m) × ZMod (Nat.lcm n m)) :
58     difference n m (orbitMap n m x) = (x.1.val : ZMod (Nat.gcd n m)) := by
59   rw [orbitMap, difference_add, difference_diagonal]
60   simp [difference]
61 
62 theorem orbitMap_injective : Function.Injective (orbitMap n m) := by
63   rintro ⟨i,t⟩ ⟨j,u⟩ h
64   have hij := congrArg (difference n m) h
65   simp only [difference_orbitMap] at hij
66   have hij' : i = j := by
67     apply Fin.ext
68     have heq := (ZMod.natCast_eq_natCast_iff' i.val j.val (Nat.gcd n m)).mp hij
69     simpa only [Nat.mod_eq_of_lt i.isLt, Nat.mod_eq_of_lt j.isLt] using heq
70   subst j
71   have htu : t = u := diagonal_injective n m (add_right_cancel h)
72   subst u
73   rfl
74 
75 variable [NeZero n] [NeZero m]
76 
77 instance lcm_neZero : NeZero (Nat.lcm n m) :=
78   ⟨Nat.lcm_ne_zero (NeZero.ne n) (NeZero.ne m)⟩
79 
80 instance gcd_neZero : NeZero (Nat.gcd n m) :=
81   ⟨Nat.ne_of_gt (Nat.gcd_pos_of_pos_left m (Nat.pos_of_ne_zero (NeZero.ne n)))⟩
82 
83 theorem orbitMap_bijective : Function.Bijective (orbitMap n m) := by
84   rw [Fintype.bijective_iff_injective_and_card]
85   refine ⟨orbitMap_injective n m, ?_⟩
86   simp only [Fintype.card_prod, Fintype.card_fin, ZMod.card]
87   exact Nat.gcd_mul_lcm n m
88 
89 /-- Explicit decomposition of the pair-index set into gcd-many lcm-cycles. -/
90 def orbitEquiv : (Fin (Nat.gcd n m) × ZMod (Nat.lcm n m)) ≃ (ZMod n × ZMod m) :=
91   Equiv.ofBijective (orbitMap n m) (orbitMap_bijective n m)
92 
93 @[simp] theorem orbitEquiv_apply (x : Fin (Nat.gcd n m) × ZMod (Nat.lcm n m)) :
94     orbitEquiv n m x = orbitMap n m x := rfl
95 
96 omit [NeZero n] [NeZero m] in
97 theorem orbitMap_translate (i : Fin (Nat.gcd n m)) (t k : ZMod (Nat.lcm n m)) :
98     orbitMap n m (i,t+k) = orbitMap n m (i,t) + diagonal n m k := by
99   simp only [orbitMap, map_add]
100   abel
101 
102 /-- Integer simultaneous translation on the actual pair-index set. -/
103 def translate (k : ℤ) (x : ZMod n × ZMod m) : ZMod n × ZMod m :=
104   x + ((k : ZMod n), (k : ZMod m))
105 
106 omit [NeZero n] [NeZero m] in
107 theorem orbitMap_translate_int (i : Fin (Nat.gcd n m))
108     (t : ZMod (Nat.lcm n m)) (k : ℤ) :
109     orbitMap n m (i,t+k) = translate n m k (orbitMap n m (i,t)) := by
110   rw [orbitMap_translate]
111   rw [diagonal_intCast]
112   rfl
113 
114 omit [NeZero n] [NeZero m] in
115 /-- The stabilizer of every pair is precisely the integer multiples of the lcm. -/
116 theorem translate_eq_iff (k : ℤ) (x : ZMod n × ZMod m) :
117     translate n m k x = x ↔ (Nat.lcm n m : ℤ) ∣ k := by
118   rw [translate, add_eq_left]
119   rw [← diagonal_intCast]
120   rw [map_eq_zero_iff (diagonal n m) (diagonal_injective n m)]
121   exact ZMod.intCast_zmod_eq_zero_iff_dvd k _
122 
123 omit [NeZero n] [NeZero m] in
124 theorem interaction_count : Fintype.card (Fin (Nat.gcd n m)) = Nat.gcd n m :=
125   Fintype.card_fin _
126 
127 theorem interaction_length : Fintype.card (ZMod (Nat.lcm n m)) = Nat.lcm n m :=
128   ZMod.card _
129 
130 omit [NeZero n] [NeZero m] in
131 theorem total_dimension : Nat.gcd n m * Nat.lcm n m = n * m :=
132   Nat.gcd_mul_lcm n m
133 
134 omit [NeZero n] [NeZero m] in
135 theorem difference_translate (k : ℤ) (x : ZMod n × ZMod m) :
136     difference n m (translate n m k x) = difference n m x := by
137   rw [translate, ← diagonal_intCast, difference_add, difference_diagonal, add_zero]
138 
139 /-- Equality of the gcd invariant is exactly equality of actual integer orbits. -/
140 theorem sameOrbit_iff (x y : ZMod n × ZMod m) :
141     (∃ k : ℤ, translate n m k x = y) ↔ difference n m x = difference n m y := by
142   constructor
143   · rintro ⟨k, rfl⟩
144     exact (difference_translate n m k x).symm
145   · intro h
146     obtain ⟨⟨i,t⟩, rfl⟩ := (orbitMap_bijective n m).surjective x
147     obtain ⟨⟨j,u⟩, rfl⟩ := (orbitMap_bijective n m).surjective y
148     simp only [difference_orbitMap] at h
149     have hij : i = j := by
150       apply Fin.ext
151       have heq := (ZMod.natCast_eq_natCast_iff' i.val j.val (Nat.gcd n m)).mp h
152       simpa only [Nat.mod_eq_of_lt i.isLt, Nat.mod_eq_of_lt j.isLt] using heq
153     subst j
154     obtain ⟨k, hk⟩ := ZMod.intCast_surjective (u-t)
155     refine ⟨k, ?_⟩
156     rw [← orbitMap_translate_int, hk, ← add_sub_assoc, add_sub_cancel_left]
157 
158 /-- Distinct chosen representatives are never in the same simultaneous-translation orbit. -/
159 theorem representatives_sameOrbit_iff (i j : Fin (Nat.gcd n m)) :
160     (∃ k : ℤ, translate n m k (0, (i.val : ZMod m)) = (0, (j.val : ZMod m))) ↔
161       i = j := by
162   rw [← orbitMap_zero n m i, ← orbitMap_zero n m j, sameOrbit_iff]
163   simp only [difference_orbitMap]
164   constructor
165   · intro h
166     apply Fin.ext
167     have heq := (ZMod.natCast_eq_natCast_iff' i.val j.val (Nat.gcd n m)).mp h
168     simpa only [Nat.mod_eq_of_lt i.isLt, Nat.mod_eq_of_lt j.isLt] using heq
169   · rintro rfl
170     rfl
171 
172 /-- Each fiber of the actual orbit invariant is an lcm-cycle. -/
173 def fiberEquiv (i : Fin (Nat.gcd n m)) :
174     ZMod (Nat.lcm n m) ≃
175       {x : ZMod n × ZMod m // difference n m x = (i.val : ZMod (Nat.gcd n m))} :=
176   Equiv.ofBijective
177     (fun t => ⟨orbitMap n m (i,t), difference_orbitMap n m (i,t)⟩) (by
178       constructor
179       · intro t u h
180         exact congrArg Prod.snd ((orbitMap_injective n m) (congrArg Subtype.val h))
181       · rintro ⟨x,hx⟩
182         obtain ⟨⟨j,t⟩, rfl⟩ := (orbitMap_bijective n m).surjective x
183         have hji : j = i := by
184           simp only [difference_orbitMap] at hx
185           apply Fin.ext
186           have heq := (ZMod.natCast_eq_natCast_iff' j.val i.val (Nat.gcd n m)).mp hx
187           simpa only [Nat.mod_eq_of_lt j.isLt, Nat.mod_eq_of_lt i.isLt] using heq
188         subst j
189         exact ⟨t, rfl⟩)
190 
191 theorem fiber_card (i : Fin (Nat.gcd n m)) :
192     Fintype.card {x : ZMod n × ZMod m //
193       difference n m x = (i.val : ZMod (Nat.gcd n m))} = Nat.lcm n m := by
194   rw [← Fintype.card_congr (fiberEquiv n m i), ZMod.card]
195 
196 @[simp] theorem fiberEquiv_apply (i : Fin (Nat.gcd n m)) (t : ZMod (Nat.lcm n m)) :
197     (fiberEquiv n m i t).val = orbitMap n m (i,t) := rfl
198 
199 /-- The inverse coordinate map intertwines translation with motion inside one cycle. -/
200 theorem orbitEquiv_symm_translate (k : ℤ) (x : ZMod n × ZMod m) :
201     (orbitEquiv n m).symm (translate n m k x) =
202       (((orbitEquiv n m).symm x).1, ((orbitEquiv n m).symm x).2 + k) := by
203   obtain ⟨⟨i,t⟩, rfl⟩ := (orbitEquiv n m).surjective x
204   have ht : (orbitEquiv n m).symm (orbitMap n m (i,t)) = (i,t) :=
205     (orbitEquiv n m).symm_apply_apply (i,t)
206   simp only [orbitEquiv_apply, ht]
207   rw [← orbitMap_translate_int]
208   exact (orbitEquiv n m).symm_apply_apply (i,t+k)
209 
210 end PaperXI.TameTensorOrbits

Back to source controls