Source: ProCGroups.CompletedGroupAlgebra.UniversalProperty.OpenSubmoduleQuotient
1import ProCGroups.CompletedGroupAlgebra.UniversalProperty.FiniteQuotient
3/-!
4# Lifts to open-submodule quotients
6The finite-quotient universal property yields a unique continuous linear lift to the quotient of a
7profinite module by an open submodule. This file constructs the lift and records its value on
8group-like generators and its factorization formula.
9-/
11open scoped Topology
13namespace CompletedGroupAlgebra
15noncomputable section
17open ProCGroups
18open ProCGroups.ProC
19open ProCGroups.InverseSystems
20open ProCGroups.Completion
22universe u v w
24variable (R : ProfiniteCommRing.{u})
25variable (G : ProfiniteGrp.{v})
27local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) : Module R N :=
28 N.module
30local instance (N : ProfiniteModule.{u, w} R.toProfiniteRing) :
31 ContinuousSMul R N :=
32 N.continuousSMul
34/--
35The quotient-target form of the existence step in Lemma 5.3.5(d): after quotienting a profinite
36target module by an open submodule, the prescribed continuous map from \(G\) extends uniquely
37from \(\widehat{R[G]}\).
38-/
39theorem completedGroupAlgebra_existsUnique_lift_to_openSubmoduleQuotient
40 (N : ProfiniteModule.{u, w} R.toProfiniteRing)
41 (f : G → N) (hf : Continuous f)
42 (W : Submodule R N) (hW : IsOpen (W : Set N)) :
43 ∃! F : CompletedGroupAlgebraCarrier R G →L[R] N ⧸ W,
44 ∀ g : G, F (completedGroupAlgebraOf R G g) = Submodule.mkQ W (f g) := by
45 let hdisc : IsDiscreteModule R (N ⧸ W) :=
46 quotient_openSubmodule_isDiscreteModule R N W hW
47 letI : IsTopologicalAddGroup (N ⧸ W) := hdisc.1.2.1
48 letI : ContinuousAdd (N ⧸ W) := inferInstance
49 letI : ContinuousSMul R (N ⧸ W) := hdisc.1.2.2
50 letI : DiscreteTopology (N ⧸ W) := hdisc.2
51 letI : T2Space (N ⧸ W) := inferInstance
52 have hqcont : Continuous (Submodule.mkQ W : N → N ⧸ W) := by
53 change Continuous (Submodule.Quotient.mk (p := W))
54 exact continuous_quotient_mk'
55 rcases exists_completedGroupAlgebraIndex_factor_continuous_discrete
56 (G := G) (N ⧸ W) (fun g : G => Submodule.mkQ W (f g))
57 (hqcont.comp hf) with
58 ⟨U, fbar, hfac⟩
59 exact completedGroupAlgebra_existsUnique_lift_of_factors (R := R) (G := G) (N ⧸ W)
60 U (fun g : G => Submodule.mkQ W (f g)) fbar hfac
62/-- The chosen quotient-valued extension attached to an open submodule of a profinite target. -/
63def completedGroupAlgebraLiftToOpenSubmoduleQuotient
64 (N : ProfiniteModule.{u, w} R.toProfiniteRing)
65 (f : G → N) (hf : Continuous f)
66 (W : Submodule R N) (hW : IsOpen (W : Set N)) :
67 CompletedGroupAlgebraCarrier R G →L[R] N ⧸ W :=
68 Classical.choose
69 (completedGroupAlgebra_existsUnique_lift_to_openSubmoduleQuotient
70 (R := R) (G := G) N f hf W hW)
72/-- The quotient-valued lift has the prescribed value on completed group-like elements. -/
73@[simp]
74theorem completedGroupAlgebraLiftToOpenSubmoduleQuotient_apply_of
75 (N : ProfiniteModule.{u, w} R.toProfiniteRing)
76 (f : G → N) (hf : Continuous f)
77 (W : Submodule R N) (hW : IsOpen (W : Set N)) (g : G) :
78 completedGroupAlgebraLiftToOpenSubmoduleQuotient
79 (R := R) (G := G) N f hf W hW
80 (completedGroupAlgebraOf R G g) =
81 Submodule.mkQ W (f g) := by
82 exact (Classical.choose_spec
83 (completedGroupAlgebra_existsUnique_lift_to_openSubmoduleQuotient
84 (R := R) (G := G) N f hf W hW)).1 g
86/-- The quotient-valued extensions are compatible with refinement of open submodules. -/
87theorem completedGroupAlgebraLiftToOpenSubmoduleQuotient_factor
88 (N : ProfiniteModule.{u, w} R.toProfiniteRing)
89 (f : G → N) (hf : Continuous f)
90 {W V : Submodule R N} (hWV : W ≤ V)
91 (hW : IsOpen (W : Set N)) (hV : IsOpen (V : Set N))
92 (x : CompletedGroupAlgebraCarrier R G) :
93 Submodule.factor hWV
94 (completedGroupAlgebraLiftToOpenSubmoduleQuotient
95 (R := R) (G := G) N f hf W hW x) =
96 completedGroupAlgebraLiftToOpenSubmoduleQuotient
97 (R := R) (G := G) N f hf V hV x := by
98 let hdiscV : IsDiscreteModule R (N ⧸ V) :=
99 quotient_openSubmodule_isDiscreteModule R N V hV
100 let hdiscW : IsDiscreteModule R (N ⧸ W) :=
101 quotient_openSubmodule_isDiscreteModule R N W hW
102 letI : DiscreteTopology (N ⧸ W) := hdiscW.2
103 letI : DiscreteTopology (N ⧸ V) := hdiscV.2
104 letI : T2Space (N ⧸ V) := inferInstance
105 let factorCLM : N ⧸ W →L[R] N ⧸ V :=
106 { toLinearMap := Submodule.factor hWV
107 cont := continuous_of_discreteTopology }
108 have hEq :
109 factorCLM.comp
110 (completedGroupAlgebraLiftToOpenSubmoduleQuotient
111 (R := R) (G := G) N f hf W hW) =
112 completedGroupAlgebraLiftToOpenSubmoduleQuotient
113 (R := R) (G := G) N f hf V hV := by
114 apply completedGroupAlgebraContinuousLinearMap_ext_of_basis (R := R) (G := G)
115 intro g
116 change Submodule.factor hWV
117 (completedGroupAlgebraLiftToOpenSubmoduleQuotient
118 (R := R) (G := G) N f hf W hW
119 (completedGroupAlgebraOf R G g)) =
120 completedGroupAlgebraLiftToOpenSubmoduleQuotient
121 (R := R) (G := G) N f hf V hV
122 (completedGroupAlgebraOf R G g)
123 rw [completedGroupAlgebraLiftToOpenSubmoduleQuotient_apply_of,
124 completedGroupAlgebraLiftToOpenSubmoduleQuotient_apply_of,
125 Submodule.factor_mk]
126 exact congrArg (fun F : CompletedGroupAlgebraCarrier R G →L[R] N ⧸ V => F x) hEq
127end
129end CompletedGroupAlgebra