def Hex.PermGroup.LeftTransversal.cosets {n : Nat} {G H : Group n} (t : LeftTransversal G H) : Array (LeftCoset H)

Equations

• t.cosets = Array.map (fun (p : Hex.PermGroup.Element G) => Hex.PermGroup.LeftCoset.mk H p.val) t.reps

@[simp]

theorem Hex.PermGroup.LeftTransversal.cosets_size {n : Nat} {G H : Group n} (t : LeftTransversal G H) : t.cosets.size = t.reps.size

theorem Hex.PermGroup.LeftTransversal.mem_cosets {n : Nat} {G H : Group n} (t : LeftTransversal G H) (p : Element G) : LeftCoset.mk H p.val ∈ t.cosets

theorem Hex.PermGroup.LeftTransversal.cosets_invariant {n : Nat} {G H : Group n} (t : LeftTransversal G H) (p : Element G) (x : LeftCoset H) (hx : x ∈ t.cosets) : (Action.leftCosets G H).act p x ∈ t.cosets

theorem Hex.PermGroup.LeftTransversal.cosets_domain {n : Nat} {G H : Group n} (t : LeftTransversal G H) : (Action.leftCosets G H).Domain t.cosets

theorem Hex.PermGroup.LeftTransversal.cosets_fixed {n : Nat} {G H : Group n} (t : LeftTransversal G H) (p : Element G) : (∀ (x : LeftCoset H), x ∈ t.cosets → (Action.leftCosets G H).act p x = x) ↔ Core.Member G H p.val

Fixing every left coset is exactly membership in every ambient conjugate of the subgroup. No normality assumption is made on the input.

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

The full coset action image and its kernel, retaining the exact checked transversal used to number the cosets.

• transversal : LeftTransversal G H
• image : (Action.leftCosets G H).Image self.transversal.cosets
• kernel : (Action.leftCosets G H).Kernel self.transversal.cosets

def Hex.PermGroup.CosetAction.ofTransversal {n : Nat} {G H : Group n} (t : LeftTransversal G H) : CosetAction G H

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.PermGroup.CosetAction.kernel_eq_core {n : Nat} {G H : Group n} (a : CosetAction G H) (h : H.IsSubgroup G) : SameGroup a.kernel.group (G.core H h)

theorem Hex.PermGroup.CosetAction.map_eq_id {n : Nat} {G H : Group n} (a : CosetAction G H) (h : H.IsSubgroup G) (p : Element G) : a.image.map p = Element.id a.image.group ↔ Generated (G.core H h).generators p.val

def Hex.PermGroup.Group.cosetAction {n : Nat} (G H : Group n) (h : H.IsSubgroup G) (cap : Nat) : Except SizeLimit (CosetAction G H)

Reject insufficient capacity before allocating the transversal or its action permutations. The kernel is the subgroup core in the original degree.

Equations

• G.cosetAction H h cap = if G.index H h ≤ cap then Except.ok (Hex.PermGroup.CosetAction.ofTransversal (G.leftTransversal H h)) else Except.error { required := G.index H h, capacity := cap }

theorem Hex.PermGroup.Group.cosetAction_ok {n : Nat} (G H : Group n) (h : H.IsSubgroup G) (cap : Nat) : (∃ (a : CosetAction G H), G.cosetAction H h cap = Except.ok a) ↔ G.index H h ≤ cap