PeriodicLatticeReduction60.lean

1 import PaperXI.ActualELatticeNormalizer59
2 import Mathlib.Algebra.Ring.Periodic
3 
4 /-!
5 # Finite reduction of the literal lattice-chain conditions
6 
7 A positive period given by a base-field scalar reduces the entire integer
8 chain to finitely many levels for every base-field linear automorphism.
9 -/
10 set_option autoImplicit false
11 noncomputable section
12 namespace PaperXI.PeriodicLatticeReduction60
13 open ActualELatticeNormalizer59
14 variable {K V : Type*} [Field K] [AddCommGroup V] [Module K V]
15 
16 /-- The exact preservation and adjacent-congruence test at one chain level. -/
17 def levelCondition (L : ℤ → AddSubgroup V) (g : V ≃ₗ[K] V) (i : ℤ) : Prop :=
18   (∀ v, g v ∈ L i ↔ v ∈ L i) ∧ (∀ v ∈ L i, g v - v ∈ L (i + 1))
19 
20 /-- Multiplication by a base-field unit transfers each one-level condition. -/
21 theorem levelCondition_shift (L : ℤ → AddSubgroup V) (c : Kˣ) (r : ℤ)
22     (hperiod : ∀ i v, (c : K) • v ∈ L (i + r) ↔ v ∈ L i)
23     (g : V ≃ₗ[K] V) (i : ℤ) :
24     levelCondition L g (i + r) ↔ levelCondition L g i := by
25   have hmap (v : V) : g ((c : K) • v) = (c : K) • g v := g.map_smul _ _
26   have hdiff (v : V) : g ((c : K) • v) - (c : K) • v = (c : K) • (g v - v) := by
27     rw [hmap, smul_sub]
28   constructor
29   · rintro ⟨hg, hd⟩
30     constructor
31     · intro v
32       have h := hg ((c : K) • v)
33       rwa [hmap, hperiod, hperiod] at h
34     · intro v hv
35       have h := hd ((c : K) • v) ((hperiod i v).mpr hv)
36       rw [hdiff, show i + r + 1 = (i + 1) + r by omega, hperiod] at h
37       exact h
38   · rintro ⟨hg, hd⟩
39     constructor
40     · intro v
41       obtain ⟨w, rfl⟩ := (LinearEquiv.smulOfNeZero K V (c : K) c.ne_zero).surjective v
42       change g ((c : K) • w) ∈ L (i + r) ↔ (c : K) • w ∈ L (i + r)
43       rw [hmap, hperiod, hperiod]
44       exact hg w
45     · intro v hv
46       obtain ⟨w, rfl⟩ := (LinearEquiv.smulOfNeZero K V (c : K) c.ne_zero).surjective v
47       change (c : K) • w ∈ L (i + r) at hv
48       change g ((c : K) • w) - (c : K) • w ∈ L (i + r + 1)
49       rw [hdiff, show i + r + 1 = (i + 1) + r by omega, hperiod]
50       exact hd w ((hperiod i w).mp hv)
51 
52 /-- The level predicate is literally periodic as a `Prop`-valued function. -/
53 theorem levelCondition_periodic (L : ℤ → AddSubgroup V) (c : Kˣ) (r : ℤ)
54     (hperiod : ∀ i v, (c : K) • v ∈ L (i + r) ↔ v ∈ L i)
55     (g : V ≃ₗ[K] V) : Function.Periodic (levelCondition L g) r := by
56   intro i
57   exact propext (levelCondition_shift L c r hperiod g i)
58 
59 /-- All infinitely many congruence conditions reduce to one positive period. -/
60 theorem mem_firstCongruence_iff_fin (L : ℤ → AddSubgroup V) (c : Kˣ) (r : ℕ)
61     (hr : 0 < r)
62     (hperiod : ∀ i v, (c : K) • v ∈ L (i + (r : ℤ)) ↔ v ∈ L i)
63     (g : V ≃ₗ[K] V) :
64     g ∈ firstCongruence L ↔ ∀ j : Fin r, levelCondition L g (j.val : ℤ) := by
65   constructor
66   · intro h j
67     exact ⟨h.1 j.val, h.2 j.val⟩
68   · intro h
69     have hall : ∀ i : ℤ, levelCondition L g i := by
70       intro i
71       have hp := levelCondition_periodic L c (r : ℤ) hperiod g
72       have hm := hp.sub_zsmul_eq (x := i) (i / (r : ℤ))
73       have he : i - (i / (r : ℤ)) • (r : ℤ) = i % (r : ℤ) := by
74         simp only [zsmul_eq_mul, Int.cast_id, Int.emod_def, mul_comm]
75       rw [he] at hm
76       rw [← hm]
77       have hn : 0 ≤ i % (r : ℤ) := Int.emod_nonneg i (by omega)
78       have hl : i % (r : ℤ) < (r : ℤ) := Int.emod_lt_of_pos i (by omega)
79       let j : Fin r := ⟨(i % (r : ℤ)).toNat, by omega⟩
80       have hj : (j.val : ℤ) = i % (r : ℤ) := by
81         dsimp [j]
82         exact Int.toNat_of_nonneg hn
83       simpa only [hj] using h j
84     exact ⟨fun i => (hall i).1, fun i => (hall i).2⟩
85 
86 end PaperXI.PeriodicLatticeReduction60

Back to source controls