ReidemeisterSchreier/Profinite/OpenSubgroups/RightQuotient.lean
1import ProCGroups.ProC.Subgroups.Products
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/ReidemeisterSchreier/Profinite/OpenSubgroups/RightQuotient.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Profinite open-subgroup Schreier theory
15Profinite open subgroup quotients, finite permutation targets, dense free models, exact right Schreier generation, and topological rank bounds.
16-/
18open Set
19open scoped Topology Pointwise
21namespace ReidemeisterSchreier
22namespace Profinite
24open ProCGroups
25open ProCGroups.ProC
27universe u
29section RightQuotientSections
31variable {F : Type u} [Group F] [TopologicalSpace F] [IsTopologicalGroup F]
33/-- The right-coset space `H \ F`, encoded via right quotients. -/
34abbrev OpenSubgroupRightQuotient (H : OpenSubgroup F) :=
35 _root_.ReidemeisterSchreier.RightQuotient (H : Subgroup F)
37/-- The right coset of an element modulo an open subgroup. -/
38def openSubgroupRightCoset (H : OpenSubgroup F) (g : F) : OpenSubgroupRightQuotient H :=
39 _root_.ReidemeisterSchreier.rightCoset (H : Subgroup F) g
41omit [IsTopologicalGroup F] in
42/-- A right coset is the base coset exactly when its representative lies in the subgroup. -/
44 {H : OpenSubgroup F} {g : F} :
45 openSubgroupRightCoset H g = openSubgroupRightCoset H (1 : F) ↔
46 g ∈ (H : Subgroup F) := by
47 exact _root_.ReidemeisterSchreier.rightCoset_eq_basepoint_iff_mem (H := (H : Subgroup F))
49omit [IsTopologicalGroup F] in
50@[simp] theorem openSubgroupRightCoset_smul
51 (H : OpenSubgroup F) (g a : F) :
52 letI : MulAction F (OpenSubgroupRightQuotient H) :=
53 _root_.ReidemeisterSchreier.rightCosetMulAction (H : Subgroup F)
54 g • openSubgroupRightCoset H a = openSubgroupRightCoset H (a * g⁻¹) :=
55 _root_.ReidemeisterSchreier.rightCosetMulAction_mk_smul (H := (H : Subgroup F)) g a
57omit [IsTopologicalGroup F] in
58@[simp] theorem openSubgroupRightCoset_inv_smul
59 (H : OpenSubgroup F) (g a : F) :
60 letI : MulAction F (OpenSubgroupRightQuotient H) :=
61 _root_.ReidemeisterSchreier.rightCosetMulAction (H : Subgroup F)
62 g⁻¹ • openSubgroupRightCoset H a = openSubgroupRightCoset H (a * g) :=
63 _root_.ReidemeisterSchreier.rightCosetMulAction_inv_mk_smul (H := (H : Subgroup F)) g a
65/-- Right cosets of an open subgroup are finite because they are equivalent to the left quotient. -/
66instance finite_openSubgroupRightQuotient (H : OpenSubgroup F) [CompactSpace F] :
67 Finite (OpenSubgroupRightQuotient H) := by
68 let e :=
69 QuotientGroup.quotientRightRelEquivQuotientLeftRel (H : Subgroup F)
70 exact Finite.of_equiv (F ⧸ (H : Subgroup F)) e.symm
72/-- Right cosets of an open subgroup inherit a `Fintype` from compactness. -/
73noncomputable instance fintype_openSubgroupRightQuotient (H : OpenSubgroup F) [CompactSpace F] :
74 Fintype (OpenSubgroupRightQuotient H) :=
75 Fintype.ofFinite (OpenSubgroupRightQuotient H)
77/-- The quotient topology on right cosets of an open subgroup is discrete. -/
78instance discreteTopology_openSubgroupRightQuotient (H : OpenSubgroup F) :
79 DiscreteTopology (OpenSubgroupRightQuotient H) := by
80 classical
81 refine discreteTopology_iff_isOpen_singleton.2 ?_
82 intro q
83 rw [← isQuotientMap_quotient_mk'.isOpen_preimage]
84 let qmk : F → OpenSubgroupRightQuotient H :=
85 @Quotient.mk' F (QuotientGroup.rightRel (H : Subgroup F))
86 let a : F := q.out
87 have hpre :
88 qmk ⁻¹' ({q} : Set (OpenSubgroupRightQuotient H)) =
89 (fun x : F => a * x⁻¹) ⁻¹' ((H : Subgroup F) : Set F) := by
90 ext x
91 constructor
92 · intro hx
93 have hEq : (Quotient.mk'' x : OpenSubgroupRightQuotient H) = Quotient.mk'' a := by
94 calc
95 (Quotient.mk'' x : OpenSubgroupRightQuotient H) = q := hx
96 _ = Quotient.mk'' a := (Quotient.out_eq' q).symm
97 have hrel : QuotientGroup.rightRel (H : Subgroup F) x a := Quotient.eq''.mp hEq
98 simpa [a] using (QuotientGroup.rightRel_apply.mp hrel)
99 · intro hx
100 have hrel : QuotientGroup.rightRel (H : Subgroup F) x a := by
101 rw [QuotientGroup.rightRel_apply]
102 simpa [a] using hx
103 change (Quotient.mk'' x : OpenSubgroupRightQuotient H) = q
104 calc
105 (Quotient.mk'' x : OpenSubgroupRightQuotient H) = Quotient.mk'' a :=
106 Quotient.eq''.mpr hrel
107 _ = q := by simp only [Quotient.out_eq, a]
108 have hpreOpen : IsOpen (qmk ⁻¹' ({q} : Set (OpenSubgroupRightQuotient H))) := by
109 rw [hpre]
110 exact H.isOpen'.preimage (continuous_const.mul continuous_inv)
111 simpa [qmk] using hpreOpen
113/-- A normalized section of the right-coset projection, sending the trivial coset to `1`. -/
114noncomputable def openSubgroupRightCosetSection
115 (H : OpenSubgroup F) : OpenSubgroupRightQuotient H → F := by
116 classical
117 intro q
118 exact
119 if hq : q = openSubgroupRightCoset H (1 : F) then
120 1
121 else
122 q.out
124omit [IsTopologicalGroup F] in
125@[simp] theorem openSubgroupRightCosetSection_spec
126 (H : OpenSubgroup F) (q : OpenSubgroupRightQuotient H) :
127 Quotient.mk'' (openSubgroupRightCosetSection (F := F) H q) = q := by
128 classical
129 by_cases hq : q = openSubgroupRightCoset H (1 : F)
130 · subst hq
131 simp only [openSubgroupRightCosetSection, openSubgroupRightCoset, rightCoset, ↓reduceDIte]
132 · simp only [openSubgroupRightCosetSection, hq, ↓reduceDIte, Quotient.out_eq]
134omit [IsTopologicalGroup F] in
135@[simp] theorem openSubgroupRightCosetSection_one
136 (H : OpenSubgroup F) :
137 openSubgroupRightCosetSection (F := F) H (openSubgroupRightCoset H (1 : F)) = 1 := by
138 classical
139 simp only [openSubgroupRightCosetSection, ↓reduceDIte]
141/-- The normalized right-coset section is continuous because the right quotient is discrete. -/
143 (H : OpenSubgroup F) :
144 Continuous (openSubgroupRightCosetSection (F := F) H) :=
145 continuous_of_discreteTopology
147end RightQuotientSections
149end Profinite
150end ReidemeisterSchreier