CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteQuotients.lean
1import CompletedGroupAlgebra.OpenFiniteQuotientTopology.FiniteQuotients
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteQuotients.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Completed group algebras
14The completed group algebra is presented as an inverse limit of finite group algebras, together with canonical augmentation, augmentation ideal, finite-stage maps, functoriality, and profinite module universal properties.
15-/
16open scoped Topology
18namespace CompletedGroupAlgebra
20noncomputable section
22open ProCGroups
23open ProCGroups.ProC
24open ProCGroups.InverseSystems
25open ProCGroups.Completion
27universe u v w
29variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
31variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
33/-- Open coefficient ideals used in the RZ §5.3 kernel-neighborhood topology. -/
35 (R : Type u) [CommRing R] [TopologicalSpace R] : Type u :=
36 {I : Ideal R // IsOpen (I : Set R)}
38omit G [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [IsTopologicalRing R] in
39/-- In a profinite coefficient ring, the open-ideal quotients separate points. This is the
40coefficient part of Lemma 5.3.5(a)'s kernel-intersection statement. -/
42 (hR : IsProfiniteRing R) {r : R}
43 (hr : ∀ I : CompletedGroupAlgebraOpenIdeal R, Ideal.Quotient.mk I.1 r = 0) :
44 r = 0 := by
45 by_contra hne
46 letI : T2Space R := hR.2.2.1
47 letI : T1Space R := inferInstance
48 have h0 : (0 : R) ∈ ({r}ᶜ : Set R) := by
49 exact fun h0r => hne h0r.symm
50 have hU : ({r}ᶜ : Set R) ∈ 𝓝 (0 : R) :=
51 isOpen_compl_singleton.mem_nhds h0
52 rcases profiniteRing_hasOpenIdealBasisAtZero R hR ({r}ᶜ) hU with
53 ⟨I, hIopen, hIU⟩
54 have hrI : r ∈ I := by
55 exact Ideal.Quotient.eq_zero_iff_mem.1 (hr ⟨I, hIopen⟩)
56 exact (hIU hrI) rfl
58/-- The two-parameter index set for the kernel-neighborhood quotients `(R/I)[G/U]`, with open
61 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
62 [TopologicalSpace G] : Type (max u v) :=
63 OrderDual (CompletedGroupAlgebraOpenIdeal R) × CompletedGroupAlgebraIndex G
66 (R : Type u) [CommRing R] [TopologicalSpace R] :
67 Nonempty (CompletedGroupAlgebraOpenIdeal R) :=
68 ⟨⟨⊤, isOpen_univ⟩⟩
71 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
72 [TopologicalSpace G] [IsTopologicalGroup G] :
73 Directed (α := CompletedGroupAlgebraOpenQuotientIndex R G) (· ≤ ·) fun K => K := by
74 intro K L
76 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) ProCGroups.FiniteGroupClass.allFinite_formation
77 K.2 L.2 with
78 ⟨W, hKW, hLW⟩
79 let I : CompletedGroupAlgebraOpenIdeal R :=
80 ⟨(OrderDual.ofDual K.1).1 ⊓ (OrderDual.ofDual L.1).1, by
81 simpa using (OrderDual.ofDual K.1).2.inter (OrderDual.ofDual L.1).2⟩
82 refine ⟨(OrderDual.toDual I, W), ?_, ?_⟩
83 · constructor
84 · change (I.1 : Ideal R) ≤ (OrderDual.ofDual K.1).1
85 exact inf_le_left
86 · exact hKW
87 · constructor
88 · change (I.1 : Ideal R) ≤ (OrderDual.ofDual L.1).1
89 exact inf_le_right
90 · exact hLW
92/-- The stage `(R/I)[G/U]` attached to an open-ideal/finite-group quotient index. -/
94 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
95 [TopologicalSpace G] [IsTopologicalGroup G]
96 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
97 Type (max u v) :=
98 CompletedGroupAlgebraCoeffQuotientStage R G ((OrderDual.ofDual K.1).1 : Ideal R) K.2
100/-- The quotient map `[R G] -> (R/I)[G/U]` for an open-ideal/finite-group quotient index. -/
102 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
103 [TopologicalSpace G] [IsTopologicalGroup G]
104 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
105 MonoidAlgebra R G →+* CompletedGroupAlgebraOpenFiniteQuotientStage R G K :=
106 groupAlgebraFiniteQuotientMap R G ((OrderDual.ofDual K.1).1 : Ideal R) K.2
108/-- The kernel neighborhood attached to an open-ideal/finite-group quotient index. -/
110 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
111 [TopologicalSpace G] [IsTopologicalGroup G]
112 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
113 Ideal (MonoidAlgebra R G) :=
114 groupAlgebraFiniteQuotientKernel R G ((OrderDual.ofDual K.1).1 : Ideal R) K.2
116@[simp]
118 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
119 [TopologicalSpace G] [IsTopologicalGroup G]
120 (K : CompletedGroupAlgebraOpenQuotientIndex R G) (x : MonoidAlgebra R G) :
121 x ∈ groupAlgebraOpenFiniteQuotientKernel R G K ↔
122 groupAlgebraOpenFiniteQuotientMap R G K x = 0 :=
123 Iff.rfl
125/-- The transition `(R/I_L)[G/U_L] -> (R/I_K)[G/U_K]` for `K ≤ L`. -/
127 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
128 [TopologicalSpace G] [IsTopologicalGroup G]
129 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
133 (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
134 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1)
135 hKL.2
137@[simp]
139 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
140 [TopologicalSpace G] [IsTopologicalGroup G]
141 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
142 (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL).comp
143 (groupAlgebraOpenFiniteQuotientMap R G L) =
144 groupAlgebraOpenFiniteQuotientMap R G K := by
146 (R := R) (G := G)
147 (hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
148 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
149 (hUV := hKL.2)
151/-- The projection `[[R G]] -> (R/I)[G/U]` for an open-ideal/finite-group quotient index. -/
153 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
154 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
155 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
156 Carrier R G →+* CompletedGroupAlgebraOpenFiniteQuotientStage R G K :=
158 ((OrderDual.ofDual K.1).1 : Ideal R) K.2
160@[simp]
162 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
163 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
164 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
165 (completedGroupAlgebraOpenFiniteQuotientProjection R G K).comp
166 (toCompletedGroupAlgebraRingHom R G) =
167 groupAlgebraOpenFiniteQuotientMap R G K := by
168 rfl
170@[simp]
172 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
173 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
174 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
175 (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL).comp
177 completedGroupAlgebraOpenFiniteQuotientProjection R G K := by
179 (R := R) (G := G)
180 (hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
181 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
182 (hUV := hKL.2)
185 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R]
186 [IsTopologicalRing R] [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
187 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
189 groupAlgebraOpenFiniteQuotientKernel R G K := by
190 intro x hx
191 rw [mem_groupAlgebraOpenFiniteQuotientKernel_iff] at hx ⊢
192 have hcomp := congrFun
193 (congrArg DFunLike.coe
194 (completedGroupAlgebraOpenFiniteQuotientTransition_comp_map (R := R) (G := G) hKL))
195 x
197 exact hcomp.symm
199/-- The discrete topology on each kernel-neighborhood quotient `(R/I)[G/U]`. This is the topology
200used in the construction of the abstract group-algebra topology. -/
202 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
203 [TopologicalSpace G] [IsTopologicalGroup G]
204 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
205 TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
206 ⊥
209 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
210 [TopologicalSpace G] [IsTopologicalGroup G]
211 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
212 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
214 DiscreteTopology (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) := by
215 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
217 exact ⟨rfl⟩
219/-- The coefficient quotient from the finite stage `R[G/U]` to the kernel-neighborhood quotient
220`(R/I)[G/U]` is continuous when the target carries the discrete quotient topology. -/
222 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
223 letI : TopologicalSpace (CompletedGroupAlgebraStage R G K.2) :=
224 (completedGroupAlgebraSystem R G).topologicalSpace K.2
225 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
227 Continuous (completedGroupAlgebraStageCoeffQuotientMap R G
228 ((OrderDual.ofDual K.1).1 : Ideal R) K.2) := by
229 let Iopen : CompletedGroupAlgebraOpenIdeal R := OrderDual.ofDual K.1
230 let Q := CompletedGroupAlgebraQuotient G K.2
231 letI : TopologicalSpace (CompletedGroupAlgebraStage R G K.2) :=
232 (completedGroupAlgebraSystem R G).topologicalSpace K.2
233 letI : TopologicalSpace (R ⧸ (Iopen.1 : Ideal R)) := ⊥
234 haveI : DiscreteTopology (R ⧸ (Iopen.1 : Ideal R)) := ⟨rfl⟩
235 have hmk : Continuous (Ideal.Quotient.mk (Iopen.1 : Ideal R)) :=
237 (R := R) (I := Iopen.1) Iopen.2
238 have hcont :
239 letI : TopologicalSpace (CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 K.2) :=
240 finiteGroupAlgebraTopology (R ⧸ (Iopen.1 : Ideal R)) Q
241 Continuous (completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 K.2) := by
244 (R := R) (S := R ⧸ (Iopen.1 : Ideal R)) Q
245 (Ideal.Quotient.mk (Iopen.1 : Ideal R)) hmk
246 have hdisc :
247 letI : TopologicalSpace (CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 K.2) :=
248 finiteGroupAlgebraTopology (R ⧸ (Iopen.1 : Ideal R)) Q
249 DiscreteTopology (CompletedGroupAlgebraCoeffQuotientStage R G Iopen.1 K.2) := by
250 dsimp [CompletedGroupAlgebraCoeffQuotientStage, Q]
252 (S := R ⧸ (Iopen.1 : Ideal R)) Q
253 let tfin : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
254 finiteGroupAlgebraTopology (R ⧸ (Iopen.1 : Ideal R)) Q
255 let tdisc : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
257 have ht : tfin = tdisc := by
258 dsimp [tfin, tdisc, completedGroupAlgebraOpenFiniteQuotientStageTopology]
259 exact hdisc.eq_bot
260 change @Continuous (CompletedGroupAlgebraStage R G K.2)
262 ((completedGroupAlgebraSystem R G).topologicalSpace K.2) tdisc
263 (completedGroupAlgebraStageCoeffQuotientMap R G Iopen.1 K.2)
264 rw [← ht]
265 exact hcont
267/-- The projection `[[RG]] -> (R/I)[G/U]` to any two-parameter finite quotient is
268continuous. -/
270 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
271 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
273 Continuous (completedGroupAlgebraOpenFiniteQuotientProjection R G K) := by
274 letI : TopologicalSpace (CompletedGroupAlgebraStage R G K.2) :=
275 (completedGroupAlgebraSystem R G).topologicalSpace K.2
276 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
279 (R := R) (G := G) K).comp ((completedGroupAlgebraSystem R G).continuous_projection K.2)
281/-- The product of all open finite quotient maps `[R G] -> (R/I)[G/U]`. -/
283 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
284 [TopologicalSpace G] [IsTopologicalGroup G] :
285 MonoidAlgebra R G →
286 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →
288 fun x K => groupAlgebraOpenFiniteQuotientMap R G K x
290/-- The kernel-neighborhood topology on `[R G]`, induced by all maps
293 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
294 [TopologicalSpace G] [IsTopologicalGroup G] :
295 TopologicalSpace (MonoidAlgebra R G) :=
296 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
297 TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
298 fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
299 TopologicalSpace.induced (groupAlgebraOpenFiniteQuotientProductMap R G) inferInstance
302 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
303 [TopologicalSpace G] [IsTopologicalGroup G] :
304 letI : TopologicalSpace (MonoidAlgebra R G) :=
306 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
307 TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
308 fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
309 Continuous (groupAlgebraOpenFiniteQuotientProductMap R G) := by
310 letI : TopologicalSpace (MonoidAlgebra R G) :=
312 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
313 TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
314 fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
315 exact continuous_induced_dom
318 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
319 [TopologicalSpace G] [IsTopologicalGroup G]
320 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
321 letI : TopologicalSpace (MonoidAlgebra R G) :=
323 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
325 Continuous (groupAlgebraOpenFiniteQuotientMap R G K) := by
326 letI : TopologicalSpace (MonoidAlgebra R G) :=
328 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,
329 TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
330 fun K => completedGroupAlgebraOpenFiniteQuotientStageTopology R G K
331 change Continuous fun x : MonoidAlgebra R G =>
333 exact (continuous_apply K).comp
337 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
338 [TopologicalSpace G] [IsTopologicalGroup G]
339 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
340 letI : TopologicalSpace (MonoidAlgebra R G) :=
342 IsOpen (groupAlgebraOpenFiniteQuotientKernel R G K : Set (MonoidAlgebra R G)) := by
343 letI : TopologicalSpace (MonoidAlgebra R G) :=
345 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
347 haveI : DiscreteTopology (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=
349 change IsOpen ((groupAlgebraOpenFiniteQuotientMap R G K) ⁻¹'
350 ({0} : Set (CompletedGroupAlgebraOpenFiniteQuotientStage R G K)))
351 exact (isOpen_discrete ({0} : Set (CompletedGroupAlgebraOpenFiniteQuotientStage R G K))).preimage
355 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
356 [TopologicalSpace G] [IsTopologicalGroup G]
357 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
358 letI : TopologicalSpace (MonoidAlgebra R G) :=
360 (groupAlgebraOpenFiniteQuotientKernel R G K : Set (MonoidAlgebra R G)) ∈
361 𝓝 (0 : MonoidAlgebra R G) := by
362 letI : TopologicalSpace (MonoidAlgebra R G) :=
364 apply IsOpen.mem_nhds
366 change (0 : MonoidAlgebra R G) ∈ groupAlgebraOpenFiniteQuotientKernel R G K
368 exact map_zero (groupAlgebraOpenFiniteQuotientMap R G K)
370@[simp]
372 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
373 [TopologicalSpace G] [IsTopologicalGroup G]
374 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L)
375 (q : CompletedGroupAlgebraQuotient G L.2)
376 (r : R ⧸ ((OrderDual.ofDual L.1).1 : Ideal R)) :
378 (MonoidAlgebra.single q r) =
379 MonoidAlgebra.single
380 ((OpenNormalSubgroupInClass.map
381 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
382 (U := OrderDual.ofDual K.2) (V := OrderDual.ofDual L.2) hKL.2) q)
383 (Ideal.Quotient.factor
384 (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
385 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1) r) := by
386 exact completedGroupAlgebraFiniteQuotientTransition_single (R := R) (G := G)
387 (hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
388 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
389 (hUV := hKL.2) q r
391@[simp]
393 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
394 [TopologicalSpace G] [IsTopologicalGroup G]
395 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :
396 completedGroupAlgebraOpenFiniteQuotientTransition R G (le_rfl : K ≤ K) =
397 RingHom.id (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) := by
398 apply MonoidAlgebra.ringHom_ext
399 · intro r
402 · intro q
404 change MonoidAlgebra.single
405 ((OpenNormalSubgroupInClass.map
406 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
407 (U := OrderDual.ofDual K.2) (V := OrderDual.ofDual K.2)
408 (le_rfl : K.2 ≤ K.2)) q) 1 =
409 MonoidAlgebra.single q 1
410 rw [OpenNormalSubgroupInClass.map_id]
411 simp only [MonoidHom.id_apply]
413@[simp 900]
415 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
416 [TopologicalSpace G] [IsTopologicalGroup G]
417 {K L M : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) (hLM : L ≤ M) :
418 (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL).comp
419 (completedGroupAlgebraOpenFiniteQuotientTransition R G hLM) =
420 completedGroupAlgebraOpenFiniteQuotientTransition R G (hKL.trans hLM) := by
421 apply MonoidAlgebra.ringHom_ext
422 · intro r
423 rw [RingHom.comp_apply, completedGroupAlgebraOpenFiniteQuotientTransition_single,
427 · intro q
428 rw [RingHom.comp_apply, completedGroupAlgebraOpenFiniteQuotientTransition_single,
431 have hmap := congrFun
432 (congrArg DFunLike.coe
433 (OpenNormalSubgroupInClass.map_comp
434 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G)
435 (U := OrderDual.ofDual K.2) (V := OrderDual.ofDual L.2) (W := OrderDual.ofDual M.2)
436 hKL.2 hLM.2))
437 q
438 exact congrArg
439 (fun t => MonoidAlgebra.single t
440 (1 : R ⧸ ((OrderDual.ofDual K.1).1 : Ideal R)))
441 hmap
444 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]
445 [TopologicalSpace G] [IsTopologicalGroup G]
446 {K L : CompletedGroupAlgebraOpenQuotientIndex R G} (hKL : K ≤ L) :
447 Function.Surjective (completedGroupAlgebraOpenFiniteQuotientTransition R G hKL) :=
449 (R := R) (G := G)
450 (hIJ := (show ((OrderDual.ofDual L.1).1 : Ideal R) ≤
451 ((OrderDual.ofDual K.1).1 : Ideal R) from hKL.1))
452 (hUV := hKL.2)
453end