AffineSharedCorrection.lean

1 module
2 public import SharedCorrection
3 public import AffinePairTransport
4 
5 /-!
6 # A finite shared obstruction for two affine congruence lifts
7 
8 Author: Komorebi P.
9 All coefficient and reduction maps below are the actual integer-linear maps.
10 No surjectivity, common correction, or compatibility premise is hidden in the
11 finite existence theorem. This concerns one lift at a time.
12 -/
13 
14 @[expose] public section
15 noncomputable section
16 set_option autoImplicit false
17 
18 namespace Komorebi.AffinePair
19 open Komorebi.NativeAffine Komorebi.SharedCorrection
20 
21 variable {d e f : ℕ}
22 
23 abbrev SharedObstruction (p : ℕ)
24     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
25     (B : (Fin d → ℤ) →ₗ[ℤ] (Fin f → ℤ)) :=
26   Common (digitMap p A) (digitMap p B)
27 
28 theorem shared_obstruction_finite (p : ℕ) (hp : 0 < p)
29     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
30     (B : (Fin d → ℤ) →ₗ[ℤ] (Fin f → ℤ)) :
31     Finite (SharedObstruction p A B) := by
32   let : NeZero p := ⟨Nat.ne_of_gt hp⟩
33   exact common_finite_of_left (digitMap p A) (digitMap p B)
34 
35 /-- Any two individually valid correction vectors give the same left label. -/
36 theorem left_class_independent (p : ℕ)
37     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
38     (B : (Fin d → ℤ) →ₗ[ℤ] (Fin f → ℤ))
39     (r : Fin e → ℤ) (u u' : Fin d → ℤ)
40     (hu : reduction p e (r + A u) = 0)
41     (hu' : reduction p e (r + A u') = 0) :
42     (Submodule.Quotient.mk u : SharedObstruction p A B) =
43       Submodule.Quotient.mk u' := by
44   apply (quotient_mk_eq_iff_common (digitMap p A) (digitMap p B) u u').mpr
45   exact ⟨u', (digit_correction_iff_same_image p A r u u' hu).mp hu', rfl⟩
46 
47 theorem right_class_independent (p : ℕ)
48     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
49     (B : (Fin d → ℤ) →ₗ[ℤ] (Fin f → ℤ))
50     (s : Fin f → ℤ) (v v' : Fin d → ℤ)
51     (hv : reduction p f (s + B v) = 0)
52     (hv' : reduction p f (s + B v') = 0) :
53     (Submodule.Quotient.mk v : SharedObstruction p A B) =
54       Submodule.Quotient.mk v' := by
55   apply (quotient_mk_eq_iff_common (digitMap p A) (digitMap p B) v v').mpr
56   exact ⟨v, rfl, ((digit_correction_iff_same_image p B s v v' hv).mp hv').symm⟩
57 
58 /-- Given individual lifts, equality in the fixed finite common quotient is
59 exactly the remaining condition for a joint lift. -/
60 theorem joint_lift_iff_class_eq (p L : ℕ) (hp : 0 < p)
61     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
62     (B : (Fin d → ℤ) →ₗ[ℤ] (Fin f → ℤ))
63     (b r : Fin e → ℤ) (c s : Fin f → ℤ) (x u v : Fin d → ℤ)
64     (hr : A x - b = (p : ℤ)^L • r)
65     (hs : B x - c = (p : ℤ)^L • s)
66     (hu : reduction p e (r + A u) = 0)
67     (hv : reduction p f (s + B v) = 0) :
68     HasJointLift p L A B b c x ↔
69     (Submodule.Quotient.mk u : SharedObstruction p A B) =
70       Submodule.Quotient.mk v := by
71   rw [joint_lift_iff_digit_correction p L hp A B b r c s x hr hs,
72     quotient_mk_eq_iff_common]
73   exact exists_congr fun t => and_congr
74     (digit_correction_iff_same_image p A r u t hu)
75     (digit_correction_iff_same_image p B s v t hv)
76 
77 /-- The unconditioned form includes individual solvability as part of the
78 criterion, so it cannot assert that arbitrary pairs of targets glue. -/
79 theorem joint_lift_iff_compatible_corrections (p L : ℕ) (hp : 0 < p)
80     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
81     (B : (Fin d → ℤ) →ₗ[ℤ] (Fin f → ℤ))
82     (b r : Fin e → ℤ) (c s : Fin f → ℤ) (x : Fin d → ℤ)
83     (hr : A x - b = (p : ℤ)^L • r)
84     (hs : B x - c = (p : ℤ)^L • s) :
85     HasJointLift p L A B b c x ↔
86     ∃ u v : Fin d → ℤ,
87       reduction p e (r + A u) = 0 ∧ reduction p f (s + B v) = 0 ∧
88       (Submodule.Quotient.mk u : SharedObstruction p A B) =
89         Submodule.Quotient.mk v := by
90   constructor
91   · intro h
92     obtain ⟨t, hA, hB⟩ :=
93       (joint_lift_iff_digit_correction p L hp A B b r c s x hr hs).mp h
94     exact ⟨t, t, hA, hB, rfl⟩
95   · rintro ⟨u, v, hu, hv, huv⟩
96     exact (joint_lift_iff_class_eq p L hp A B b r c s x u v hr hs hu hv).mpr huv
97 
98 /-- Every actual lower-level solution supplies its residuals and a finite
99 quotient whose compatibility condition characterizes the next joint lift. -/
100 theorem finite_affine_pair_compatibility (p L : ℕ) (hp : 0 < p)
101     (A : (Fin d → ℤ) →ₗ[ℤ] (Fin e → ℤ))
102     (B : (Fin d → ℤ) →ₗ[ℤ] (Fin f → ℤ))
103     (b : Fin e → ℤ) (c : Fin f → ℤ) (x : Fin d → ℤ)
104     (hxA : ∀ i, (p : ℤ)^L ∣ (A x - b) i)
105     (hxB : ∀ i, (p : ℤ)^L ∣ (B x - c) i) :
106     ∃ (r : Fin e → ℤ) (s : Fin f → ℤ),
107       A x - b = (p : ℤ)^L • r ∧ B x - c = (p : ℤ)^L • s ∧
108       Finite (SharedObstruction p A B) ∧
109       (HasJointLift p L A B b c x ↔
110         ∃ u v : Fin d → ℤ,
111           reduction p e (r + A u) = 0 ∧ reduction p f (s + B v) = 0 ∧
112           (Submodule.Quotient.mk u : SharedObstruction p A B) =
113             Submodule.Quotient.mk v) := by
114   obtain ⟨r, hr⟩ := residual_exists p L A b x hxA
115   obtain ⟨s, hs⟩ := residual_exists p L B c x hxB
116   exact ⟨r, s, hr, hs, shared_obstruction_finite p hp A B,
117     joint_lift_iff_compatible_corrections p L hp A B b r c s x hr hs⟩
118 
119 end Komorebi.AffinePair
120 
121 #print axioms Komorebi.AffinePair.SharedObstruction
122 #print axioms Komorebi.AffinePair.shared_obstruction_finite
123 #print axioms Komorebi.AffinePair.left_class_independent
124 #print axioms Komorebi.AffinePair.right_class_independent
125 #print axioms Komorebi.AffinePair.joint_lift_iff_class_eq
126 #print axioms Komorebi.AffinePair.joint_lift_iff_compatible_corrections
127 #print axioms Komorebi.AffinePair.finite_affine_pair_compatibility

Back to source controls