Source: ProCGroups.ReidemeisterSchreier.Profinite.OpenSubgroups.RightQuotient
1import ProCGroups.ProC.Subgroups.Products
2import ProCGroups.ReidemeisterSchreier.RightQuotient
4/-!
5# Right cosets of open subgroups
7For an open subgroup this module specializes the right-coset space used by
8Schreier rewriting. It supplies the coset action, finiteness under compactness,
9the discrete quotient topology, and a normalized continuous section of the
10right-coset projection.
11-/
13open Set
14open scoped Topology Pointwise
16namespace ReidemeisterSchreier
17namespace Profinite
19open ProCGroups
20open ProCGroups.ProC
22universe u
24section RightQuotientSections
26variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
28/-- An open subgroup of a compact topological group is compact in its subtype
29topology. This standard instance is shared by the bundled profinite and
30pro-\(C\) subgroup carriers. -/
31noncomputable instance compactSpace_openSubgroupSubtype
32 (H : OpenSubgroup F) [CompactSpace F] :
33 CompactSpace ↥(H : Subgroup F) := by
34 exact
35 (Subgroup.isClosed_of_isOpen (H : Subgroup F)
36 H.isOpen').isClosedEmbedding_subtypeVal.compactSpace
38/-- The right-coset space \(F/H\), encoded via right quotients. -/
39abbrev OpenSubgroupRightQuotient (H : OpenSubgroup F) :=
40 _root_.ReidemeisterSchreier.RightQuotient (H : Subgroup F)
42/-- The right coset of an element modulo an open subgroup. -/
43def openSubgroupRightCoset (H : OpenSubgroup F) (g : F) : OpenSubgroupRightQuotient H :=
44 _root_.ReidemeisterSchreier.rightCoset (H : Subgroup F) g
46omit [IsTopologicalGroup F] in
47/-- A right coset is the base coset exactly when its representative lies in the subgroup. -/
48theorem openSubgroupRightCoset_eq_basepoint_iff_mem
49 {H : OpenSubgroup F} {g : F} :
50 openSubgroupRightCoset H g = openSubgroupRightCoset H (1 : F) ↔
51 g ∈ (H : Subgroup F) := by
52 exact _root_.ReidemeisterSchreier.rightCoset_eq_basepoint_iff_mem (H := (H : Subgroup F))
54omit [IsTopologicalGroup F] in
55/--
56The open-subgroup right-coset action sends the coset of \(a\) by \(g\) to the coset of \(a
57g^{-1}\).
58-/
59@[simp] theorem openSubgroupRightCoset_smul
60 (H : OpenSubgroup F) (g a : F) :
61 letI : MulAction F (OpenSubgroupRightQuotient H) :=
62 _root_.ReidemeisterSchreier.rightCosetMulAction (H : Subgroup F)
63 g • openSubgroupRightCoset H a = openSubgroupRightCoset H (a * g⁻¹) :=
64 _root_.ReidemeisterSchreier.rightCosetMulAction_mk_smul (H := (H : Subgroup F)) g a
66omit [IsTopologicalGroup F] in
67/--
68The open-subgroup right-coset action sends the coset of \(a\) by \(g^{-1}\) to the coset of \(a
69g\).
70-/
71@[simp] theorem openSubgroupRightCoset_inv_smul
72 (H : OpenSubgroup F) (g a : F) :
73 letI : MulAction F (OpenSubgroupRightQuotient H) :=
74 _root_.ReidemeisterSchreier.rightCosetMulAction (H : Subgroup F)
75 g⁻¹ • openSubgroupRightCoset H a = openSubgroupRightCoset H (a * g) :=
76 _root_.ReidemeisterSchreier.rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F)) g a
78/-- Right cosets of an open subgroup are finite because they are equivalent to the left quotient. -/
79instance finite_openSubgroupRightQuotient (H : OpenSubgroup F) [CompactSpace F] :
80 Finite (OpenSubgroupRightQuotient H) := by
81 let e :=
82 QuotientGroup.quotientRightRelEquivQuotientLeftRel (H : Subgroup F)
83 exact Finite.of_equiv (F ⧸ (H : Subgroup F)) e.symm
85/-- Right cosets of an open subgroup inherit a Fintype from compactness. -/
86noncomputable instance fintype_openSubgroupRightQuotient (H : OpenSubgroup F) [CompactSpace F] :
87 Fintype (OpenSubgroupRightQuotient H) :=
88 Fintype.ofFinite (OpenSubgroupRightQuotient H)
90/-- The quotient topology on right cosets of an open subgroup is discrete. -/
91instance discreteTopology_openSubgroupRightQuotient (H : OpenSubgroup F) :
92 DiscreteTopology (OpenSubgroupRightQuotient H) := by
93 classical
94 refine discreteTopology_iff_isOpen_singleton.2 ?_
95 intro q
96 rw [← isQuotientMap_quotient_mk'.isOpen_preimage]
97 let qmk : F → OpenSubgroupRightQuotient H :=
98 @Quotient.mk' F (QuotientGroup.rightRel (H : Subgroup F))
99 let a : F := q.out
100 have hpre :
101 qmk ⁻¹' ({q} : Set (OpenSubgroupRightQuotient H)) =
102 (fun x : F => a * x⁻¹) ⁻¹' ((H : Subgroup F) : Set F) := by
103 ext x
104 constructor
105 · intro hx
106 have hEq : (Quotient.mk'' x : OpenSubgroupRightQuotient H) = Quotient.mk'' a := by
107 calc
108 (Quotient.mk'' x : OpenSubgroupRightQuotient H) = q := hx
109 _ = Quotient.mk'' a := (Quotient.out_eq' q).symm
110 have hrel : QuotientGroup.rightRel (H : Subgroup F) x a := Quotient.eq''.mp hEq
111 simpa [a] using (QuotientGroup.rightRel_apply.mp hrel)
112 · intro hx
113 have hrel : QuotientGroup.rightRel (H : Subgroup F) x a := by
114 rw [QuotientGroup.rightRel_apply]
115 simpa [a] using hx
116 change (Quotient.mk'' x : OpenSubgroupRightQuotient H) = q
117 calc
118 (Quotient.mk'' x : OpenSubgroupRightQuotient H) = Quotient.mk'' a :=
119 Quotient.eq''.mpr hrel
120 _ = q := by simp only [Quotient.out_eq, a]
121 have hpreOpen : IsOpen (qmk ⁻¹' ({q} : Set (OpenSubgroupRightQuotient H))) := by
122 rw [hpre]
123 exact H.isOpen'.preimage (continuous_const.mul continuous_inv)
124 simpa [qmk] using hpreOpen
126/-- A normalized section of the right-coset projection, sending the trivial coset to \(1\). -/
127noncomputable def openSubgroupRightCosetSection
128 (H : OpenSubgroup F) : OpenSubgroupRightQuotient H → F := by
129 classical
130 intro q
131 exact
132 if hq : q = openSubgroupRightCoset H (1 : F) then
133 1
134 else
135 q.out
137omit [IsTopologicalGroup F] in
138/--
139The chosen section of the open-subgroup right quotient projects back to the given right coset.
140-/
141@[simp] theorem openSubgroupRightCosetSection_spec
142 (H : OpenSubgroup F) (q : OpenSubgroupRightQuotient H) :
143 Quotient.mk'' (openSubgroupRightCosetSection (F := F) H q) = q := by
144 classical
145 by_cases hq : q = openSubgroupRightCoset H (1 : F)
146 · subst hq
147 simp only [openSubgroupRightCosetSection, openSubgroupRightCoset, rightCoset, ↓reduceDIte]
148 · simp only [openSubgroupRightCosetSection, hq, ↓reduceDIte, Quotient.out_eq]
150omit [IsTopologicalGroup F] in
151/--
152The chosen section of the open-subgroup right quotient sends the identity coset to the identity
153representative.
154-/
155@[simp] theorem openSubgroupRightCosetSection_one
156 (H : OpenSubgroup F) :
157 openSubgroupRightCosetSection (F := F) H (openSubgroupRightCoset H (1 : F)) = 1 := by
158 classical
159 simp only [openSubgroupRightCosetSection, ↓reduceDIte]
161/--
162The normalized right-coset section is continuous because the right quotient is discrete. It is a
163continuity claim, checked through the topology generated by finite-stage projections.
164-/
165theorem continuous_openSubgroupRightCosetSection
166 (H : OpenSubgroup F) :
167 Continuous (openSubgroupRightCosetSection (F := F) H) :=
168 continuous_of_discreteTopology
170end RightQuotientSections
172end Profinite
173end ReidemeisterSchreier