CompletionAssembly.lean

1 import PaperX.CommonSpine
2 
3 /-! Assemble the source's conditional completion statement using only positive
4 precision, continuous coefficient inclusions, and prescribed local predicates.
5 Closedness is an explicit hypothesis of the manuscript, not an unconditional claim. -/
6 set_option autoImplicit false
7 namespace PaperX.CompletionAssembly
8 open PaperX.RepresentationLimits PaperX.RepresentationTopology PaperX.RepresentationForests
9 open PaperX.SystemCompletion PaperX.CommonSpine
10 
11 variable {R G ι : Type} [CommRing R] [Group G] [Fintype ι] [DecidableEq ι]
12 
13 theorem finite_zero_level (I : Ideal R) (C : Conditions (G := G) (ι := ι) I) :
14     Finite {ρ : MatrixRep (R ⧸ I^0) G ι // C.allowed 0 ρ} := by
15   have : Subsingleton (R ⧸ I^0) := by
16     simp only [pow_zero, Ideal.one_eq_top]
17     infer_instance
18   have : Subsingleton (MatrixRep (R ⧸ I^0) G ι) := ⟨fun a b => by
19     ext g i j
20     exact Subsingleton.elim _ _⟩
21   infer_instance
22 
23 theorem positive_finite_levels (I : Ideal R) (C : Conditions (G := G) (ι := ι) I)
24     (h : ∀ k, 0 < k → Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ}) :
25     ∀ k, Finite {ρ : MatrixRep (R ⧸ I^k) G ι // C.allowed k ρ} := by
26   intro k
27   by_cases hk : k = 0
28   · subst k
29     exact finite_zero_level I C
30   · exact h k (Nat.pos_of_ne_zero hk)
31 
32 theorem positive_levels_iff_all (I : Ideal R) (C : Conditions (G := G) (ι := ι) I) :
33     (∀ k, 0 < k → ∃ ρ, C.allowed k ρ) ↔ ∀ k, ∃ ρ, C.allowed k ρ := by
34   constructor
35   · intro h k
36     by_cases hk : k = 0
37     · subst k
38       obtain ⟨ρ, hρ⟩ := h 1 (by decide)
39       exact ⟨transition I (Nat.zero_le 1) ρ, C.downward _ _ hρ⟩
40     · exact h k (Nat.pos_of_ne_zero hk)
41   · intro h k _
42     exact h k
43 
44 theorem residual_and_higher_iff_all (I : Ideal R) (C : Conditions (G := G) (ι := ι) I) :
45     ((∃ ρ, C.allowed 1 ρ) ∧ ∀ k, 2 ≤ k → ∃ ρ, C.allowed k ρ) ↔
46       ∀ k, ∃ ρ, C.allowed k ρ := by
47   rw [← positive_levels_iff_all]
48   constructor
49   · rintro ⟨h1, hh⟩ k hk
50     by_cases h : k = 1
51     · subst k; exact h1
52     · exact hh k (by omega)
53   · intro h
54     exact ⟨h 1 (by decide), fun k hk => h k (by omega)⟩
55 
56 /-- Prescribed local predicates are evaluated on the actual field-valued
57 representations produced by coefficient change. -/
58 theorem conditional_common_spine_completion
59     {Λ V E : Type} [TopologicalSpace G] [Field E]
60     (O K : Λ → Type) [∀ l, CommRing (O l)] [∀ l, Field (K l)]
61     [∀ l, TopologicalSpace (K l)]
62     (I : (l : Λ) → Ideal (O l)) [∀ l, IsAdicComplete (I l) (O l)]
63     (C : (l : Λ) → Conditions (G := G) (ι := ι) (I l))
64     (finite : ∀ l k, 0 < k → Finite {ρ : MatrixRep (O l ⧸ (I l)^k) G ι // (C l).allowed k ρ})
65     (occupied : ∀ l k, 0 < k → ∃ ρ, (C l).allowed k ρ)
66     (continuous : ∀ l k ρ, (C l).allowed k ρ → FiniteRepContinuous ρ)
67     (inc : (l : Λ) → O l →+* K l)
68     (hinc : ∀ l, @Continuous (O l) (K l) (I l).adicTopology inferInstance (inc l))
69     (emb : (l : Λ) → E →+* K l)
70     (Local : (l : Λ) → MatrixRep (K l) G ι → Prop)
71     (stable : ∀ l ρ, Realizes (I l) (C l) ρ → Local l (changeCoefficients (inc l) ρ))
72     (sample : V → G) (good : Λ → V → Prop)
73     (P : V → Polynomial E) (localP : (l : Λ) → V → Polynomial (O l))
74     (integrality : ∀ l v, good l v → (localP l v).map (inc l) = (P v).map (emb l))
75     (spec : ∀ l k τ, (C l).allowed k τ → ∀ v, good l v →
76       (τ (sample v)).charpoly = (localP l v).map (Ideal.Quotient.mk ((I l)^k))) :
77     ∃ ρ : (l : Λ) → MatrixRep (O l) G ι,
78       SystemRealizes O I C ρ ∧
79       (∀ l, Continuous (changeCoefficients (inc l) (ρ l)) ∧
80         Local l (changeCoefficients (inc l) (ρ l))) ∧
81       ∀ l v, good l v →
82         (changeCoefficients (inc l) (ρ l) (sample v)).charpoly = (P v).map (emb l) := by
83   obtain ⟨ρ, hρ, hlocal, hpoly⟩ := common_spine_completion O K I C
84     (fun l => positive_finite_levels (I l) (C l) (finite l))
85     (fun l => (positive_levels_iff_all (I l) (C l)).mp (occupied l)) continuous
86     (fun l r => Local l (changeCoefficients (inc l) r)) stable inc emb sample good
87     P localP integrality spec
88   exact ⟨ρ, hρ, fun l => ⟨coefficient_change_continuous (I l) (inc l) (hinc l) (ρ l)
89     (hlocal l).1, (hlocal l).2⟩, hpoly⟩
90 
91 end PaperX.CompletionAssembly

Back to source controls