ReidemeisterSchreier/RightQuotient.lean
1import Mathlib.GroupTheory.QuotientGroup.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ReidemeisterSchreier/RightQuotient.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Right quotients of groups
14This file contains the group-theoretic right-coset quotient API used by both
15discrete and profinite Reidemeister-Schreier constructions. It is mathlib-only:
16topology, compactness, and open-subgroup sections are added in profinite files.
17-/
19namespace ReidemeisterSchreier
21universe u
23variable {G : Type u} [Group G]
25/-- The right quotient `H \ G`, encoded by mathlib's right-coset relation. -/
26abbrev RightQuotient (H : Subgroup G) :=
27 Quotient (QuotientGroup.rightRel H)
29/-- The right coset of an element modulo a subgroup. -/
30def rightCoset (H : Subgroup G) (g : G) : RightQuotient H :=
31 Quotient.mk'' g
33/-- A right coset is the base coset exactly when its representative lies in the subgroup. -/
35 {H : Subgroup G} {g : G} :
36 rightCoset H g = rightCoset H (1 : G) ↔ g ∈ H := by
37 constructor
38 · intro hg
39 have hrel : QuotientGroup.rightRel H g 1 := Quotient.exact' hg
40 have hginv : g⁻¹ ∈ H := by
41 simpa using (QuotientGroup.rightRel_apply.mp hrel)
42 simpa using H.inv_mem hginv
43 · intro hg
44 apply Quotient.sound'
45 rw [QuotientGroup.rightRel_apply]
46 simpa using H.inv_mem hg
48/-- Right multiplication on right cosets, expressed as a left action by
49`g • [a] = [a * g⁻¹]`. -/
50def rightCosetMulAction (H : Subgroup G) :
51 MulAction G (RightQuotient H) where
52 smul g :=
53 Quotient.map' (fun a => a * g⁻¹) fun a b hab => by
54 rw [QuotientGroup.rightRel_apply] at hab ⊢
55 simpa [mul_assoc] using hab
56 one_smul q := by
57 refine Quotient.inductionOn' q ?_
58 intro a
59 apply Quotient.sound'
60 rw [QuotientGroup.rightRel_apply]
61 simp only [inv_one, mul_one, mul_inv_cancel, one_mem]
62 mul_smul g h q := by
63 refine Quotient.inductionOn' q ?_
64 intro a
65 apply Quotient.sound'
66 rw [QuotientGroup.rightRel_apply]
69@[simp] theorem rightCosetMulAction_mk_smul
70 (H : Subgroup G) (g a : G) :
71 letI := rightCosetMulAction H
72 g • (Quotient.mk'' a : RightQuotient H) = Quotient.mk'' (a * g⁻¹) :=
73 rfl
75@[simp] theorem rightCosetMulAction_inv_mk_smul
76 (H : Subgroup G) (g a : G) :
77 letI := rightCosetMulAction H
78 g⁻¹ • (Quotient.mk'' a : RightQuotient H) = Quotient.mk'' (a * g) := by
79 rw [rightCosetMulAction_mk_smul (H := H) g⁻¹ a]
82@[simp] theorem rightCosetMulAction_rightCoset_smul
83 (H : Subgroup G) (g a : G) :
84 letI := rightCosetMulAction H
85 g • rightCoset H a = rightCoset H (a * g⁻¹) :=
86 rightCosetMulAction_mk_smul H g a
88@[simp] theorem rightCosetMulAction_inv_rightCoset_smul
89 (H : Subgroup G) (g a : G) :
90 letI := rightCosetMulAction H
91 g⁻¹ • rightCoset H a = rightCoset H (a * g) :=
92 rightCosetMulAction_inv_mk_smul H g a
94/-- Right cosets are equivalent to the usual left quotient. -/
95def rightQuotientEquivLeftQuotient (H : Subgroup G) :
96 RightQuotient H ≃ G ⧸ H :=
97 QuotientGroup.quotientRightRelEquivQuotientLeftRel H
99end ReidemeisterSchreier