structure Hex.PermGroup.RightTransversal {n : Nat} (G H : Group n) : Type

A right transversal uses cosets Hg, with equality tested by xy⁻¹ ∈ H. It is a distinct result type from a left transversal.

• reps : Array (Element G)
• distinct (i j : Fin self.reps.size) : Generated H.generators (self.reps[↑i].val.comp self.reps[↑j].val.inv) → i = j
• covers (p : Element G) : ∃ (i : Fin self.reps.size), Generated H.generators (p.val.comp self.reps[↑i].val.inv)
• words : Vector Program self.reps.size
• checked (i : Fin self.reps.size) : checkWord G.generators self.reps[↑i].val self.words[↑i] = true

def Hex.PermGroup.LeftTransversal.inverse {n✝ : Nat} {G H : Group n✝} (t : LeftTransversal G H) : RightTransversal G H

Inversion converts a complete left transversal to a complete right transversal, including its programs in the original input generators.

Equations

• t.inverse = { reps := Array.map Hex.PermGroup.Element.inv t.reps, distinct := ⋯, covers := ⋯, words := Vector.cast ⋯ (Vector.map Hex.PermGroup.Program.inv t.words), checked := ⋯ }

theorem Hex.PermGroup.RightTransversal.disjoint {n : Nat} {G H : Group n} (t : RightTransversal G H) {i j : Fin t.reps.size} (hne : i ≠ j) (p : Perm n) : ¬(Generated H.generators (p.comp t.reps[↑i].val.inv) ∧ Generated H.generators (p.comp t.reps[↑j].val.inv))

theorem Hex.PermGroup.RightTransversal.covers_product {n : Nat} {G H : Group n} (t : RightTransversal G H) (p : Element G) : ∃ (i : Fin t.reps.size), ∃ (q : Element H), q.val.comp t.reps[↑i].val = p.val