AdicCompanions.lean

1 import PaperXII.AdicMatrixGroups
2 
3 /-! Continuous companion reconstruction into the actual adic matrix group.
4 Finite conditions are predicates on continuous quotient representations, and
5 the comparison with representations over the complete ring is constructed. -/
6 set_option autoImplicit false
7 namespace PaperXII.AdicCompanions
8 
9 open ContinuousMonoidHom Matrix AdicMatrixGroups
10 
11 variable {R Γ ι : Type} [CommRing R] [Group Γ] [TopologicalSpace Γ]
12     [Fintype ι] [DecidableEq ι] (I : Ideal R)
13 
14 /-- Continuous representations into GL over R with the specified I-adic topology. -/
15 abbrev AdicRep :=
16   let _ : TopologicalSpace R := I.adicTopology
17   Γ →ₜ* GL ι R
18 
19 /-- The actual finite reduction of a continuous adic representation. -/
20 def reduceRep (n : ℕ) (ρ : AdicRep (Γ := Γ) (ι := ι) I) : Γ →ₜ* GL ι (Coeff I n) := by
21   let _ : TopologicalSpace R := I.adicTopology
22   exact
23     { __ := (AdicMatrixGroups.reduce I n).comp ρ.toMonoidHom
24       continuous_toFun := (quotientMap_continuous I n).generalLinearGroup_map.comp ρ.continuous }
25 
26 /-- Integral realizations satisfying every declared finite condition. -/
27 def AdicRealization (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop) :=
28   {ρ : AdicRep (Γ := Γ) (ι := ι) I // ∀ n, A n (reduceRep I n ρ)}
29 
30 /-- Use the proved group homeomorphism to realize a completed branch over R. -/
31 noncomputable def realize [IsAdicComplete I R]
32     (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop)
33     (c : InverseLimitRepresentations.Complete (step I) A) : AdicRep (Γ := Γ) (ι := ι) I := by
34   let _ : TopologicalSpace R := I.adicTopology
35   exact
36     { __ := (lift I).comp c.val.toMonoidHom
37       continuous_toFun := (lift_continuous I).comp c.val.continuous }
38 
39 /-- Integral realization has exactly the finite reductions of the completed branch. -/
40 theorem realize_reduces [IsAdicComplete I R]
41     (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop)
42     (c : InverseLimitRepresentations.Complete (step I) A) (n : ℕ) :
43     reduceRep I n (realize I A c) =
44       (InverseLimitRepresentations.coordinate (G := fun n ↦ GL ι (Coeff I n))
45         (step (ι := ι) I) n).comp c.val := by
46   let _ : TopologicalSpace R := I.adicTopology
47   apply ContinuousMonoidHom.ext
48   intro g
49   exact reduce_lift I (c.val g) n
50 
51 /-- All finite admissibility predicates survive the actual adic reconstruction. -/
52 theorem realize_admissible [IsAdicComplete I R]
53     (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop)
54     (c : InverseLimitRepresentations.Complete (step I) A) (n : ℕ) :
55     A n (reduceRep I n (realize I A c)) := by
56   rw [realize_reduces]
57   exact c.property n
58 
59 /-- Reconstruction as a map to the actual integral realization space. -/
60 noncomputable def fromComplete [IsAdicComplete I R]
61     (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop)
62     (c : InverseLimitRepresentations.Complete (step I) A) : AdicRealization I A :=
63   ⟨realize I A c, realize_admissible I A c⟩
64 
65 /-- An integral realization determines its continuous representation in the limit group. -/
66 def toComplete (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop)
67     (ρ : AdicRealization I A) : InverseLimitRepresentations.Complete (step I) A := by
68   let _ : TopologicalSpace R := I.adicTopology
69   exact ⟨{ __ := (toLimit I).comp ρ.val.toMonoidHom
70            continuous_toFun := (toLimit_continuous I).comp ρ.val.continuous },
71     fun n ↦ ρ.property n⟩
72 
73 /-- Recovering the integral realization after reduction gives the original map. -/
74 theorem fromComplete_toComplete [IsAdicComplete I R]
75     (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop) (ρ : AdicRealization I A) :
76     fromComplete I A (toComplete I A ρ) = ρ := by
77   let _ : TopologicalSpace R := I.adicTopology
78   apply Subtype.ext
79   apply ContinuousMonoidHom.ext
80   intro g
81   exact lift_toLimit I (ρ.val g)
82 
83 /-- Reducing the integral reconstruction recovers the original completed branch. -/
84 theorem toComplete_fromComplete [IsAdicComplete I R]
85     (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop)
86     (c : InverseLimitRepresentations.Complete (step I) A) :
87     toComplete I A (fromComplete I A c) = c := by
88   let _ : TopologicalSpace R := I.adicTopology
89   apply Subtype.ext
90   apply ContinuousMonoidHom.ext
91   intro g
92   exact toLimit_lift I (c.val g)
93 
94 /-- The realization comparison is an actual equivalence, not an assumed effectivity map. -/
95 noncomputable def completionEquiv [IsAdicComplete I R]
96     (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop) :
97     InverseLimitRepresentations.Complete (step I) A ≃ AdicRealization I A where
98   toFun := fromComplete I A
99   invFun := toComplete I A
100   left_inv := toComplete_fromComplete I A
101   right_inv := fromComplete_toComplete I A
102 
103 /-- Finite occupied forests of continuous matrix representations have actual adic realizations. -/
104 theorem exists_adic_realization [IsAdicComplete I R]
105     (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop)
106     (hA : ∀ n ρ, A (n + 1) ρ → A n ((step I n).comp ρ))
107     [∀ n, Finite {ρ : Γ →ₜ* GL ι (Coeff I n) // A n ρ}]
108     (hne : ∀ n, Nonempty {ρ : Γ →ₜ* GL ι (Coeff I n) // A n ρ}) :
109     Nonempty (AdicRealization I A) := by
110   obtain ⟨c⟩ := InverseLimitRepresentations.exists_complete (step I) A hA hne
111   exact ⟨fromComplete I A c⟩
112 
113 /-- The residual representation is retained at the first positive precision. -/
114 theorem exists_adic_realization_with_root [IsAdicComplete I R]
115     (A : ∀ n, (Γ →ₜ* GL ι (Coeff I n)) → Prop)
116     (hA : ∀ n ρ, A (n + 1) ρ → A n ((step I n).comp ρ))
117     [∀ n, Finite {ρ : Γ →ₜ* GL ι (Coeff I n) // A n ρ}]
118     (hne : ∀ n, Nonempty {ρ : Γ →ₜ* GL ι (Coeff I n) // A n ρ})
119     (root : Γ →ₜ* GL ι (Coeff I 1)) (hroot : ∀ ρ, A 1 ρ → ρ = root) :
120     ∃ ρ : AdicRealization I A, reduceRep I 1 ρ.val = root := by
121   obtain ⟨ρ⟩ := exists_adic_realization I A hA hne
122   exact ⟨ρ, hroot _ (ρ.property 1)⟩
123 
124 /-- Separatedness alone determines an integral representation from all its finite reductions. -/
125 theorem adicRep_ext [IsHausdorff I R] (ρ σ : AdicRep (Γ := Γ) (ι := ι) I)
126     (h : ∀ n, reduceRep I n ρ = reduceRep I n σ) : ρ = σ := by
127   let _ : TopologicalSpace R := I.adicTopology
128   apply ContinuousMonoidHom.ext
129   intro g
130   apply ext_of_reductions I
131   intro n
132   exact DFunLike.congr_fun (h n) g
133 
134 end PaperXII.AdicCompanions

Back to source controls