GaloisComparisonCompletion.lean

1 import PaperX.LocalComparisonCompletion
2 import Mathlib.FieldTheory.AbsoluteGaloisGroup
3 import Mathlib.NumberTheory.Padics.PadicNumbers
4 
5 /-! An actual arithmetic specialization: restrictions from the absolute Galois
6 group of Q to the absolute Galois groups of Q_p. The chosen maps are induced
7 by the actual field embeddings and choices of algebraic-closure embeddings.
8 Exact local Galois representation isomorphism is the conclusion; no Hodge--Tate
9 or Weil--Deligne interpretation is built into an arbitrary predicate. -/
10 set_option autoImplicit false
11 namespace PaperX.GaloisComparisonCompletion
12 open PaperX.RepresentationLimits PaperX.RepresentationTopology PaperX.RepresentationClasses
13 open PaperX.ClassCompletion PaperX.ComparisonCertificates
14 
15 /-- The actual continuous homomorphism induced by Q→Q_p. -/
16 noncomputable def localRestriction (p : ℕ) [Fact p.Prime] :
17     Field.absoluteGaloisGroup ℚ_[p] →ₜ* Field.absoluteGaloisGroup ℚ :=
18   Field.absoluteGaloisGroup.map (algebraMap ℚ ℚ_[p])
19 
20 /-- The actual local/global groups instantiate certificate completion. The
21 templates prescribe entire local actions, a stronger condition than a packet label.
22 Nonemptiness and the fixed determinant bounds are substantive explicit inputs. -/
23 theorem rational_galois_comparison_completion
24     {R K ι S : Type} [CommRing R] [Field K] [TopologicalSpace K]
25     [Fintype ι] [DecidableEq ι] [Finite S]
26     (p : S → ℕ) [∀ s, Fact (p s).Prime]
27     (I : Ideal R) [IsAdicComplete I R] (hI : I.FG) [Finite (R ⧸ I)]
28     (C : ClassConditions (G := Field.absoluteGaloisGroup ℚ) (ι := ι) I)
29     (τ : ∀ s, MatrixRep R (Field.absoluteGaloisGroup ℚ_[p s]) ι)
30     (d : S → ℕ)
31     (finiteC : ∀ k, 0 < k → Finite {c // C.allowed k c})
32     (occupied : ∀ k, 0 < k → Nonempty
33       (Node I (framed I C) (fun s => (localRestriction (p s)).toMonoidHom) τ d k))
34     (continuous : ∀ k c, C.allowed k c →
35       ∃ σ, classOf σ = c ∧ FiniteRepContinuous σ)
36     (inc : R →+* K) (hinj : Function.Injective inc)
37     (hinc : @Continuous R K I.adicTopology inferInstance inc) :
38     ∃ (ρ : MatrixRep R (Field.absoluteGaloisGroup ℚ) ι)
39       (P : S → Matrix ι ι R),
40       (∀ k, C.allowed k (classOf (reduce I ρ k))) ∧
41       Continuous (changeCoefficients inc ρ) ∧
42       ∀ s, ∃ u : (Matrix ι ι K)ˣ,
43         (u : Matrix ι ι K) = (P s).map inc ∧
44         conjugate u (changeCoefficients inc (τ s)) =
45           changeCoefficients inc (ρ.comp (localRestriction (p s)).toMonoidHom) :=
46   PaperX.LocalComparisonCompletion.unframed_comparison_completion I hI C
47     (fun s => (localRestriction (p s)).toMonoidHom) τ d finiteC occupied continuous
48     inc hinj hinc
49 
50 end PaperX.GaloisComparisonCompletion

Back to source controls