@[instance_reducible]

def Hex.PermGroup.LeftCoset.setoid {n : Nat} (H : Group n) : Setoid (Perm n)

Left cosets satisfy pH = qH exactly when q⁻¹p lies in H.

Equations

• Hex.PermGroup.LeftCoset.setoid H = { r := fun (p q : Hex.Perm n) => Hex.PermGroup.Generated H.generators (q.inv.comp p), iseqv := ⋯ }

@[reducible, inline]

abbrev Hex.PermGroup.LeftCoset {n : Nat} (H : Group n) : Type

Cosets retain representatives internally, with equality determined by a checked subgroup membership test. No normality assumption is made.

Equations

• Hex.PermGroup.LeftCoset H = Quotient (Hex.PermGroup.LeftCoset.setoid H)

@[instance_reducible]

instance Hex.PermGroup.LeftCoset.instDecidableEq {n : Nat} (H : Group n) : DecidableEq (LeftCoset H)

Equations

• Hex.PermGroup.LeftCoset.instDecidableEq H = Quotient.decidableEq

def Hex.PermGroup.LeftCoset.mk {n : Nat} (H : Group n) (p : Perm n) : LeftCoset H

Equations

• Hex.PermGroup.LeftCoset.mk H p = Quotient.mk (Hex.PermGroup.LeftCoset.setoid H) p

theorem Hex.PermGroup.LeftCoset.eq_iff {n : Nat} (H : Group n) (p q : Perm n) : mk H p = mk H q ↔ Generated H.generators (q.inv.comp p)

@[simp]

theorem Hex.PermGroup.LeftCoset.eq_id {n : Nat} (H : Group n) (p : Perm n) : mk H p = mk H (Perm.id n) ↔ Generated H.generators p

def Hex.PermGroup.LeftCoset.act {n : Nat} {H : Group n} (p : Perm n) (q : LeftCoset H) : LeftCoset H

Left multiplication is well-defined on left cosets for every subgroup.

Equations

• Hex.PermGroup.LeftCoset.act p q = Quotient.liftOn q (fun (r : Hex.Perm n) => Hex.PermGroup.LeftCoset.mk H (p.comp r)) ⋯

@[simp]

theorem Hex.PermGroup.LeftCoset.act_mk {n : Nat} (H : Group n) (p q : Perm n) : act p (mk H q) = mk H (p.comp q)

@[simp]

theorem Hex.PermGroup.LeftCoset.act_id {n : Nat} {H : Group n} (q : LeftCoset H) : act (Perm.id n) q = q

theorem Hex.PermGroup.LeftCoset.act_comp {n : Nat} {H : Group n} (p q : Perm n) (r : LeftCoset H) : act (p.comp q) r = act p (act q r)

def Hex.PermGroup.Action.leftCosets {n : Nat} (G H : Group n) : Action G (LeftCoset H)

The left action used for transversal discovery, including nonnormal subgroups.

Equations

• Hex.PermGroup.Action.leftCosets G H = { act := fun (p : Hex.PermGroup.Element G) (q : Hex.PermGroup.LeftCoset H) => Hex.PermGroup.LeftCoset.act p.val q, id_act := ⋯, comp_act := ⋯ }