AffinePairTransport.lean

1 module
2 public import AffineObstructionCore
3 
4 /-!
5 # Exact transport for two affine lifting conditions
6 
7 Author: Komorebi P.
8 The same correction vector must satisfy both residual-digit equations.
9 The modulus is any positive natural number; level zero is included.
10 -/
11 
12 @[expose] public section
13 set_option autoImplicit false
14 
15 namespace Komorebi.AffinePair
16 open Komorebi.NativeAffine
17 
18 variable {d e f : ℕ}
19 
20 /-- Two systems lift at a single vector representing the original residue. -/
21 def HasJointLift (p L : ℕ)
22     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
23     (B : (Fin d → ℤ) →ₗ[ℤ] (Fin f → ℤ))
24     (b : Fin e → ℤ) (c : Fin f → ℤ) (x : Fin d → ℤ) : Prop :=
25   ∃ y : Fin d → ℤ,
26     (∀ i, (p : ℤ)^L ∣ (y - x) i) ∧
27     (∀ i, (p : ℤ)^(L+1) ∣ (A y - b) i) ∧
28     (∀ i, (p : ℤ)^(L+1) ∣ (B y - c) i)
29 
30 theorem next_level_iff_digit (p L : ℕ) (hp : 0 < p)
31     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
32     (b r : Fin e → ℤ) (x t : Fin d → ℤ)
33     (hr : A x - b = (p : ℤ)^L • r) :
34     (∀ i, (p : ℤ)^(L+1) ∣ (A (x + (p : ℤ)^L • t) - b) i) ↔
35     reduction p e (r + A t) = 0 := by
36   rw [reduction_zero_iff]
37   have hq : (p : ℤ)^L ≠ 0 :=
38     pow_ne_zero _ (Int.natCast_ne_zero.mpr (Nat.ne_of_gt hp))
39   constructor <;> intro h i
40   · have hi := h i
41     rw [affine_residual_transport _ A b r x t hr] at hi
42     change (p : ℤ)^(L+1) ∣ (p : ℤ)^L * (r + A t) i at hi
43     rwa [pow_succ, mul_dvd_mul_iff_left hq] at hi
44   · rw [affine_residual_transport _ A b r x t hr]
45     change (p : ℤ)^(L+1) ∣ (p : ℤ)^L * (r + A t) i
46     rw [pow_succ, mul_dvd_mul_iff_left hq]
47     exact h i
48 
49 theorem joint_lift_iff_digit_correction (p L : ℕ) (hp : 0 < p)
50     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
51     (B : (Fin d → ℤ) →ₗ[ℤ] (Fin f → ℤ))
52     (b r : Fin e → ℤ) (c s : Fin f → ℤ) (x : Fin d → ℤ)
53     (hr : A x - b = (p : ℤ)^L • r)
54     (hs : B x - c = (p : ℤ)^L • s) :
55     HasJointLift p L A B b c x ↔
56     ∃ t : Fin d → ℤ, reduction p e (r + A t) = 0 ∧
57       reduction p f (s + B t) = 0 := by
58   constructor
59   · rintro ⟨y, hy, hA, hB⟩
60     obtain ⟨t, rfl⟩ := (same_residue_iff ((p : ℤ)^L) x y).mp hy
61     exact ⟨t, (next_level_iff_digit p L hp A b r x t hr).mp hA,
62       (next_level_iff_digit p L hp B c s x t hs).mp hB⟩
63   · rintro ⟨t, hA, hB⟩
64     refine ⟨x + (p : ℤ)^L • t,
65       (same_residue_iff ((p : ℤ)^L) x _).mpr ⟨t, rfl⟩, ?_, ?_⟩
66     · exact (next_level_iff_digit p L hp A b r x t hr).mpr hA
67     · exact (next_level_iff_digit p L hp B c s x t hs).mpr hB
68 
69 /-- With any known individual correction, its whole solution set is a fiber
70 of the actual reduced coefficient map. -/
71 theorem digit_correction_iff_same_image (p : ℕ)
72     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
73     (r : Fin e → ℤ) (u t : Fin d → ℤ)
74     (hu : reduction p e (r + A u) = 0) :
75     reduction p e (r + A t) = 0 ↔ digitMap p A t = digitMap p A u := by
76   have hu' : reduction p e r + digitMap p A u = 0 := by
77     simpa only [map_add, digitMap, LinearMap.comp_apply] using hu
78   have ht : reduction p e (r + A t) = reduction p e r + digitMap p A t := by
79     simp only [map_add, digitMap, LinearMap.comp_apply]
80   rw [ht]
81   constructor
82   · intro h
83     exact add_left_cancel (h.trans hu'.symm)
84   · intro h
85     rwa [h]
86 
87 end Komorebi.AffinePair
88 
89 #print axioms Komorebi.AffinePair.HasJointLift
90 #print axioms Komorebi.AffinePair.next_level_iff_digit
91 #print axioms Komorebi.AffinePair.joint_lift_iff_digit_correction
92 #print axioms Komorebi.AffinePair.digit_correction_iff_same_image

Back to source controls