ReidemeisterSchreier.RightQuotient
This module formalizes right quotients and transversals for subgroup rewriting.
import
- Mathlib.GroupTheory.QuotientGroup.Basic
abbrev RightQuotient (H : Subgroup G) :=
Quotient (QuotientGroup.rightRel H)The right quotient \(H\backslash G\) is realized as the standard quotient by the right-coset relation.
def rightCoset (H : Subgroup G) (g : G) : RightQuotient H :=
Quotient.mk'' gThe right coset of an element modulo a subgroup.
theorem rightCoset_eq_basepoint_iff_mem
{H : Subgroup G} {g : G} :
rightCoset H g = rightCoset H (1 : G) ↔ g ∈ HA right coset is the base coset exactly when its representative lies in the subgroup.
Show proof
by
constructor
· intro hg
have hrel : QuotientGroup.rightRel H g 1 := Quotient.exact' hg
have hginv : g⁻¹ ∈ H := by
simpa using (QuotientGroup.rightRel_apply.mp hrel)
simpa using H.inv_mem hginv
· intro hg
apply Quotient.sound'
rw [QuotientGroup.rightRel_apply]
simpa using H.inv_mem hgProof. Unfold the right-coset quotient relation. Two elements define the same quotient point exactly when they differ by an element of the subgroup on the right, and the quotient map respects multiplication by representatives through this relation. The stated formulas follow by rewriting membership and equality in the quotient relation.
□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]Right multiplication on right cosets, expressed as the left action \(g\cdot [a]=[a g^{-1}]\).
@[simp] theorem rightCosetMulAction_mk_smul
(H : Subgroup G) (g a : G) :
letIThe right-coset multiplication action has the displayed representative formula.
Show proof
rightCosetMulAction H
g • (Quotient.mk'' a : RightQuotient H) = Quotient.mk'' (a * g⁻¹) :=
rflProof. Unfold the right-coset quotient relation. Two elements define the same quotient point exactly when they differ by an element of the subgroup on the right, and the quotient map respects multiplication by representatives through this relation. The stated formulas follow by rewriting membership and equality in the quotient relation.
□@[simp] theorem rightCosetMulAction_inv_mk_smul
(H : Subgroup G) (g a : G) :
letIThe right-coset multiplication action has the displayed representative formula.
Show proof
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]Proof. Unfold the right-coset quotient relation. Two elements define the same quotient point exactly when they differ by an element of the subgroup on the right, and the quotient map respects multiplication by representatives through this relation. The stated formulas follow by rewriting membership and equality in the quotient relation.
□@[simp] theorem rightCosetMulAction_rightCoset_smul
(H : Subgroup G) (g a : G) :
letIUnder the left action on right cosets, \(g\) sends the right coset of \(a\) to the right coset of \(a g^{-1}\).
Show proof
rightCosetMulAction H
g • rightCoset H a = rightCoset H (a * g⁻¹) :=
rightCosetMulAction_mk_smul H g aProof. Unfold the right-coset quotient relation. Two elements define the same quotient point exactly when they differ by an element of the subgroup on the right, and the quotient map respects multiplication by representatives through this relation. The stated formulas follow by rewriting membership and equality in the quotient relation.
□@[simp] theorem rightCosetMulAction_inv_rightCoset_smul
(H : Subgroup G) (g a : G) :
letIUnder the left action on right cosets, \(g^{-1}\) sends the right coset of \(a\) to the right coset of \(a g\).
Show proof
rightCosetMulAction H
g⁻¹ • rightCoset H a = rightCoset H (a * g) :=
rightCosetMulAction_inv_mk_smul H g aProof. Unfold the right-coset quotient relation. Two elements define the same quotient point exactly when they differ by an element of the subgroup on the right, and the quotient map respects multiplication by representatives through this relation. The stated formulas follow by rewriting membership and equality in the quotient relation.
□def rightQuotientEquivLeftQuotient (H : Subgroup G) :
RightQuotient H ≃ G ⧸ H :=
QuotientGroup.quotientRightRelEquivQuotientLeftRel HRight cosets are equivalent to the usual left quotient. It packages mutually inverse maps as an algebraic or topological equivalence.