ConditionalArithmeticSpine.lean

1 import PaperX.DeterminantSpine
2 import PaperX.InverseLimitLocalConditions
3 
4 /-! The universal conditional implication of source Claim 8.2.
5 
6 The selected weight and packet relations are parameters, just as the source
7 quantifies over a chosen spine and assumes inverse-limit closure. They are not
8 definitions of Hodge--Tate or Weil--Deligne attachment. Instantiating such a
9 relation and proving its closure is an application premise, not a conclusion.
10 Determinants are coefficient-specific: no common E-valued character on G is
11 required. The shared polynomial data still live over E.
12 -/
13 set_option autoImplicit false
14 namespace PaperX.ConditionalArithmeticSpine
15 open PaperX.RepresentationLimits PaperX.RepresentationClasses
16 open PaperX.RepresentationTopology PaperX.ClassCompletion PaperX.ClassInvariants
17 open PaperX.ClassCommonSpine PaperX.InverseLimitLocalConditions
18 open PaperX.DeterminantSpine
19 
20 variable {Λ G ι V E : Type} [Group G] [Fintype ι] [DecidableEq ι] [Field E]
21 variable (K : Λ → Type) [∀ l, Field (K l)]
22 
23 /-- A precise interface for the source's chosen data. The relations retain their
24 supplied meaning; this structure neither constructs them nor declares them true.
25 Inactive places can be represented by implications inside the packet relation.
26 The determinant family may vary with the coefficient place. -/
27 structure Spine where
28   sample : V → G
29   good : Λ → V → Prop
30   good_cofinite : ∀ l, {v | ¬ good l v}.Finite
31   polynomial : V → Polynomial E
32   determinant : (l : Λ) → G → K l
33   Weight : Type
34   weights : Weight
35   hasWeights : (l : Λ) → Weight → MatrixRep (K l) G ι → Prop
36   PacketIndex : Type
37   Packet : PacketIndex → Type
38   packets : (j : PacketIndex) → Packet j
39   hasPacket : (l : Λ) → (j : PacketIndex) → Packet j → MatrixRep (K l) G ι → Prop
40 
41 variable {K}
42 
43 /-- Exactly the selected full local conditions, with the common labels visible. -/
44 def LocalRealizes (S : Spine (G := G) (ι := ι) (V := V) (E := E) K)
45     (l : Λ) (ρ : MatrixRep (K l) G ι) : Prop :=
46   S.hasWeights l S.weights ρ ∧ ∀ j, S.hasPacket l j (S.packets j) ρ
47 
48 /-- Realization of every item of the chosen spine. Continuity is a separate
49 conclusion of completion. This definition imposes no extra WD convention beyond
50 the supplied packet relation, and no semisimplicity beyond the selected data. -/
51 def RealizesSpine (S : Spine (G := G) (ι := ι) (V := V) (E := E) K)
52     (emb : (l : Λ) → E →+* K l) (ρ : (l : Λ) → MatrixRep (K l) G ι) : Prop :=
53   (∀ l v, S.good l v → (ρ l (S.sample v)).charpoly =
54     (S.polynomial v).map (emb l)) ∧
55   (∀ l g, (ρ l g).det = S.determinant l g) ∧
56   ∀ l, LocalRealizes S l (ρ l)
57 
58 /-- The good-place metadata in the chosen spine gives an actual almost-everywhere
59 common polynomial statement at every coefficient place. -/
60 theorem realizes_almost_everywhere
61     (S : Spine (G := G) (ι := ι) (V := V) (E := E) K)
62     (emb : (l : Λ) → E →+* K l) (ρ : (l : Λ) → MatrixRep (K l) G ι)
63     (h : RealizesSpine S emb ρ) (l : Λ) :
64     ∀ᶠ v in Filter.cofinite,
65       (ρ l (S.sample v)).charpoly = (S.polynomial v).map (emb l) := by
66   have hg : ∀ᶠ v in Filter.cofinite, S.good l v :=
67     Filter.mem_cofinite.mpr (S.good_cofinite l)
68   exact hg.mono (fun v hv => h.1 l v hv)
69 
70 /-- An integral realization supplies the actual branch promised in the source,
71 including its allowed objects and exact successive reductions. -/
72 def reductionBranch {R : Type} [CommRing R] (I : Ideal R)
73     (C : ClassConditions (G := G) (ι := ι) I) (ρ : MatrixRep R G ι)
74     (hρ : ∀ k, C.allowed k (classOf (reduce I ρ k))) :
75     PaperX.Compactness.Branch (PaperX.RepresentationForests.tower I (framed I C)) where
76   value k := ⟨reduce I ρ k, hρ k⟩
77   compatible k := Subtype.ext (transition_reduce I ρ (Nat.le_succ k))
78 
79 @[simp] theorem reductionBranch_value {R : Type} [CommRing R] (I : Ideal R)
80     (C : ClassConditions (G := G) (ι := ι) I) (ρ : MatrixRep R G ι)
81     (hρ : ∀ k, C.allowed k (classOf (reduce I ρ k))) (k : ℕ) :
82     ((reductionBranch I C ρ hρ).value k).val = reduce I ρ k := rfl
83 
84 variable [TopologicalSpace G] [∀ l, TopologicalSpace (K l)]
85 
86 /-- All four source ingredients are used: a specified spine and its reductions,
87 finite nonempty admissible levels, total compatible reduction maps (in C), and
88 inverse-limit closure of the selected full local conditions. Finite branching
89 requires no additional assumption because every level is finite.
90 
91 The complete coefficient rings and continuity of finite admissible objects are
92 the ambient representation setting. No coefficient-prime carrier, finite-level
93 liftability, arithmetic local closure, or coherent framing is concluded for free.
94 -/
95 theorem adelic_finite_depth_completion
96     (O : Λ → Type) [∀ l, CommRing (O l)]
97     (I : (l : Λ) → Ideal (O l)) [∀ l, IsAdicComplete (I l) (O l)]
98     (hI : ∀ l, (I l).FG) [∀ l, Finite (O l ⧸ I l)]
99     (C : (l : Λ) → ClassConditions (G := G) (ι := ι) (I l))
100     (finite : ∀ l k, 0 < k → Finite {c // (C l).allowed k c})
101     (occupied : ∀ l k, 0 < k → ∃ c, (C l).allowed k c)
102     (continuous : ∀ l k c, (C l).allowed k c →
103       ∃ ρ, classOf ρ = c ∧ FiniteRepContinuous ρ)
104     (inc : (l : Λ) → O l →+* K l)
105     (hinc : ∀ l, @Continuous (O l) (K l) (I l).adicTopology inferInstance (inc l))
106     (emb : (l : Λ) → E →+* K l)
107     (S : Spine (G := G) (ι := ι) (V := V) (E := E) K)
108     (closed : ∀ l, InverseLimitClosed (I l) (C l)
109       (fun ρ => LocalRealizes S l (changeCoefficients (inc l) ρ)))
110     (localP : (l : Λ) → V → Polynomial (O l))
111     (poly_integral : ∀ l v, S.good l v →
112       (localP l v).map (inc l) = (S.polynomial v).map (emb l))
113     (poly_spec : ∀ l k c, (C l).allowed k c → ∀ v, S.good l v →
114       classCharpoly c (S.sample v) = (localP l v).map (Ideal.Quotient.mk ((I l)^k)))
115     (localDet : (l : Λ) → G → O l)
116     (det_integral : ∀ l g, inc l (localDet l g) = S.determinant l g)
117     (det_spec : ∀ l k c, (C l).allowed k c → ∀ g,
118       classDet c g = Ideal.Quotient.mk ((I l)^k) (localDet l g)) :
119     ∃ ρ : (l : Λ) → MatrixRep (O l) G ι,
120       (∀ l k, (C l).allowed k (classOf (reduce (I l) (ρ l) k))) ∧
121       (∀ l, Continuous (changeCoefficients (inc l) (ρ l))) ∧
122       RealizesSpine S emb (fun l => changeCoefficients (inc l) (ρ l)) := by
123   obtain ⟨ρ, hρ, hl, hp⟩ := unframed_common_spine_completion O K I hI C
124     finite occupied continuous inc hinc emb (LocalRealizes S)
125     (fun l => (inverseLimitClosed_iff_realizations (I l) (C l) _).mp (closed l))
126     S.sample S.good S.polynomial localP poly_integral poly_spec
127   refine ⟨ρ, hρ, fun l => (hl l).1, hp, ?_, fun l => (hl l).2⟩
128   intro l g
129   rw [determinant_changeCoefficients,
130     class_realization_has_determinant (I l) (C l) (ρ l) (hρ l) (localDet l)
131       (det_spec l) g, det_integral]
132 
133 end PaperX.ConditionalArithmeticSpine

Back to source controls