theorem Hex.PermGroup.Generated.commutes {n : Nat} {S : Array (Perm n)} {p q : Perm n} (hq : Generated S q) (h : ∀ (s : Perm n), s ∈ S → p.comp s = s.comp p) : p.comp q = q.comp p

Commutation with generators extends through products and inverses.

def Hex.PermGroup.Group.isNormal {n : Nat} (H G : Group n) (_h : H.IsSubgroup G) : Bool

Test conjugates of original subgroup generators by symmetric ambient generators. Containment is supplied separately, as required for normality.

Equations

• H.isNormal G _h = decide (∀ (i : Fin G.working.generators.size) (j : Fin H.generators.size), H.contains (G.working.generators[↑i].conj H.generators[↑j]) = true)

theorem Hex.PermGroup.Group.isNormal_iff {n : Nat} (H G : Group n) (h : H.IsSubgroup G) : H.isNormal G h = true ↔ ∀ (p q : Perm n), Generated G.generators p → Generated H.generators q → Generated H.generators (p.conj q)

def Hex.PermGroup.Group.isAbelian {n : Nat} (G : Group n) : Bool

Check commutation of the original generator pairs, without enumerating the group.

Equations

• G.isAbelian = decide (∀ (i j : Fin G.generators.size), G.generators[↑i].comp G.generators[↑j] = G.generators[↑j].comp G.generators[↑i])

def Hex.PermGroup.Group.abelianFailure? {n : Nat} (G : Group n) : Option (Fin G.generators.size × Fin G.generators.size)

A noncommuting original generator pair, in deterministic index order.

Equations

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

theorem Hex.PermGroup.Group.abelianFailure_none {n : Nat} (G : Group n) : G.abelianFailure? = none ↔ G.isAbelian = true

theorem Hex.PermGroup.Group.abelianFailure_sound {n : Nat} (G : Group n) (i j : Fin G.generators.size) (h : G.abelianFailure? = some (i, j)) : G.generators[↑i].comp G.generators[↑j] ≠ G.generators[↑j].comp G.generators[↑i]

def Hex.PermGroup.Group.normalFailure? {n : Nat} (H G : Group n) : Option (Fin G.working.generators.size × Fin H.generators.size)

A symmetric ambient generator and original subgroup generator whose conjugate has a failed complete sift in the subgroup.

Equations

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

theorem Hex.PermGroup.Group.normalFailure_none {n : Nat} (H G : Group n) (h : H.IsSubgroup G) : H.normalFailure? G = none ↔ H.isNormal G h = true

theorem Hex.PermGroup.Group.normalFailure_sound {n : Nat} (H G : Group n) (i : Fin G.working.generators.size) (j : Fin H.generators.size) (h : H.normalFailure? G = some (i, j)) : ¬Generated H.generators (G.working.generators[↑i].conj H.generators[↑j])

theorem Hex.PermGroup.Group.isAbelian_iff {n : Nat} (G : Group n) : G.isAbelian = true ↔ ∀ (p q : Perm n), Generated G.generators p → Generated G.generators q → p.comp q = q.comp p

def Hex.PermGroup.Group.isTransitive {n : Nat} (G : Group n) : Bool

Transitivity requires a nonempty action. A singleton is transitive, including when its generator array is empty.

Equations

• G.isTransitive = if hn : 0 < n then have points := G.orbit ⟨0, hn⟩; decide (∀ (b : Fin n), b ∈ points) else false

theorem Hex.PermGroup.Group.isTransitive_iff {n : Nat} (G : Group n) : G.isTransitive = true ↔ 0 < n ∧ ∀ (a b : Fin n), ∃ (p : Perm n), Generated G.generators p ∧ p.get a = b