LocalComparisonCompletion.lean

1 import PaperX.ComparisonCertificates
2 import PaperX.CertificateIsomorphisms
3 import PaperX.ClassCommonSpine
4 
5 /-! Completion with independently meaningful local comparison equations. The
6 comparison matrices and their fixed detecting depths replace an uninterpreted
7 local-stability predicate for this particular class of conditions. Arithmetic
8 identification and the existence of uniform detecting bounds remain separate. -/
9 set_option autoImplicit false
10 namespace PaperX.LocalComparisonCompletion
11 open PaperX.RepresentationLimits PaperX.RepresentationTopology PaperX.RepresentationClasses
12 open PaperX.RepresentationForests PaperX.ClassCompletion PaperX.ClassCommonSpine
13 open PaperX.CompletionAssembly PaperX.ComparisonCertificates PaperX.CertificateIsomorphisms
14 
15 variable {R G ι S : Type} [CommRing R] [Group G] [TopologicalSpace G]
16 variable [Fintype ι] [DecidableEq ι] [Finite S]
17 variable {H : S → Type} [∀ s, Group (H s)]
18 
19 /-- Positive finite unframed levels, occupied comparison certificates, and one
20 continuous representative in each allowed class give actual local conjugacies.
21 Finite comparison matrices need not be units. The field inclusion is injective. -/
22 theorem unframed_comparison_completion
23     (I : Ideal R) [IsAdicComplete I R] (hI : I.FG) [Finite (R ⧸ I)]
24     (C : ClassConditions (G := G) (ι := ι) I)
25     (φ : ∀ s, H s →* G) (τ : ∀ s, MatrixRep R (H s) ι) (d : S → ℕ)
26     (finiteC : ∀ k, 0 < k → Finite {c // C.allowed k c})
27     (occupied : ∀ k, 0 < k → Nonempty (Node I (framed I C) φ τ d k))
28     (continuous : ∀ k c, C.allowed k c → ∃ σ, classOf σ = c ∧ FiniteRepContinuous σ)
29     {K : Type} [Field K] [TopologicalSpace K]
30     (inc : R →+* K) (hinj : Function.Injective inc)
31     (hinc : @Continuous R K I.adicTopology inferInstance inc) :
32     ∃ (ρ : MatrixRep R G ι) (P : S → Matrix ι ι R),
33       (∀ k, C.allowed k (classOf (reduce I ρ k))) ∧
34       Continuous (changeCoefficients inc ρ) ∧
35       ∀ s, ∃ u : (Matrix ι ι K)ˣ,
36         (u : Matrix ι ι K) = (P s).map inc ∧
37         conjugate u (changeCoefficients inc (τ s)) =
38           changeCoefficients inc (ρ.comp (φ s)) := by
39   have hf : ∀ k, Finite {ρ // (framed I C).allowed k ρ} := by
40     apply positive_finite_levels
41     intro k hk
42     let : Finite (R ⧸ I^k) := finite_coefficients I hI k
43     let : Finite {c // C.allowed k c} := finiteC k hk
44     exact framed_finite I C k
45   have ho : ∀ k, Nonempty (Node I (framed I C) φ τ d k) := by
46     intro k
47     by_cases hk : k = 0
48     · subst k
49       obtain ⟨x⟩ := occupied 1 (by decide)
50       exact ⟨nodeTransition I (framed I C) φ τ d (Nat.zero_le 1) x⟩
51     · exact occupied k (Nat.pos_of_ne_zero hk)
52   obtain ⟨ρ, P, hρ, hc, hP, hd⟩ := exists_continuous_comparison_realization I
53     (framed I C) φ τ d (finite_coefficients I hI) hf ho
54     (fun k σ hσ => all_frames_continuous (classOf σ) (continuous k _ hσ) σ rfl)
55   refine ⟨ρ, P, hρ, coefficient_change_continuous I inc hinc ρ hc, ?_⟩
56   intro s
57   apply exists_conjugating_unit inc hinj (ρ.comp (φ s)) (τ s) (P s) ?_ (hP s)
58   intro hz
59   exact hd s (by rw [hz, map_zero])
60 
61 /-- The common polynomial theorem with actual local isomorphisms produced by
62 fixed-depth certificates. There is no generic Local or stable premise here.
63 The finite witnesses, their detecting bounds and the local templates are explicit. -/
64 theorem certified_common_spine_completion
65     {Λ V E : Type} [Field E]
66     (O K : Λ → Type) [∀ l, CommRing (O l)] [∀ l, Field (K l)]
67     [∀ l, TopologicalSpace (K l)]
68     (I : ∀ l, Ideal (O l)) [∀ l, IsAdicComplete (I l) (O l)]
69     (hI : ∀ l, (I l).FG) [∀ l, Finite (O l ⧸ I l)]
70     (C : ∀ l, ClassConditions (G := G) (ι := ι) (I l))
71     (φ : ∀ s, H s →* G) (τ : ∀ l s, MatrixRep (O l) (H s) ι)
72     (d : Λ → S → ℕ)
73     (finiteC : ∀ l k, 0 < k → Finite {c // (C l).allowed k c})
74     (occupied : ∀ l k, 0 < k →
75       Nonempty (Node (I l) (framed (I l) (C l)) φ (τ l) (d l) k))
76     (continuous : ∀ l k c, (C l).allowed k c →
77       ∃ σ, classOf σ = c ∧ FiniteRepContinuous σ)
78     (inc : ∀ l, O l →+* K l) (hinj : ∀ l, Function.Injective (inc l))
79     (hinc : ∀ l, @Continuous (O l) (K l) (I l).adicTopology inferInstance (inc l))
80     (emb : ∀ l, E →+* K l) (sample : V → G) (good : Λ → V → Prop)
81     (P : V → Polynomial E) (localP : ∀ l, V → Polynomial (O l))
82     (integrality : ∀ l v, good l v → (localP l v).map (inc l) = (P v).map (emb l))
83     (spec : ∀ l k c, (C l).allowed k c → ∀ v, good l v →
84       PaperX.ClassInvariants.classCharpoly c (sample v) =
85         (localP l v).map (Ideal.Quotient.mk ((I l)^k))) :
86     ∃ (ρ : ∀ l, MatrixRep (O l) G ι) (Q : ∀ l, S → Matrix ι ι (O l)),
87       (∀ l k, (C l).allowed k (classOf (reduce (I l) (ρ l) k))) ∧
88       (∀ l, Continuous (changeCoefficients (inc l) (ρ l))) ∧
89       (∀ l s, ∃ u : (Matrix ι ι (K l))ˣ,
90         (u : Matrix ι ι (K l)) = (Q l s).map (inc l) ∧
91         conjugate u (changeCoefficients (inc l) (τ l s)) =
92           changeCoefficients (inc l) ((ρ l).comp (φ s))) ∧
93       ∀ l v, good l v →
94         (changeCoefficients (inc l) (ρ l) (sample v)).charpoly = (P v).map (emb l) := by
95   classical
96   have hx (l : Λ) := unframed_comparison_completion (I l) (hI l) (C l) φ (τ l)
97     (d l) (finiteC l) (occupied l) (continuous l) (inc l) (hinj l) (hinc l)
98   choose ρ Q hρ hc hQ using hx
99   refine ⟨ρ, Q, hρ, hc, hQ, ?_⟩
100   intro l v hv
101   apply PaperX.CommonSpine.polynomial_base_change (inc l) (emb l) (ρ l)
102     (sample v) (localP l v) (P v) ?_ (integrality l v hv)
103   apply PaperX.CommonSpine.charpoly_detected (I l)
104   intro k
105   exact spec l k (classOf (reduce (I l) (ρ l) k)) (hρ l k) v hv
106 
107 end PaperX.LocalComparisonCompletion

Back to source controls