ConditionalCompletion.lean

1 import PaperXII.AdicLocalConditions
2 
3 /-! Exact conditional completion statement for the amended Paper XII 10.5.
4 All arithmetic existence, continuity, integrality, and finite local equations
5 are explicit inputs; the completion and quotient factors are constructed. -/
6 set_option autoImplicit false
7 namespace PaperXII.ConditionalCompletion
8 
9 open ContinuousMonoidHom Matrix
10 open AdicMatrixGroups AdicCompanions ContinuousClasses ClassCompanions AdicSpines
11 open AdicLocalConditions LocalQuotients PaperX.ClassInvariants
12 
13 variable {Γ ι : Type} [Group Γ] [TopologicalSpace Γ] [Fintype ι] [DecidableEq ι]
14 
15 /-- Positive finite class forests realize the prescribed common spine and every
16 declared polynomial quotient condition on the actual representation entries. -/
17 theorem simultaneous_companion_completion
18     {Λ Ω L V : Type} [Field L] (O K : Λ → Type)
19     [∀ l, CommRing (O l)] [∀ l, Field (K l)] [∀ l, TopologicalSpace (K l)]
20     (J : ∀ l, Ideal (O l)) [∀ l, IsAdicComplete (J l) (O l)]
21     (hJ : ∀ l, (J l).FG) [∀ l, Finite (O l ⧸ J l)]
22     (C : ∀ l n, LevelClass (Γ := Γ) (ι := ι) (J l) n → Prop)
23     (hC : ∀ l n c, C l (n + 1) c → C l n (classStep (J l) n c))
24     (finiteC : ∀ l n, 0 < n → Finite {c // C l n c})
25     (hc : ∀ l n, 0 < n → ∀ c, C l n c → ClassContinuous c)
26     (hne : ∀ l n, 0 < n → ∃ c, C l n c)
27     (root : ∀ l, LevelClass (Γ := Γ) (ι := ι) (J l) 1)
28     (hroot : ∀ l c, C l 1 c → c = root l)
29     (inc : ∀ l, O l →+* K l)
30     (hinc : ∀ l, @Continuous (O l) (K l) (J l).adicTopology inferInstance (inc l))
31     (emb : ∀ l, L →+* K l) (frob : Ω → Γ) (good : Λ → Ω → Prop)
32     (P : Ω → Polynomial L) (localP : ∀ l, Ω → Polynomial (O l))
33     (hmatch : ∀ l v, good l v → (localP l v).map (inc l) = (P v).map (emb l))
34     (hspec : ∀ l n, 0 < n → ∀ c, C l n c → ∀ v, good l v →
35       classCharpoly c (frob v) = (localP l v).map (quotientMap (J l) n))
36     (H : Λ → Subgroup Γ)
37     (hH : ∀ l n, 0 < n → ∀ c, C l n c → ClassTrivial (H l) c)
38     (relations : ∀ l, V → Ideal (MvPolynomial (Coordinates (Γ := Γ) (ι := ι)) (O l)))
39     (hrelations : ∀ l v n, 0 < n → ∀ σ, Framed (J l) (C l) n σ →
40       relations l v ≤ RingHom.ker (finitePoint (J l) n σ)) :
41     ∃ ρ : ∀ l, AdicRealization (J l) (Framed (J l) (C l)),
42       (∀ l, classOfRep (reduceRep (J l) 1 (ρ l).val) = root l) ∧
43       (∀ l v, good l v →
44         (fieldRep (J l) (inc l) (hinc l) (ρ l).val (frob v)).val.charpoly =
45           (P v).map (emb l)) ∧
46       (∀ l g, g ∈ H l → fieldRep (J l) (inc l) (hinc l) (ρ l).val g = 1) ∧
47       ∀ l v, Factors (relations l v) (point (J l) (ρ l).val) := by
48   obtain ⟨ρ, hrootρ, hpolyρ, hHρ⟩ := ClassSpines.simultaneous_class_spine
49     O K J hJ C hC finiteC hc hne root hroot inc hinc emb frob good P localP
50     hmatch hspec H hH
51   exact ⟨ρ, hrootρ, hpolyρ, hHρ, fun l v ↦
52     class_condition_preserved (J l) (C l) (relations l v) (ρ l) (hrelations l v)⟩
53 
54 end PaperXII.ConditionalCompletion

Back to source controls