CompletedGroupAlgebra/UniversalProperty/OpenSubmoduleQuotient.lean
1import CompletedGroupAlgebra.UniversalProperty.FiniteQuotient
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/UniversalProperty/OpenSubmoduleQuotient.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Open-submodule quotient lifts
14This module proves the open-submodule quotient version of the completed group-algebra universal property, reducing continuity to finite discrete quotients.
15-/
17open scoped Topology
19namespace CompletedGroupAlgebra
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
26open ProCGroups.Completion
28universe u v w
30variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]
31variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
33/-- Quotient-target form of Lemma 5.3.5(d)'s existence step: after quotienting a profinite target
34module by an open submodule, the prescribed continuous map from `G` extends uniquely from
35`[[RG]]`. -/
37 (hG : ProCGroups.IsProfiniteGroup G)
38 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
39 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
40 (W : Submodule R N) (hW : IsOpen (W : Set N)) :
41 ∃! F : Carrier R G →L[R] N ⧸ W,
42 ∀ g : G, F (completedGroupAlgebraOf R G g) = Submodule.mkQ W (f g) := by
43 let hdisc : IsDiscreteModule R (N ⧸ W) :=
44 quotient_openSubmodule_isDiscreteModule R N hN W hW
45 letI : IsTopologicalRing R := hN.1.1
46 letI : IsTopologicalAddGroup (N ⧸ W) := hdisc.1.2.1
47 letI : ContinuousAdd (N ⧸ W) := inferInstance
48 letI : ContinuousSMul R (N ⧸ W) := hdisc.1.2.2
49 letI : DiscreteTopology (N ⧸ W) := hdisc.2
50 letI : T2Space (N ⧸ W) := inferInstance
51 have hqcont : Continuous (Submodule.mkQ W : N → N ⧸ W) := by
52 change Continuous (Submodule.Quotient.mk (p := W))
53 exact continuous_quotient_mk'
55 (G := G) hG (N ⧸ W) (fun g : G => Submodule.mkQ W (f g))
56 (hqcont.comp hf) with
57 ⟨U, fbar, hfac⟩
58 exact completedGroupAlgebra_existsUnique_lift_of_factors (R := R) (G := G) hG (N ⧸ W)
59 U (fun g : G => Submodule.mkQ W (f g)) fbar hfac
61/-- The chosen quotient-valued extension attached to an open submodule of a profinite target. -/
63 (hG : ProCGroups.IsProfiniteGroup G)
64 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
65 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
66 (W : Submodule R N) (hW : IsOpen (W : Set N)) :
67 Carrier R G →L[R] N ⧸ W :=
68 Classical.choose
70 (R := R) (G := G) hG N hN f hf W hW)
72/-- The quotient-valued lift has the prescribed value on completed group-like elements. -/
73@[simp]
75 (hG : ProCGroups.IsProfiniteGroup G)
76 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
77 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
78 (W : Submodule R N) (hW : IsOpen (W : Set N)) (g : G) :
80 (R := R) (G := G) hG N hN f hf W hW
81 (completedGroupAlgebraOf R G g) =
82 Submodule.mkQ W (f g) := by
83 exact (Classical.choose_spec
85 (R := R) (G := G) hG N hN f hf W hW)).1 g
87/-- The quotient-valued extensions are compatible with refinement of open submodules. -/
89 (hG : ProCGroups.IsProfiniteGroup G)
90 (N : Type (max u v)) [AddCommGroup N] [TopologicalSpace N] [Module R N]
91 (hN : IsProfiniteModule R N) (f : G → N) (hf : Continuous f)
92 {W V : Submodule R N} (hWV : W ≤ V)
93 (hW : IsOpen (W : Set N)) (hV : IsOpen (V : Set N))
94 (x : Carrier R G) :
95 Submodule.factor hWV
97 (R := R) (G := G) hG N hN f hf W hW x) =
99 (R := R) (G := G) hG N hN f hf V hV x := by
100 let hdiscV : IsDiscreteModule R (N ⧸ V) :=
101 quotient_openSubmodule_isDiscreteModule R N hN V hV
102 let hdiscW : IsDiscreteModule R (N ⧸ W) :=
103 quotient_openSubmodule_isDiscreteModule R N hN W hW
104 letI : DiscreteTopology (N ⧸ W) := hdiscW.2
105 letI : DiscreteTopology (N ⧸ V) := hdiscV.2
106 letI : T2Space (N ⧸ V) := inferInstance
107 let factorCLM : N ⧸ W →L[R] N ⧸ V :=
108 { toLinearMap := Submodule.factor hWV
109 cont := continuous_of_discreteTopology }
110 have hEq :
111 factorCLM.comp
113 (R := R) (G := G) hG N hN f hf W hW) =
115 (R := R) (G := G) hG N hN f hf V hV := by
116 apply completedGroupAlgebraContinuousLinearMap_ext_of_basis (R := R) (G := G) hG
117 intro g
118 change Submodule.factor hWV
120 (R := R) (G := G) hG N hN f hf W hW
121 (completedGroupAlgebraOf R G g)) =
123 (R := R) (G := G) hG N hN f hf V hV
124 (completedGroupAlgebraOf R G g)
127 Submodule.factor_mk]
128 exact congrArg (fun F : Carrier R G →L[R] N ⧸ V => F x) hEq
129end