This module exposes the right-coset quotient of a group by a subgroup and its natural action
g • [a] = [a * g⁻¹].
The quotient is intentionally only a coset space: for a non-normal subgroup it has no multiplication. Algebraic quotient arguments therefore use the usual left quotient rather than a misleading MulEquiv wrapper.
The right quotient H \ G, encoded by mathlib's right-coset relation.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
universe u
variable {G : Type u} [Group G]abbrev RightQuotient (H : Subgroup G)The right coset of an element modulo a subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
universe u
variable {G : Type u} [Group G]def rightCoset (H : Subgroup G) (g : G) : RightQuotient HA right coset is the base coset exactly when its representative lies in the subgroup.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
universe u
variable {G : Type u} [Group G]theorem rightCoset_eq_basepoint_iff_mem
{H : Subgroup G} {g : G} :
rightCoset H g = rightCoset H (1 : G) ↔ g ∈ HRight multiplication on right cosets, expressed as a left action by g • [a] = [a * g⁻¹].
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
universe u
variable {G : Type u} [Group G]def rightCosetMulAction (H : Subgroup G) :
MulAction G (RightQuotient H) where
smul g :=
Quotient.map' (fun a => a * g⁻¹) fun a b hab => by
rw [QuotientGroup.rightRel_apply] at hab ⊢
simpa [mul_assoc] using hab
one_smul q := by
refine Quotient.inductionOn' q ?_
intro a
apply Quotient.sound'
rw [QuotientGroup.rightRel_apply]
simp only [inv_one, mul_one, mul_inv_cancel, one_mem]
mul_smul g h q := by
refine Quotient.inductionOn' q ?_
intro a
apply Quotient.sound'
rw [QuotientGroup.rightRel_apply]
simp only [mul_assoc, mul_inv_rev, inv_inv, inv_mul_cancel_left, mul_inv_cancel, one_mem]Acting on a represented right coset multiplies its representative by the inverse on the right.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
universe u
variable {G : Type u} [Group G]
attribute [instance] rightCosetMulActiontheorem rightCosetMulAction_mk_smul
(H : Subgroup G) (g a : G) :
letI := rightCosetMulAction H
g • (Quotient.mk'' a : RightQuotient H) = Quotient.mk'' (a * g⁻¹) :=
rflActing by an inverse on a represented right coset multiplies its representative on the right.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ReidemeisterSchreier
universe u
variable {G : Type u} [Group G]
attribute [instance] rightCosetMulActiontheorem rightCosetMulAction_inv_mk_smul
(H : Subgroup G) (g a : G) :
letI := rightCosetMulAction H
g⁻¹ • (Quotient.mk'' a : RightQuotient H) = Quotient.mk'' (a * g) := by
rw [rightCosetMulAction_mk_smul (H := H) g⁻¹ a]
simp only [inv_inv]