FiniteAffineObstruction.lean

1 import Mathlib.Data.ZMod.Basic
2 import Mathlib.LinearAlgebra.Quotient.Basic
3 import Mathlib.Algebra.Module.Pi
4 
5 /-!
6 # A finite obstruction for affine integer systems
7 
8 For any finite affine system A x = b, any modulus p > 0, and any L >= 0,
9 the next lift of a fixed solution modulo p^L exists exactly when its residual
10 digit vanishes in an explicitly constructed finite cokernel. No lift or
11 surjectivity criterion is assumed. This is an affine-linear result, not a
12 formalization of arbitrary nonlinear native tower objects.
13 -/
14 
15 noncomputable section
16 set_option autoImplicit false
17 
18 namespace Komorebi.NativeAffine
19 
20 variable {d e : ℕ}
21 
22 /-- Coordinate reduction, viewed as an integer-linear map. -/
23 def reduction (p n : ℕ) : (Fin n → ℤ) →ₗ[ℤ] (Fin n → ZMod p) where
24   toFun x i := (x i : ZMod p)
25   map_add' x y := by ext i; simp
26   map_smul' k x := by ext i; simp
27 
28 /-- The reduction of the actual integer coefficient map. -/
29 def digitMap (p : ℕ) (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ)) :
30     (Fin d → ℤ) →ₗ[ℤ] (Fin e → ZMod p) :=
31   (reduction p e).comp A
32 
33 /-- A finite cokernel, taken over the underlying integer module. -/
34 abbrev Obstruction (p : ℕ) (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ)) :=
35   (Fin e → ZMod p) ⧸ LinearMap.range (digitMap p A)
36 
37 def obstruction (p : ℕ) (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
38     (r : Fin e → ℤ) : Obstruction p A :=
39   Submodule.Quotient.mk (reduction p e r)
40 
41 theorem obstruction_finite (p : ℕ) [NeZero p]
42     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ)) : Finite (Obstruction p A) := by
43   infer_instance
44 
45 /-- Cokernel zero is equivalent to an actual correcting vector. -/
46 theorem obstruction_zero_iff_correction (p : ℕ)
47     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ)) (r : Fin e → ℤ) :
48     obstruction p A r = 0 ↔ ∃ t : Fin d → ℤ, reduction p e (r + A t) = 0 := by
49   change Submodule.Quotient.mk (reduction p e r) = 0 ↔ _
50   rw [Submodule.Quotient.mk_eq_zero]
51   constructor
52   · rintro ⟨t, ht⟩
53     refine ⟨-t, ?_⟩
54     change digitMap p A t = reduction p e r at ht
55     simp only [map_add, map_neg]
56     change reduction p e r + -(digitMap p A t) = 0
57     rw [ht, add_neg_cancel]
58   · rintro ⟨t, ht⟩
59     refine ⟨-t, ?_⟩
60     rw [map_neg]
61     have h : reduction p e r + digitMap p A t = 0 := by
62       simpa only [map_add, digitMap, LinearMap.comp_apply] using ht
63     exact (eq_neg_of_add_eq_zero_left h).symm
64 
65 /-- Changing the base representative by p^L times a vector adds A s to
66 the residual, without changing its cokernel class. -/
67 theorem obstruction_representative_independent (p : ℕ)
68     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ)) (r : Fin e → ℤ) (s : Fin d → ℤ) :
69     obstruction p A (r + A s) = obstruction p A r := by
70   change Submodule.Quotient.mk (reduction p e (r + A s)) = _
71   rw [map_add, Submodule.Quotient.mk_add]
72   have hs : (Submodule.Quotient.mk (reduction p e (A s)) : Obstruction p A) = 0 := by
73     rw [Submodule.Quotient.mk_eq_zero]
74     exact ⟨s, rfl⟩
75   rw [hs, add_zero]
76   rfl
77 
78 theorem reduction_zero_iff (p : ℕ) (r : Fin e → ℤ) :
79     reduction p e r = 0 ↔ ∀ i, (p : ℤ) ∣ r i := by
80   constructor
81   · intro h i
82     exact (ZMod.intCast_zmod_eq_zero_iff_dvd (r i) p).mp (congrFun h i)
83   · intro h
84     ext i
85     exact (ZMod.intCast_zmod_eq_zero_iff_dvd (r i) p).mpr (h i)
86 
87 /-- Exact residual transport is derived from linearity. -/
88 theorem affine_residual_transport (q : ℤ)
89     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
90     (b r : Fin e → ℤ) (x t : Fin d → ℤ) (hr : A x - b = q • r) :
91     A (x + q • t) - b = q • (r + A t) := by
92   rw [map_add, map_smul, add_sub_right_comm, hr, smul_add]
93 
94 /-- A fixed residual digit determines exactly whether the solution lifts
95 from modulus p^L to p^(L+1). This includes all finite affine integer systems. -/
96 theorem affine_lift_iff_obstruction_zero (p L : ℕ) (hp : 0 < p)
97     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
98     (b r : Fin e → ℤ) (x : Fin d → ℤ)
99     (hr : A x - b = (p : ℤ)^L • r) :
100     (∃ t : Fin d → ℤ, ∀ i,
101       (p : ℤ)^(L+1) ∣ (A (x + (p : ℤ)^L • t) - b) i) ↔
102     obstruction p A r = 0 := by
103   rw [obstruction_zero_iff_correction]
104   have hq : (p : ℤ)^L ≠ 0 := pow_ne_zero _ (Int.natCast_ne_zero.mpr (Nat.ne_of_gt hp))
105   constructor
106   · rintro ⟨t, ht⟩
107     refine ⟨t, (reduction_zero_iff p (r + A t)).mpr ?_⟩
108     intro i
109     have hi := ht i
110     rw [affine_residual_transport _ A b r x t hr] at hi
111     change (p : ℤ)^(L+1) ∣ (p : ℤ)^L * (r + A t) i at hi
112     rwa [pow_succ, mul_dvd_mul_iff_left hq] at hi
113   · rintro ⟨t, ht⟩
114     refine ⟨t, ?_⟩
115     intro i
116     rw [affine_residual_transport _ A b r x t hr]
117     change (p : ℤ)^(L+1) ∣ (p : ℤ)^L * (r + A t) i
118     rw [pow_succ, mul_dvd_mul_iff_left hq]
119     exact (reduction_zero_iff p (r + A t)).mp ht i
120 
121 /-- Every solution modulo p^L has a residual vector; the criterion above
122 does not require an unexplained residual representation assumption. -/
123 theorem residual_exists (p L : ℕ)
124     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ)) (b : Fin e → ℤ) (x : Fin d → ℤ)
125     (hx : ∀ i, (p : ℤ)^L ∣ (A x - b) i) :
126     ∃ r : Fin e → ℤ, A x - b = (p : ℤ)^L • r := by
127   choose r hr using hx
128   exact ⟨r, funext hr⟩
129 
130 /-- All representatives of one residue vector are obtained by digit correction. -/
131 theorem same_residue_iff (q : ℤ) (x y : Fin d → ℤ) :
132     (∀ i, q ∣ (y - x) i) ↔ ∃ t : Fin d → ℤ, y = x + q • t := by
133   constructor
134   · intro h
135     choose t ht using h
136     refine ⟨t, ?_⟩
137     ext i
138     have hi := ht i
139     change y i - x i = q * t i at hi
140     change y i = x i + q * t i
141     exact sub_eq_iff_eq_add'.mp hi
142   · rintro ⟨t, rfl⟩ i
143     change q ∣ x i + q * t i - x i
144     simp
145 
146 /-- Every finite affine system has an explicit finite obstruction at each
147 actual solution, and its vanishing is equivalent to existence of a next-level
148 solution with the same lower-level residue. -/
149 theorem finite_affine_obstruction (p L : ℕ) (hp : 0 < p)
150     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ)) (b : Fin e → ℤ) (x : Fin d → ℤ)
151     (hx : ∀ i, (p : ℤ)^L ∣ (A x - b) i) :
152     ∃ r : Fin e → ℤ,
153       A x - b = (p : ℤ)^L • r ∧
154       Finite (Obstruction p A) ∧
155       ((∃ y : Fin d → ℤ,
156         (∀ i, (p : ℤ)^L ∣ (y - x) i) ∧
157         (∀ i, (p : ℤ)^(L+1) ∣ (A y - b) i)) ↔ obstruction p A r = 0) := by
158   obtain ⟨r, hr⟩ := residual_exists p L A b x hx
159   let : NeZero p := ⟨Nat.ne_of_gt hp⟩
160   refine ⟨r, hr, obstruction_finite p A, ?_⟩
161   rw [← affine_lift_iff_obstruction_zero p L hp A b r x hr]
162   constructor
163   · rintro ⟨y, hy, hAy⟩
164     obtain ⟨t, rfl⟩ := (same_residue_iff ((p : ℤ)^L) x y).mp hy
165     exact ⟨t, hAy⟩
166   · rintro ⟨t, ht⟩
167     exact ⟨x + (p : ℤ)^L • t,
168       (same_residue_iff ((p : ℤ)^L) x _).mpr ⟨t, rfl⟩, ht⟩
169 
170 #print axioms reduction
171 #print axioms digitMap
172 #print axioms Obstruction
173 #print axioms obstruction
174 #print axioms obstruction_finite
175 #print axioms obstruction_zero_iff_correction
176 #print axioms obstruction_representative_independent
177 #print axioms reduction_zero_iff
178 #print axioms affine_residual_transport
179 #print axioms affine_lift_iff_obstruction_zero
180 #print axioms residual_exists
181 #print axioms same_residue_iff
182 #print axioms finite_affine_obstruction
183 
184 end Komorebi.NativeAffine

Back to source controls