theorem Hex.PermGroup.Blocks.Invariant.generated {n : Nat} {S : Array (Perm n)} {R : Fin n → Fin n → Prop} (hS : ∀ (s : Perm n), s ∈ S → s.inv ∈ S) (hR : Invariant S R) {g : Perm n} (hg : Generated S g) (x y : Fin n) : R x y ↔ R (g.get x) (g.get y)

Preservation by symmetric generators extends to the entire group, in both directions. This applies to arbitrary relations, not only partitions.

def Hex.PermGroup.Partition.IsInvariant {n : Nat} (p : Partition n) (G : Group n) : Prop

Every represented group element permutes the blocks.

Equations

• p.IsInvariant G = ∀ (g : Hex.Perm n), Hex.PermGroup.Generated G.generators g → ∀ (x y : Fin n), p.Same x y ↔ p.Same (g.get x) (g.get y)

def Hex.PermGroup.Partition.isInvariant {n : Nat} (p : Partition n) (G : Group n) : Bool

Check the complete chain's symmetric generators on block representatives.

Equations

• p.isInvariant G = Hex.PermGroup.Blocks.checkInvariant G.chain.generators p

theorem Hex.PermGroup.Partition.isInvariant_iff {n : Nat} (p : Partition n) (G : Group n) : p.isInvariant G = true ↔ p.IsInvariant G

def Hex.PermGroup.Group.blocksCert {n : Nat} (G : Group n) (pairs : List (Fin n × Fin n)) : Blocks.Solution G.chain.generators pairs

A seeded minimal block system and its forced-union certificate. The checked chain supplies symmetric generators without recomputing normalization.

Equations

• G.blocksCert pairs = Hex.PermGroup.Blocks.solve G.chain.generators pairs

def Hex.PermGroup.Group.blocks {n : Nat} (G : Group n) (pairs : List (Fin n × Fin n)) : Partition n

Least invariant equivalence relation containing the independent input pairs.

Equations

• G.blocks pairs = (G.blocksCert pairs).partition

theorem Hex.PermGroup.Group.blocks_invariant {n : Nat} (G : Group n) (pairs : List (Fin n × Fin n)) : (G.blocks pairs).IsInvariant G

theorem Hex.PermGroup.Group.blocks_seeds {n : Nat} (G : Group n) (pairs : List (Fin n × Fin n)) (q : Fin n × Fin n) (hq : q ∈ pairs) : (G.blocks pairs).Same q.fst q.snd

theorem Hex.PermGroup.Group.blocks_least {n : Nat} (G : Group n) (pairs : List (Fin n × Fin n)) (R : Fin n → Fin n → Prop) (hR : Equivalence R) (hG : ∀ (g : Perm n), Generated G.generators g → ∀ (x y : Fin n), R x y → R (g.get x) (g.get y)) (hs : ∀ (q : Fin n × Fin n), q ∈ pairs → R q.fst q.snd) : (G.blocks pairs).Refines R

Minimality among all invariant equivalence relations, including relations not supplied as a canonical partition.

@[simp]

theorem Hex.PermGroup.Group.blocks_empty {n : Nat} (G : Group n) : G.blocks [] = Partition.discrete n

theorem Hex.PermGroup.Group.blocks_star {n : Nat} (G : Group n) (a : Fin n) : G.blocks (List.map (fun (b : Fin n) => (a, b)) (List.finRange n)) = Partition.indiscrete n

Joining every point to one point forces the indiscrete partition.