theorem Hex.PermGroup.Partition.eq_discrete {n : Nat} (p : Partition n) : p = discrete n ↔ ∀ (x y : Fin n), p.Same x y → x = y

theorem Hex.PermGroup.Partition.eq_indiscrete {n : Nat} (p : Partition n) : p = indiscrete n ↔ ∀ (x y : Fin n), p.Same x y

theorem Hex.PermGroup.Partition.IsInvariant.nonsingleton {n : Nat} {p : Partition n} {G : Group n} (hp : p.IsInvariant G) (ht : G.isTransitive = true) (hd : p ≠ discrete n) (a : Fin n) : ∃ (b : Fin n), b ≠ a ∧ p.Same a b

Transitivity transports a nonsingleton block to the block through any chosen point. Thus every nondiscrete invariant partition is detected there.

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

Primitive actions have degree at least two, are transitive, and admit only the discrete and indiscrete invariant partitions.

Equations

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

theorem Hex.PermGroup.Group.primitive_criterion {n : Nat} (G : Group n) (hn : 2 ≤ n) (ht : G.isTransitive = true) (a : Fin n) : G.IsPrimitive ↔ ∀ (b : Fin n), b ≠ a → G.blocks [(a, b)] = Partition.indiscrete n

The fixed-point seeded criterion is equivalent to the full invariant partition condition. Transitivity is essential to the reverse direction.