AffineObstructionCore.lean

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

Back to source controls