CommonSpine.lean

1 import PaperX.SystemCompletion
2 
3 /-! Actual polynomial coefficients survive reconstruction and coefficient change.
4 The common coefficient field is not mapped into an integral DVR: local integral
5 polynomials and embeddings into local fields are supplied separately. Good-place
6 predicates are explicit and may depend on the coefficient index. No Chebotarev,
7 Galois realization, or Hodge--Tate theorem is introduced as an axiom. -/
8 set_option autoImplicit false
9 namespace PaperX.CommonSpine
10 open PaperX.RepresentationLimits PaperX.RepresentationTopology PaperX.RepresentationForests
11 open PaperX.SystemCompletion
12 variable {R G ι : Type*} [CommRing R] [Group G] [Fintype ι] [DecidableEq ι]
13 variable (I : Ideal R)
14 
15 /-- Separatedness alone identifies prescribed integral characteristic polynomials. -/
16 theorem charpoly_detected [IsHausdorff I R] (ρ : MatrixRep R G ι) (g : G)
17     (P : Polynomial R)
18     (h : ∀ k, (reduce I ρ k g).charpoly = P.map (Ideal.Quotient.mk (I^k))) :
19     (ρ g).charpoly = P := by
20   apply Polynomial.ext
21   intro n
22   apply scalar_ext I
23   intro k
24   have H : (Polynomial.map (Ideal.Quotient.mk (I^k)) (ρ g).charpoly).coeff n =
25       (P.map (Ideal.Quotient.mk (I^k))).coeff n := by
26     rw [← Matrix.charpoly_map]
27     exact congrArg (fun p : Polynomial (R ⧸ I^k) => p.coeff n) (h k)
28   simpa using H
29 
30 /-- Specifying Frobenius polynomials at all allowed reductions determines the
31 whole polynomial, rather than just the trace or a bounded coefficient sample. -/
32 theorem realization_has_spine {R G ι V : Type} [CommRing R] [Group G]
33     [Fintype ι] [DecidableEq ι] (I : Ideal R) [IsHausdorff I R]
34     (C : Conditions (G := G) (ι := ι) I) (ρ : MatrixRep R G ι) (hρ : Realizes I C ρ)
35     (sample : V → G) (good : V → Prop) (P : V → Polynomial R)
36     (spec : ∀ k τ, C.allowed k τ → ∀ v, good v →
37       (τ (sample v)).charpoly = (P v).map (Ideal.Quotient.mk (I^k))) :
38     ∀ v, good v → (ρ (sample v)).charpoly = P v := by
39   intro v hv
40   apply charpoly_detected I ρ (sample v) (P v)
41   intro k
42   exact spec k _ (hρ k) v hv
43 
44 /-- Base change realizes the common polynomial over the local field. -/
45 theorem polynomial_base_change {K E : Type*} [CommRing K] [CommRing E]
46     (inc : R →+* K) (emb : E →+* K) (ρ : MatrixRep R G ι) (g : G)
47     (localP : Polynomial R) (commonP : Polynomial E)
48     (hlocal : (ρ g).charpoly = localP)
49     (hcommon : localP.map inc = commonP.map emb) :
50     (changeCoefficients inc ρ g).charpoly = commonP.map emb := by
51   change ((ρ g).map inc).charpoly = _
52   rw [Matrix.charpoly_map, hlocal, hcommon]
53 
54 /-- Common-spine completion at the representation-and-polynomial level. Local
55 arithmetic conditions are only those justified by the supplied stability input.
56 All good-place restrictions, local integrality, and coefficient embeddings remain
57 visible hypotheses. This is not an unconditional strict compatibility theorem. -/
58 theorem common_spine_completion
59     {Λ G ι V E : Type} [Group G] [TopologicalSpace G] [Fintype ι] [DecidableEq ι]
60     [Field E] (O K : Λ → Type) [∀ l, CommRing (O l)] [∀ l, Field (K l)]
61     (I : (l : Λ) → Ideal (O l)) [∀ l, IsAdicComplete (I l) (O l)]
62     (C : (l : Λ) → Conditions (G := G) (ι := ι) (I l))
63     (finite : ∀ l k, Finite {ρ : MatrixRep (O l ⧸ (I l)^k) G ι // (C l).allowed k ρ})
64     (occupied : ∀ l k, ∃ ρ, (C l).allowed k ρ)
65     (continuous : ∀ l k ρ, (C l).allowed k ρ → FiniteRepContinuous ρ)
66     (Local : (l : Λ) → MatrixRep (O l) G ι → Prop)
67     (stable : ∀ l ρ, Realizes (I l) (C l) ρ → Local l ρ)
68     (inc : (l : Λ) → O l →+* K l) (emb : (l : Λ) → E →+* K l)
69     (sample : V → G) (good : Λ → V → Prop)
70     (P : V → Polynomial E) (localP : (l : Λ) → V → Polynomial (O l))
71     (integrality : ∀ l v, good l v → (localP l v).map (inc l) = (P v).map (emb l))
72     (spec : ∀ l k τ, (C l).allowed k τ → ∀ v, good l v →
73       (τ (sample v)).charpoly = (localP l v).map (Ideal.Quotient.mk ((I l)^k))) :
74     ∃ ρ : (l : Λ) → MatrixRep (O l) G ι,
75       SystemRealizes O I C ρ ∧
76       (∀ l, AdicRepContinuous (I l) (ρ l) ∧ Local l (ρ l)) ∧
77       ∀ l v, good l v →
78         (changeCoefficients (inc l) (ρ l) (sample v)).charpoly = (P v).map (emb l) := by
79   obtain ⟨ρ,hρ,hc⟩ := continuous_system_completion O I C finite occupied continuous Local stable
80   refine ⟨ρ,hρ,hc,?_⟩
81   intro l v hv
82   exact polynomial_base_change (inc l) (emb l) (ρ l) (sample v) (localP l v) (P v)
83     (realization_has_spine (I l) (C l) (ρ l) (hρ l) sample (good l) (localP l)
84       (spec l) v hv) (integrality l v hv)
85 
86 end PaperX.CommonSpine

Back to source controls