InverseLimitRepresentations.lean

1 import PaperXII.CompanionForests
2 import Mathlib.Topology.Algebra.ContinuousMonoidHom
3 import Mathlib.Topology.Algebra.Group.Subgroup
4 
5 /-! Concrete effectivity for compatible continuous representations.
6 Targets are actual inverse-limit groups with the subspace topology of the product.
7 Admissibility consists of specified finite-level predicates preserved by reduction.
8 This does not identify the limit with a particular adic matrix group or establish
9 arithmetic local conditions that have no supplied finite-level description. -/
10 set_option autoImplicit false
11 namespace PaperXII.InverseLimitRepresentations
12 
13 open ContinuousMonoidHom PaperX.Compactness
14 
15 variable {Γ : Type} [Group Γ] [TopologicalSpace Γ]
16     {G : ℕ → Type} [∀ n, Group (G n)] [∀ n, TopologicalSpace (G n)]
17 
18 /-- The actual subgroup of compatible tuples, with its inherited product-subspace topology. -/
19 def limit (q : ∀ n, G (n + 1) →ₜ* G n) : Subgroup (∀ n, G n) where
20   carrier := {x | ∀ n, q n (x (n + 1)) = x n}
21   one_mem' := by intro n; exact map_one (q n)
22   mul_mem' := by
23     intro x y hx hy n
24     change q n (x (n + 1) * y (n + 1)) = x n * y n
25     rw [map_mul, hx n, hy n]
26   inv_mem' := by
27     intro x hx n
28     change q n (x (n + 1))⁻¹ = (x n)⁻¹
29     rw [map_inv, hx n]
30 
31 /-- Continuous projection from the actual limit group. -/
32 def coordinate (q : ∀ n, G (n + 1) →ₜ* G n) (n : ℕ) : limit q →ₜ* G n where
33   toFun x := x.val n
34   map_one' := rfl
35   map_mul' _ _ := rfl
36   continuous_toFun := (continuous_apply n).comp continuous_subtype_val
37 
38 /-- Assemble a compatible family of continuous representations into one continuous representation. -/
39 def assemble (q : ∀ n, G (n + 1) →ₜ* G n) (ρ : ∀ n, Γ →ₜ* G n)
40     (hρ : ∀ n, (q n).comp (ρ (n + 1)) = ρ n) : Γ →ₜ* limit q where
41   toFun g := ⟨fun n ↦ ρ n g, fun n ↦ DFunLike.congr_fun (hρ n) g⟩
42   map_one' := by apply Subtype.ext; funext n; exact map_one (ρ n)
43   map_mul' g h := by apply Subtype.ext; funext n; exact map_mul (ρ n) g h
44   continuous_toFun := (continuous_pi (fun n ↦ (ρ n).continuous)).subtype_mk _
45 
46 /-- Reconstructed representations have exactly the supplied finite reductions. -/
47 theorem coordinate_assemble (q : ∀ n, G (n + 1) →ₜ* G n) (ρ : ∀ n, Γ →ₜ* G n)
48     (hρ : ∀ n, (q n).comp (ρ (n + 1)) = ρ n) (n : ℕ) :
49     (coordinate q n).comp (assemble q ρ hρ) = ρ n := by
50   ext g
51   rfl
52 
53 /-- Agreement of all reductions determines the entire continuous representation. -/
54 theorem ext_of_coordinates (q : ∀ n, G (n + 1) →ₜ* G n)
55     (ρ σ : Γ →ₜ* limit q)
56     (h : ∀ n, (coordinate q n).comp ρ = (coordinate q n).comp σ) : ρ = σ := by
57   apply ContinuousMonoidHom.ext
58   intro g
59   apply Subtype.ext
60   funext n
61   exact DFunLike.congr_fun (h n) g
62 
63 /-- The forest consists of actual admissible continuous finite-level representations. -/
64 def forest (q : ∀ n, G (n + 1) →ₜ* G n) (A : ∀ n, (Γ →ₜ* G n) → Prop)
65     (hA : ∀ n ρ, A (n + 1) ρ → A n ((q n).comp ρ)) : Tower where
66   Level n := {ρ : Γ →ₜ* G n // A n ρ}
67   parent n ρ := ⟨(q n).comp ρ.val, hA n ρ.val ρ.property⟩
68 
69 /-- Complete realizations are continuous representations satisfying every finite admissibility condition. -/
70 def Complete (q : ∀ n, G (n + 1) →ₜ* G n) (A : ∀ n, (Γ →ₜ* G n) → Prop) :=
71   {ρ : Γ →ₜ* limit q // ∀ n, A n ((coordinate q n).comp ρ)}
72 
73 /-- A complete realization reduces to a branch of its declared admissible forest. -/
74 def toBranch (q : ∀ n, G (n + 1) →ₜ* G n) (A : ∀ n, (Γ →ₜ* G n) → Prop)
75     (hA : ∀ n ρ, A (n + 1) ρ → A n ((q n).comp ρ))
76     (ρ : Complete q A) : Branch (forest q A hA) where
77   value n := ⟨(coordinate q n).comp ρ.val, ρ.property n⟩
78   compatible n := by
79     apply Subtype.ext
80     ext g
81     exact (ρ.val g).property n
82 
83 /-- A branch reconstructs an actual continuous representation satisfying all finite conditions. -/
84 def fromBranch (q : ∀ n, G (n + 1) →ₜ* G n) (A : ∀ n, (Γ →ₜ* G n) → Prop)
85     (hA : ∀ n ρ, A (n + 1) ρ → A n ((q n).comp ρ))
86     (b : Branch (forest q A hA)) : Complete q A :=
87   ⟨assemble q (fun n ↦ (b.value n).val)
88     (fun n ↦ congrArg Subtype.val (b.compatible n)), fun n ↦ by
89       change A n (b.value n).val
90       exact (b.value n).property⟩
91 
92 /-- Reduction and reconstruction are inverse on complete representations. -/
93 theorem fromBranch_toBranch (q : ∀ n, G (n + 1) →ₜ* G n) (A : ∀ n, (Γ →ₜ* G n) → Prop)
94     (hA : ∀ n ρ, A (n + 1) ρ → A n ((q n).comp ρ)) (ρ : Complete q A) :
95     fromBranch q A hA (toBranch q A hA ρ) = ρ := by
96   apply Subtype.ext
97   apply ext_of_coordinates q
98   intro n
99   rfl
100 
101 /-- Reconstruction and reduction are inverse on branches. -/
102 theorem toBranch_fromBranch (q : ∀ n, G (n + 1) →ₜ* G n) (A : ∀ n, (Γ →ₜ* G n) → Prop)
103     (hA : ∀ n ρ, A (n + 1) ρ → A n ((q n).comp ρ)) (b : Branch (forest q A hA)) :
104     toBranch q A hA (fromBranch q A hA b) = b := by
105   apply CompanionForests.branch_ext
106   intro n
107   apply Subtype.ext
108   ext g
109   rfl
110 
111 /-- The effectivity equivalence is constructed, not assumed as an interface field. -/
112 def realizationEquiv (q : ∀ n, G (n + 1) →ₜ* G n) (A : ∀ n, (Γ →ₜ* G n) → Prop)
113     (hA : ∀ n ρ, A (n + 1) ρ → A n ((q n).comp ρ)) :
114     Complete q A ≃ Branch (forest q A hA) where
115   toFun := toBranch q A hA
116   invFun := fromBranch q A hA
117   left_inv := fromBranch_toBranch q A hA
118   right_inv := toBranch_fromBranch q A hA
119 
120 /-- Finite nonempty admissible levels yield an actual continuous limit representation. -/
121 theorem exists_complete (q : ∀ n, G (n + 1) →ₜ* G n) (A : ∀ n, (Γ →ₜ* G n) → Prop)
122     (hA : ∀ n ρ, A (n + 1) ρ → A n ((q n).comp ρ))
123     [∀ n, Finite {ρ : Γ →ₜ* G n // A n ρ}]
124     (hne : ∀ n, Nonempty {ρ : Γ →ₜ* G n // A n ρ}) : Nonempty (Complete q A) := by
125   let _ : ∀ n, Finite ((forest q A hA).Level n) := fun n ↦ inferInstanceAs
126     (Finite {ρ : Γ →ₜ* G n // A n ρ})
127   obtain ⟨b⟩ := CompanionForests.branch_exists (forest q A hA) hne
128   exact ⟨fromBranch q A hA b⟩
129 
130 /-- The constructed representation retains a declared fixed residual representation. -/
131 theorem exists_complete_with_root (q : ∀ n, G (n + 1) →ₜ* G n)
132     (A : ∀ n, (Γ →ₜ* G n) → Prop)
133     (hA : ∀ n ρ, A (n + 1) ρ → A n ((q n).comp ρ))
134     [∀ n, Finite {ρ : Γ →ₜ* G n // A n ρ}]
135     (hne : ∀ n, Nonempty {ρ : Γ →ₜ* G n // A n ρ})
136     (root : Γ →ₜ* G 0) (hroot : ∀ ρ, A 0 ρ → ρ = root) :
137     ∃ ρ : Complete q A, (coordinate q 0).comp ρ.val = root := by
138   obtain ⟨ρ⟩ := exists_complete q A hA hne
139   exact ⟨ρ, hroot _ (ρ.property 0)⟩
140 
141 /-- Claim 10.4 for the concrete realization model: an empty level rules out completion. -/
142 theorem empty_level_no_complete (q : ∀ n, G (n + 1) →ₜ* G n)
143     (A : ∀ n, (Γ →ₜ* G n) → Prop) (n : ℕ)
144     (h : ¬ Nonempty {ρ : Γ →ₜ* G n // A n ρ}) : ¬ Nonempty (Complete q A) := by
145   rintro ⟨ρ⟩
146   exact h ⟨⟨(coordinate q n).comp ρ.val, ρ.property n⟩⟩
147 
148 /-- All declared finite Frobenius labels survive reconstruction. -/
149 theorem finite_labels_preserved (q : ∀ n, G (n + 1) →ₜ* G n)
150     (A : ∀ n, (Γ →ₜ* G n) → Prop) (ρ : Complete q A)
151     {Ω : Type*} {L : ℕ → Type*} (frob : Ω → Γ)
152     (label : ∀ n, G n → L n) (spine : ∀ n, Ω → L n)
153     (hlabel : ∀ n σ, A n σ → ∀ v, label n (σ (frob v)) = spine n v) :
154     ∀ n v, label n ((ρ.val (frob v)).val n) = spine n v := by
155   intro n v
156   exact hlabel n ((coordinate q n).comp ρ.val) (ρ.property n) v
157 
158 /-- Simultaneous concrete reconstruction with coefficient groups varying across the index set. -/
159 theorem simultaneous_complete {I : Type} (H : I → ℕ → Type)
160     [∀ i n, Group (H i n)] [∀ i n, TopologicalSpace (H i n)]
161     (q : ∀ i n, H i (n + 1) →ₜ* H i n) (A : ∀ i n, (Γ →ₜ* H i n) → Prop)
162     (hA : ∀ i n ρ, A i (n + 1) ρ → A i n ((q i n).comp ρ))
163     [∀ i n, Finite {ρ : Γ →ₜ* H i n // A i n ρ}]
164     (hne : ∀ i n, Nonempty {ρ : Γ →ₜ* H i n // A i n ρ}) :
165     Nonempty (∀ i, Complete (q i) (A i)) := by
166   classical
167   exact ⟨fun i ↦ Classical.choice (exists_complete (q i) (A i) (hA i) (hne i))⟩
168 
169 end PaperXII.InverseLimitRepresentations

Back to source controls