def Hex.PermGroup.Search.Predicate.centralizer {n : Nat} (H : Group n) : Predicate n

Commutation is tested on the original generators of the second group.

Equations

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

theorem Hex.PermGroup.Search.Predicate.centralizer_iff {n : Nat} (H : Group n) (p : Perm n) : (centralizer H).test p = true ↔ ∀ (q : Perm n), Generated H.generators q → p.comp q = q.comp p

def Hex.PermGroup.Search.Centralizer.reject {n : Nat} {G : Group n} (H : Group n) (t : Node G) (r : Fin H.generators.size × Fin n) : Bool

Once x is assigned, commutation forces the image of h(x). Reject if that image is outside its remaining suffix orbit. This includes conflicts with an already assigned image, whose suffix orbit is a singleton.

Equations

• Hex.PermGroup.Search.Centralizer.reject H t r = (decide (↑r.snd < t.base) && !t.imagePossible (H.generators[↑r.fst].get r.snd) (H.generators[↑r.fst].get (t.rep.val.get r.snd)))

theorem Hex.PermGroup.Search.Centralizer.reject_sound {n : Nat} {G : Group n} (H : Group n) (t : Node G) (r : Fin H.generators.size × Fin n) (hr : reject H t r = true) (p : Perm n) (hp : t.Contains p) : (Predicate.centralizer H).test p = false

def Hex.PermGroup.Search.Centralizer.constraint {n : Nat} (G H : Group n) : Constraint G (Predicate.centralizer H)

Replay identifies the original generator and assigned source point that forced an impossible image. Discovery follows generator then point order.

Equations

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

def Hex.PermGroup.Group.centralizerSearch {n : Nat} (G H : Group n) : Search.Solution (Search.Centralizer.constraint G H)

Exact centralizer search, with replay of forced-image pruning and complete coverage of every remaining chain branch. H need not be a subgroup of G.

Equations

• G.centralizerSearch H = Hex.PermGroup.Search.solve (Hex.PermGroup.Search.Centralizer.constraint G H)

def Hex.PermGroup.Group.centralizer {n : Nat} (G H : Group n) : Group n

Equations

• G.centralizer H = (G.centralizerSearch H).group

theorem Hex.PermGroup.Group.mem_centralizer {n : Nat} (G H : Group n) (p : Perm n) : Generated (G.centralizer H).generators p ↔ Generated G.generators p ∧ ∀ (q : Perm n), Generated H.generators q → p.comp q = q.comp p

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

The center is the centralizer of the group in itself.

Equations

• G.center = G.centralizer G

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

def Hex.PermGroup.Group.centralizerPerm {n : Nat} (G : Group n) (q : Perm n) : Group n

Centralizing one permutation is centralizing the cyclic group it generates; the permutation itself need not belong to the ambient group.

Equations

• G.centralizerPerm q = G.centralizer (Hex.PermGroup.Group.ofGenerators #[q])

theorem Hex.PermGroup.Group.mem_centralizerPerm {n : Nat} (G : Group n) (q p : Perm n) : Generated (G.centralizerPerm q).generators p ↔ Generated G.generators p ∧ p.comp q = q.comp p