ClassCommonSpine.lean

1 import PaperX.ClassCompletion
2 import PaperX.ClassInvariants
3 
4 /-! The full conditional common-spine completion interface on unframed levels.
5 The local closure input remains a stated hypothesis; no arithmetic invariant is
6 silently defined to be this predicate. -/
7 set_option autoImplicit false
8 namespace PaperX.ClassCommonSpine
9 open PaperX.RepresentationLimits PaperX.RepresentationTopology PaperX.RepresentationClasses
10 open PaperX.RepresentationForests PaperX.ClassCompletion PaperX.ClassInvariants
11 open PaperX.CompletionAssembly PaperX.SystemCompletion
12 
13 /-- A class with one continuous representative has all its frames continuous. -/
14 theorem all_frames_continuous {R G ι : Type} [CommRing R] [Group G]
15     [TopologicalSpace G] [Fintype ι] [DecidableEq ι]
16     (c : ClassRep R G ι) (h : ∃ σ, classOf σ = c ∧ FiniteRepContinuous σ)
17     (ρ : MatrixRep R G ι) (hρ : classOf ρ = c) : FiniteRepContinuous ρ := by
18   obtain ⟨σ, hσ, hc⟩ := h
19   exact finiteContinuous_of_classOf_eq (hρ.trans hσ.symm) hc
20 
21 /-- An actual continuous integral representation realizes all admissible classes. -/
22 theorem continuous_class_completion {R G ι : Type} [CommRing R] [Group G]
23     [TopologicalSpace G] [Fintype ι] [DecidableEq ι]
24     (I : Ideal R) [IsAdicComplete I R]
25     (C : ClassConditions (G := G) (ι := ι) I)
26     (finiteR : ∀ k, Finite (R ⧸ I^k))
27     (finiteC : ∀ k, 0 < k → Finite {c // C.allowed k c})
28     (occupied : ∀ k, 0 < k → ∃ c, C.allowed k c)
29     (continuous : ∀ k c, C.allowed k c → ∃ ρ, classOf ρ = c ∧ FiniteRepContinuous ρ) :
30     ∃ ρ : MatrixRep R G ι,
31       (∀ k, C.allowed k (classOf (reduce I ρ k))) ∧ AdicRepContinuous I ρ := by
32   apply exists_continuous_realization I (framed I C)
33   · apply positive_finite_levels
34     intro k hk
35     let : Finite (R ⧸ I^k) := finiteR k
36     let : Finite {c // C.allowed k c} := finiteC k hk
37     exact framed_finite I C k
38   · apply (positive_levels_iff_all I (framed I C)).mp
39     intro k hk
40     exact (framed_nonempty_iff I C k).mpr (occupied k hk)
41   · intro k ρ hρ
42     exact all_frames_continuous (classOf ρ) (continuous k _ hρ) ρ rfl
43 
44 /-- Positive finite unframed levels over finite-residue complete coefficient
45 rings give continuous realizations with the whole common polynomial spine and
46 the explicitly supplied inverse-limit-closed local conditions. -/
47 theorem unframed_common_spine_completion
48     {Λ G ι V E : Type} [Group G] [TopologicalSpace G] [Fintype ι] [DecidableEq ι]
49     [Field E] (O K : Λ → Type) [∀ l, CommRing (O l)] [∀ l, Field (K l)]
50     [∀ l, TopologicalSpace (K l)]
51     (I : (l : Λ) → Ideal (O l)) [∀ l, IsAdicComplete (I l) (O l)]
52     (hI : ∀ l, (I l).FG) [∀ l, Finite (O l ⧸ I l)]
53     (C : (l : Λ) → ClassConditions (G := G) (ι := ι) (I l))
54     (finite : ∀ l k, 0 < k → Finite {c // (C l).allowed k c})
55     (occupied : ∀ l k, 0 < k → ∃ c, (C l).allowed k c)
56     (continuous : ∀ l k c, (C l).allowed k c →
57       ∃ ρ, classOf ρ = c ∧ FiniteRepContinuous ρ)
58     (inc : (l : Λ) → O l →+* K l)
59     (hinc : ∀ l, @Continuous (O l) (K l) (I l).adicTopology inferInstance (inc l))
60     (emb : (l : Λ) → E →+* K l)
61     (Local : (l : Λ) → MatrixRep (K l) G ι → Prop)
62     (stable : ∀ l ρ, (∀ k, (C l).allowed k (classOf (reduce (I l) ρ k))) →
63       Local l (changeCoefficients (inc l) ρ))
64     (sample : V → G) (good : Λ → V → Prop)
65     (P : V → Polynomial E) (localP : (l : Λ) → V → Polynomial (O l))
66     (integrality : ∀ l v, good l v → (localP l v).map (inc l) = (P v).map (emb l))
67     (spec : ∀ l k c, (C l).allowed k c → ∀ v, good l v →
68       classCharpoly c (sample v) = (localP l v).map (Ideal.Quotient.mk ((I l)^k))) :
69     ∃ ρ : (l : Λ) → MatrixRep (O l) G ι,
70       (∀ l k, (C l).allowed k (classOf (reduce (I l) (ρ l) k))) ∧
71       (∀ l, Continuous (changeCoefficients (inc l) (ρ l)) ∧
72         Local l (changeCoefficients (inc l) (ρ l))) ∧
73       ∀ l v, good l v →
74         (changeCoefficients (inc l) (ρ l) (sample v)).charpoly = (P v).map (emb l) := by
75   apply conditional_common_spine_completion O K I (fun l => framed (I l) (C l))
76     ?_ ?_ ?_ inc hinc emb Local stable sample good P localP integrality ?_
77   · intro l k hk
78     let : Finite (O l ⧸ (I l)^k) := finite_coefficients (I l) (hI l) k
79     let : Finite {c // (C l).allowed k c} := finite l k hk
80     exact framed_finite (I l) (C l) k
81   · intro l k hk
82     exact (framed_nonempty_iff (I l) (C l) k).mpr (occupied l k hk)
83   · intro l k ρ hρ
84     exact all_frames_continuous (classOf ρ) (continuous l k _ hρ) ρ rfl
85   · intro l k ρ hρ v hv
86     exact spec l k (classOf ρ) hρ v hv
87 
88 end PaperX.ClassCommonSpine

Back to source controls