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

One representative in G for every left coset of H met by G, with checked programs in the original generators of G.

• reps : Array (Element G)
• distinct : (Array.map (fun (p : Element G) => LeftCoset.mk H p.val) self.reps).toList.Nodup
• covers (p : Element G) : ∃ (i : Fin self.reps.size), LeftCoset.mk H self.reps[↑i].val = LeftCoset.mk H p.val
• 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.ofOrbit {n : Nat} {G H : Group n} (c : Action.Orbit G (LeftCoset H)) (hc : Action.Orbit.Valid (Action.leftCosets G H) (LeftCoset.mk H (Perm.id n)) c) : LeftTransversal G H

Export the representatives discovered by the left coset action.

Equations

• Hex.PermGroup.LeftTransversal.ofOrbit c hc = { reps := c.reps.toArray, distinct := ⋯, covers := ⋯, words := Vector.cast ⋯ c.words, checked := ⋯ }

theorem Hex.PermGroup.LeftTransversal.class_injective {n : Nat} {G H : Group n} (t : LeftTransversal G H) {i j : Fin t.reps.size} (h : LeftCoset.mk H t.reps[↑i].val = LeftCoset.mk H t.reps[↑j].val) : i = j

def Hex.PermGroup.LeftTransversal.product {n : Nat} {G H : Group n} (t : LeftTransversal G H) (h : H.IsSubgroup G) (i : Fin t.reps.size) (p : Element H) : Element G

The unique product of a transversal representative and a subgroup element.

Equations

• t.product h i p = t.reps[↑i].comp ⟨p.val, ⋯⟩

@[simp]

theorem Hex.PermGroup.LeftTransversal.product_class {n : Nat} {G H : Group n} (t : LeftTransversal G H) (h : H.IsSubgroup G) (i : Fin t.reps.size) (p : Element H) : LeftCoset.mk H (t.product h i p).val = LeftCoset.mk H t.reps[↑i].val

theorem Hex.PermGroup.LeftTransversal.product_injective {n : Nat} {G H : Group n} (t : LeftTransversal G H) (h : H.IsSubgroup G) {i j : Fin t.reps.size} {p q : Element H} (he : t.product h i p = t.product h j q) : i = j ∧ p = q

theorem Hex.PermGroup.LeftTransversal.product_surjective {n : Nat} {G H : Group n} (t : LeftTransversal G H) (h : H.IsSubgroup G) (p : Element G) : ∃ (i : Fin t.reps.size), ∃ (q : Element H), t.product h i q = p

def Hex.PermGroup.LeftTransversal.products {n : Nat} {G H : Group n} (t : LeftTransversal G H) (h : H.IsSubgroup G) : List (Element G)

This finite product list is used only in the erased cardinality proof; the executable transversal builder never enumerates either group.

Equations

• t.products h = List.flatMap (fun (i : Fin t.reps.size) => List.map (t.product h i) H.enumerate.toList) (List.finRange t.reps.size)

theorem Hex.PermGroup.LeftTransversal.products_nodup {n : Nat} {G H : Group n} (t : LeftTransversal G H) (h : H.IsSubgroup G) : (t.products h).Nodup

theorem Hex.PermGroup.LeftTransversal.mem_products {n : Nat} {G H : Group n} (t : LeftTransversal G H) (h : H.IsSubgroup G) (p : Element G) : p ∈ t.products h

theorem Hex.PermGroup.LeftTransversal.products_length {n : Nat} {G H : Group n} (t : LeftTransversal G H) (h : H.IsSubgroup G) : (t.products h).length = t.reps.size * H.order

theorem Hex.PermGroup.LeftTransversal.order_eq {n : Nat} {G H : Group n} (t : LeftTransversal G H) (h : H.IsSubgroup G) : G.order = t.reps.size * H.order

Lagrange's formula for the verified transversal, using exact naturals.