ComparisonCertificates.lean

1 import PaperX.MatrixWitnessLimits
2 import PaperX.RepresentationForests
3 import PaperX.FiniteFiberBranches
4 
5 /-! Finite local intertwining certificates are selected together with the global
6 representation. A fixed detecting depth prevents the comparison determinants
7 from tending to zero. No compatible choices of witnesses are assumed. -/
8 set_option autoImplicit false
9 namespace PaperX.ComparisonCertificates
10 open PaperX.RepresentationLimits PaperX.RepresentationTopology PaperX.RepresentationForests
11 variable {R G ι S : Type} [CommRing R] [Group G] [Fintype ι] [DecidableEq ι]
12 variable (I : Ideal R) (C : Conditions (G := G) (ι := ι) I)
13 variable {H : S → Type} [∀ s, Group (H s)]
14 variable (φ : ∀ s, H s →* G) (τ : ∀ s, MatrixRep R (H s) ι) (d : S → ℕ)
15 
16 /-- The determinant test is imposed only once the fixed detecting precision is
17 available. In particular, precision zero is not required to contain a nonzero scalar. -/
18 structure Node (k : ℕ) where
19   rep : MatrixRep (R ⧸ I^k) G ι
20   allowed : C.allowed k rep
21   comparison : ∀ _s : S, Matrix ι ι (R ⧸ I^k)
22   intertwines : ∀ s g, rep (φ s g) * comparison s = comparison s * (reduce I (τ s) k) g
23   detected : ∀ s (h : d s ≤ k), Ideal.Quotient.factorPow I h (comparison s).det ≠ 0
24 
25 /-- The full certificate reduces, including its determinant test at the same
26 fixed depth. This is a total parent map, not a surjectivity assumption. -/
27 def nodeTransition {j k : ℕ} (h : j ≤ k) (x : Node I C φ τ d k) :
28     Node I C φ τ d j where
29   rep := transition I h x.rep
30   allowed := C.downward h x.rep x.allowed
31   comparison s := (x.comparison s).map (Ideal.Quotient.factorPow I h)
32   intertwines s g := by
33     have hx := congrArg (fun A => A.map (Ideal.Quotient.factorPow I h)) (x.intertwines s g)
34     rw [Matrix.map_mul, Matrix.map_mul] at hx
35     have hτ := congrArg (fun ρ => ρ g) (transition_reduce I (τ s) h)
36     change ((reduce I (τ s) k) g).map (Ideal.Quotient.factorPow I h) = _ at hτ
37     rw [hτ] at hx
38     exact hx
39   detected s hs := by
40     change Ideal.Quotient.factorPow I hs
41       ((Ideal.Quotient.factorPow I h).mapMatrix (x.comparison s)).det ≠ 0
42     rw [← (Ideal.Quotient.factorPow I h).map_det]
43     simpa only [Ideal.Quotient.factor_comp_apply] using x.detected s (hs.trans h)
44 
45 /-- Both representations and their comparison matrices belong to the branch. -/
46 def certificateTower : PaperX.Compactness.Tower where
47   Level k := Node I C φ τ d k
48   parent k := nodeTransition I C φ τ d (Nat.le_succ k)
49 
50 /-- Coefficient finiteness controls witnesses, whereas finiteness of the actual
51 allowed representation set is a separate premise. The group need not be finite. -/
52 theorem node_finite [Finite S] (k : ℕ) [Finite (R ⧸ I^k)]
53     [Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ}] :
54     Finite (Node I C φ τ d k) := by
55   let f : Node I C φ τ d k →
56       {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ} × (S → Matrix ι ι (R ⧸ I^k)) :=
57     fun x => (⟨x.rep, x.allowed⟩, x.comparison)
58   apply Finite.of_injective f
59   intro x y h
60   have hrep : x.rep = y.rep := congrArg (fun z => z.1.val) h
61   have hmat : x.comparison = y.comparison := congrArg Prod.snd h
62   cases x
63   cases y
64   cases hrep
65   cases hmat
66   rfl
67 
68 /-- Compactness makes simultaneous coherent choices from separately occupied
69 augmented levels. No coherent sequence of comparison matrices is an input. -/
70 theorem exists_certificate_branch [Finite S]
71     (finiteR : ∀ k, Finite (R ⧸ I^k))
72     (finiteC : ∀ k, Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ})
73     (occupied : ∀ k, Nonempty (Node I C φ τ d k)) :
74     Nonempty (PaperX.Compactness.Branch (certificateTower I C φ τ d)) := by
75   apply PaperX.Compactness.finite_branch_compactness
76   · apply PaperX.FiniteFiberBranches.finite_levels
77     intro k
78     let : Finite (R ⧸ I^k) := finiteR k
79     let : Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ} := finiteC k
80     exact node_finite I C φ τ d k
81   · exact occupied
82 
83 /-- Adjacent compatibility gives compatibility at every pair of precisions. -/
84 theorem branch_rep_compatible
85     (b : PaperX.Compactness.Branch (certificateTower I C φ τ d))
86     {j k : ℕ} (h : j ≤ k) :
87     transition I h (b.value k).rep = (b.value j).rep := by
88   ext g a c
89   apply (Ideal.Quotient.eq_factor_of_eq_factor_succ
90     (fun _ _ h => Ideal.pow_le_pow_right h)
91     (fun m => (b.value m).rep g a c) ?_ h).symm
92   intro m
93   exact (congrArg (fun x => x.rep g a c) (b.compatible m)).symm
94 
95 def branchRepFamily
96     (b : PaperX.Compactness.Branch (certificateTower I C φ τ d)) : Family R I G ι where
97   maps k := (b.value k).rep
98   compatible := branch_rep_compatible I C φ τ d b
99 
100 open PaperX.MatrixWitnessLimits
101 
102 /-- The comparison matrices come from the same augmented branch as the representation. -/
103 def branchMatrixFamily
104     (b : PaperX.Compactness.Branch (certificateTower I C φ τ d)) (s : S) :
105     MatrixFamily R I ι :=
106   matrix_family_of_succ I (fun k => (b.value k).comparison s)
107     (fun k => congrArg (fun x => x.comparison s) (b.compatible k))
108 
109 /-- Simultaneous reconstruction produces integral comparisons satisfying the
110 actual local intertwining equations and retaining a finite nonzero determinant test. -/
111 theorem branch_realizes [IsAdicComplete I R]
112     (b : PaperX.Compactness.Branch (certificateTower I C φ τ d)) :
113     let ρ := reconstruct I (branchRepFamily I C φ τ d b)
114     let P := fun s => reconstructMatrix I (branchMatrixFamily I C φ τ d b s)
115     Realizes I C ρ ∧
116       (∀ s g, ρ (φ s g) * P s = P s * τ s g) ∧
117       (∀ s, Ideal.Quotient.mk (I^(d s)) (P s).det ≠ 0) := by
118   dsimp only
119   refine ⟨?_, ?_, ?_⟩
120   · intro k
121     rw [reconstruct_reduces]
122     exact (b.value k).allowed
123   · intro s g
124     apply reconstructMatrix_local_intertwines
125     intro k x
126     exact (b.value k).intertwines s x
127   · intro s
128     have hx := (b.value (d s)).detected s (le_refl _)
129     simp only [Ideal.Quotient.factor_eq, RingHom.id_apply] at hx
130     rw [(Ideal.Quotient.mk (I^(d s))).map_det]
131     change ((reconstructMatrix I (branchMatrixFamily I C φ τ d b s)).map
132       (Ideal.Quotient.mk (I^(d s)))).det ≠ 0
133     rw [reconstructMatrix_reduces]
134     exact hx
135 
136 /-- Existence uses occupied finite certificate levels. The detecting depths
137 are fixed before the quantification over precision. -/
138 theorem exists_comparison_realization [IsAdicComplete I R] [Finite S]
139     (finiteR : ∀ k, Finite (R ⧸ I^k))
140     (finiteC : ∀ k, Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ})
141     (occupied : ∀ k, Nonempty (Node I C φ τ d k)) :
142     ∃ (ρ : MatrixRep R G ι) (P : S → Matrix ι ι R),
143       Realizes I C ρ ∧
144       (∀ s g, ρ (φ s g) * P s = P s * τ s g) ∧
145       (∀ s, Ideal.Quotient.mk (I^(d s)) (P s).det ≠ 0) := by
146   obtain ⟨b⟩ := exists_certificate_branch I C φ τ d finiteR finiteC occupied
147   exact ⟨reconstruct I (branchRepFamily I C φ τ d b),
148     fun s => reconstructMatrix I (branchMatrixFamily I C φ τ d b s),
149     branch_realizes I C φ τ d b⟩
150 
151 /-- Finite continuity is checked on allowed representations, and survives the
152 same simultaneous reconstruction used for the local comparison certificates. -/
153 theorem exists_continuous_comparison_realization [IsAdicComplete I R] [Finite S]
154     [TopologicalSpace G]
155     (finiteR : ∀ k, Finite (R ⧸ I^k))
156     (finiteC : ∀ k, Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ})
157     (occupied : ∀ k, Nonempty (Node I C φ τ d k))
158     (continuous : ∀ k ρ, C.allowed k ρ → FiniteRepContinuous ρ) :
159     ∃ (ρ : MatrixRep R G ι) (P : S → Matrix ι ι R),
160       Realizes I C ρ ∧ AdicRepContinuous I ρ ∧
161       (∀ s g, ρ (φ s g) * P s = P s * τ s g) ∧
162       (∀ s, Ideal.Quotient.mk (I^(d s)) (P s).det ≠ 0) := by
163   obtain ⟨b⟩ := exists_certificate_branch I C φ τ d finiteR finiteC occupied
164   have hb := branch_realizes I C φ τ d b
165   refine ⟨reconstruct I (branchRepFamily I C φ τ d b),
166     fun s => reconstructMatrix I (branchMatrixFamily I C φ τ d b s),
167     hb.1, ?_, hb.2⟩
168   apply reconstructed_continuous
169   intro k
170   exact continuous k (b.value k).rep (b.value k).allowed
171 
172 /-- An actual integral realization with detected comparison determinants supplies
173 an augmented node at every precision by reduction. -/
174 def node_of_integral (ρ : MatrixRep R G ι) (P : S → Matrix ι ι R)
175     (hρ : Realizes I C ρ)
176     (hP : ∀ s g, ρ (φ s g) * P s = P s * τ s g)
177     (hdet : ∀ s, Ideal.Quotient.mk (I^(d s)) (P s).det ≠ 0) (k : ℕ) :
178     Node I C φ τ d k where
179   rep := reduce I ρ k
180   allowed := hρ k
181   comparison s := (P s).map (Ideal.Quotient.mk (I^k))
182   intertwines s g := by
183     have hx := congrArg (fun A => A.map (Ideal.Quotient.mk (I^k))) (hP s g)
184     rw [Matrix.map_mul, Matrix.map_mul] at hx
185     exact hx
186   detected s hs := by
187     change Ideal.Quotient.factorPow I hs
188       ((Ideal.Quotient.mk (I^k)).mapMatrix (P s)).det ≠ 0
189     rw [← (Ideal.Quotient.mk (I^k)).map_det, Ideal.Quotient.factor_mk]
190     exact hdet s
191 
192 /-- The finite criterion is exact for integral comparisons carrying these fixed
193 determinant certificates. It does not assert that arbitrary local packets supply them. -/
194 theorem comparison_realization_iff [IsAdicComplete I R] [Finite S]
195     (finiteR : ∀ k, Finite (R ⧸ I^k))
196     (finiteC : ∀ k, Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ}) :
197     (∃ (ρ : MatrixRep R G ι) (P : S → Matrix ι ι R),
198       Realizes I C ρ ∧
199       (∀ s g, ρ (φ s g) * P s = P s * τ s g) ∧
200       (∀ s, Ideal.Quotient.mk (I^(d s)) (P s).det ≠ 0)) ↔
201       ∀ k, Nonempty (Node I C φ τ d k) := by
202   constructor
203   · rintro ⟨ρ, P, hρ, hP, hdet⟩ k
204     exact ⟨node_of_integral I C φ τ d ρ P hρ hP hdet k⟩
205   · exact exists_comparison_realization I C φ τ d finiteR finiteC
206 
207 end PaperX.ComparisonCertificates

Back to source controls