AdicSpines.lean

1 import PaperXII.AdicCompanions
2 
3 /-! Integral Frobenius polynomials and unramifiedness survive actual adic reconstruction.
4 Common coefficient fields map to local fields. Integral lifts of the common
5 polynomials are supplied separately; no field is mapped into a valuation ring. -/
6 set_option autoImplicit false
7 namespace PaperXII.AdicSpines
8 
9 open ContinuousMonoidHom Matrix AdicMatrixGroups AdicCompanions
10 
11 variable {R Γ ι : Type} [CommRing R] [Group Γ] [TopologicalSpace Γ]
12     [Fintype ι] [DecidableEq ι] (I : Ideal R)
13 
14 /-- Equality of every reduced characteristic polynomial determines the entire integral polynomial. -/
15 theorem charpoly_detected [IsHausdorff I R] (B : GL ι R) (P : Polynomial R)
16     (h : ∀ n, (AdicMatrixGroups.reduce I n B).val.charpoly = P.map (quotientMap I n)) :
17     B.val.charpoly = P := by
18   apply Polynomial.ext
19   intro k
20   apply PaperX.RepresentationLimits.scalar_ext I
21   intro n
22   have hn := congrArg (fun f : Polynomial (Coeff I n) ↦ f.coeff k) (h n)
23   change ((B.val.map (Ideal.Quotient.mk (I ^ n))).charpoly).coeff k =
24     (P.map (Ideal.Quotient.mk (I ^ n))).coeff k at hn
25   simpa only [Matrix.charpoly_map, Polynomial.coeff_map] using hn
26 
27 /-- Every prescribed integral Frobenius polynomial survives, at every declared good place. -/
28 theorem spine_preserved [IsHausdorff I R]
29     (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop) (ρ : AdicRealization I A)
30     {Ω : Type*} (frob : Ω → Γ) (good : Ω → Prop) (P : Ω → Polynomial R)
31     (hspec : ∀ n σ, A n σ → ∀ v, good v →
32       (σ (frob v)).val.charpoly = (P v).map (quotientMap I n)) :
33     ∀ v, good v → (ρ.val (frob v)).val.charpoly = P v := by
34   intro v hv
35   apply charpoly_detected I
36   intro n
37   exact hspec n (reduceRep I n ρ.val) (ρ.property n) v hv
38 
39 /-- A supplied inertia subgroup acts trivially on the lift if it does so at every finite level. -/
40 theorem unramified_preserved [IsHausdorff I R]
41     (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop) (ρ : AdicRealization I A)
42     (H : Subgroup Γ)
43     (hspec : ∀ n σ, A n σ → ∀ g, g ∈ H → σ g = 1) :
44     ∀ g, g ∈ H → ρ.val g = 1 := by
45   intro g hg
46   apply ext_of_reductions I
47   intro n
48   rw [map_one]
49   exact hspec n (reduceRep I n ρ.val) (ρ.property n) g hg
50 
51 /-- Actual continuous coefficient change to the declared local field or topological coefficient ring. -/
52 def fieldRep {K : Type*} [CommRing K] [TopologicalSpace K]
53     (inc : R →+* K) (hinc : @Continuous R K I.adicTopology inferInstance inc)
54     (ρ : AdicRep (Γ := Γ) (ι := ι) I) : Γ →ₜ* GL ι K := by
55   let _ : TopologicalSpace R := I.adicTopology
56   exact
57     { __ := (GeneralLinearGroup.map inc).comp ρ.toMonoidHom
58       continuous_toFun := hinc.generalLinearGroup_map.comp ρ.continuous }
59 
60 /-- The local integral polynomial gives the exact common-field polynomial after coefficient change. -/
61 theorem fieldRep_charpoly {K L : Type*} [CommRing K] [TopologicalSpace K] [CommRing L]
62     (inc : R →+* K) (hinc : @Continuous R K I.adicTopology inferInstance inc)
63     (emb : L →+* K) (ρ : AdicRep (Γ := Γ) (ι := ι) I) (g : Γ)
64     (localP : Polynomial R) (commonP : Polynomial L)
65     (hlocal : (ρ g).val.charpoly = localP)
66     (hmatch : localP.map inc = commonP.map emb) :
67     (fieldRep I inc hinc ρ g).val.charpoly = commonP.map emb := by
68   let _ : TopologicalSpace R := I.adicTopology
69   change ((ρ g).val.map inc).charpoly = _
70   rw [Matrix.charpoly_map, hlocal, hmatch]
71 
72 /-- Unramifiedness survives actual coefficient change as well. -/
73 theorem fieldRep_unramified {K : Type*} [CommRing K] [TopologicalSpace K]
74     (inc : R →+* K) (hinc : @Continuous R K I.adicTopology inferInstance inc)
75     (ρ : AdicRep (Γ := Γ) (ι := ι) I) (H : Subgroup Γ)
76     (hρ : ∀ g, g ∈ H → ρ g = 1) : ∀ g, g ∈ H → fieldRep I inc hinc ρ g = 1 := by
77   let _ : TopologicalSpace R := I.adicTopology
78   intro g hg
79   change GeneralLinearGroup.map inc (ρ g) = 1
80   rw [hρ g hg, map_one]
81 
82 /-- Simultaneous actual adic realizations with a common algebraic Frobenius spine.
83 Local integrality, finite occupancy, and reduction stability remain explicit inputs. -/
84 theorem simultaneous_common_spine
85     {Λ Ω L : Type} [Field L] (O K : Λ → Type)
86     [∀ l, CommRing (O l)] [∀ l, Field (K l)] [∀ l, TopologicalSpace (K l)]
87     (J : ∀ l, Ideal (O l)) [∀ l, IsAdicComplete (J l) (O l)]
88     (A : ∀ l n, (Γ →ₜ* GL ι (Coeff (J l) n)) → Prop)
89     (hA : ∀ l n σ, A l (n + 1) σ → A l n ((step (J l) n).comp σ))
90     [∀ l n, Finite {σ : Γ →ₜ* GL ι (Coeff (J l) n) // A l n σ}]
91     (hne : ∀ l n, Nonempty {σ : Γ →ₜ* GL ι (Coeff (J l) n) // A l n σ})
92     (inc : ∀ l, O l →+* K l)
93     (hinc : ∀ l, @Continuous (O l) (K l) (J l).adicTopology inferInstance (inc l))
94     (emb : ∀ l, L →+* K l) (frob : Ω → Γ) (good : Λ → Ω → Prop)
95     (P : Ω → Polynomial L) (localP : ∀ l, Ω → Polynomial (O l))
96     (hmatch : ∀ l v, good l v → (localP l v).map (inc l) = (P v).map (emb l))
97     (hspec : ∀ l n σ, A l n σ → ∀ v, good l v →
98       (σ (frob v)).val.charpoly = (localP l v).map (quotientMap (J l) n)) :
99     ∃ ρ : ∀ l, AdicRealization (J l) (A l), ∀ l v, good l v →
100       (fieldRep (J l) (inc l) (hinc l) (ρ l).val (frob v)).val.charpoly =
101         (P v).map (emb l) := by
102   classical
103   let ρ : ∀ l, AdicRealization (J l) (A l) :=
104     fun l ↦ Classical.choice (exists_adic_realization (J l) (A l) (hA l) (hne l))
105   refine ⟨ρ, ?_⟩
106   intro l v hv
107   exact fieldRep_charpoly (J l) (inc l) (hinc l) (emb l) (ρ l).val (frob v)
108     (localP l v) (P v)
109     (spine_preserved (J l) (A l) (ρ l) frob (good l) (localP l) (hspec l) v hv)
110     (hmatch l v hv)
111 
112 end PaperXII.AdicSpines

Back to source controls