Source: ProCGroups.ReidemeisterSchreier.RightQuotient
1import Mathlib.GroupTheory.QuotientGroup.Basic
3/-!
4# Right cosets for Schreier rewriting
6This module exposes the right-coset quotient of a group by a subgroup and its
7natural action
9`g • [a] = [a * g⁻¹]`.
11The quotient is intentionally only a coset space: for a non-normal subgroup it
12has no multiplication. Algebraic quotient arguments therefore use the usual
13left quotient rather than a misleading `MulEquiv` wrapper.
14-/
16namespace ReidemeisterSchreier
18universe u
20variable {G : Type u} [Group G]
22/-- The right quotient `H \ G`, encoded by mathlib's right-coset relation. -/
23abbrev RightQuotient (H : Subgroup G) :=
24 Quotient (QuotientGroup.rightRel H)
26/-- The right coset of an element modulo a subgroup. -/
27def rightCoset (H : Subgroup G) (g : G) : RightQuotient H :=
28 Quotient.mk'' g
30/-- A right coset is the base coset exactly when its representative lies in the subgroup. -/
31theorem rightCoset_eq_basepoint_iff_mem
32 {H : Subgroup G} {g : G} :
33 rightCoset H g = rightCoset H (1 : G) ↔ g ∈ H := by
34 constructor
35 · intro hg
36 have hrel : QuotientGroup.rightRel H g 1 := Quotient.exact' hg
37 have hginv : g⁻¹ ∈ H := by
38 simpa using (QuotientGroup.rightRel_apply.mp hrel)
39 simpa using H.inv_mem hginv
40 · intro hg
41 apply Quotient.sound'
42 rw [QuotientGroup.rightRel_apply]
43 simpa using H.inv_mem hg
45/-- Right multiplication on right cosets, expressed as a left action by
46`g • [a] = [a * g⁻¹]`. -/
47@[reducible] def rightCosetMulAction (H : Subgroup G) :
48 MulAction G (RightQuotient H) where
49 smul g :=
50 Quotient.map' (fun a => a * g⁻¹) fun a b hab => by
51 rw [QuotientGroup.rightRel_apply] at hab ⊢
52 simpa [mul_assoc] using hab
53 one_smul q := by
54 refine Quotient.inductionOn' q ?_
55 intro a
56 apply Quotient.sound'
57 rw [QuotientGroup.rightRel_apply]
58 simp only [inv_one, mul_one, mul_inv_cancel, one_mem]
59 mul_smul g h q := by
60 refine Quotient.inductionOn' q ?_
61 intro a
62 apply Quotient.sound'
63 rw [QuotientGroup.rightRel_apply]
64 simp only [mul_assoc, mul_inv_rev, inv_inv, inv_mul_cancel_left, mul_inv_cancel, one_mem]
66/-- Acting on a represented right coset multiplies its representative by the inverse on the
67right. -/
68@[simp] theorem rightCosetMulAction_mk_smul
69 (H : Subgroup G) (g a : G) :
70 letI := rightCosetMulAction H
71 g • (Quotient.mk'' a : RightQuotient H) = Quotient.mk'' (a * g⁻¹) :=
72 rfl
74/-- Acting by an inverse on a represented right coset multiplies its representative on the
75right. -/
76@[simp] theorem rightCosetMulAction_inv_mk_smul
77 (H : Subgroup G) (g a : G) :
78 letI := rightCosetMulAction H
79 g⁻¹ • (Quotient.mk'' a : RightQuotient H) = Quotient.mk'' (a * g) := by
80 rw [rightCosetMulAction_mk_smul (H := H) g⁻¹ a]
81 simp only [inv_inv]
83end ReidemeisterSchreier