inductive Hex.PermGroup.Derived.Member {n : Nat} (G : Group n) : Perm n → Prop

The subgroup generated by commutators of all ambient elements.

• id {n : Nat} {G : Group n} : Member G (Perm.id n)
• comm {n : Nat} {G : Group n} {p q : Perm n} : Generated G.generators p → Generated G.generators q → Member G (p.comm q)
• comp {n : Nat} {G : Group n} {p q : Perm n} : Member G p → Member G q → Member G (p.comp q)
• inv {n : Nat} {G : Group n} {p : Perm n} : Member G p → Member G p.inv

theorem Hex.PermGroup.Derived.Member.conj {n : Nat} {G : Group n} {p g : Perm n} (hp : Member G p) (hg : Generated G.generators g) : Member G (g.conj p)

def Hex.PermGroup.Derived.seeds {n : Nat} (G : Group n) : Array (Perm n)

Original generator-pair commutators in first-occurrence order, omitting identities and duplicates. Removing this redundancy prevents repeated squaring of the presentation size in a derived series.

Equations

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

theorem Hex.PermGroup.Derived.mem_seeds {n : Nat} (G : Group n) (r : Perm n) : r ∈ seeds G ↔ (∃ (p : Perm n), p ∈ G.generators ∧ ∃ (q : Perm n), q ∈ G.generators ∧ p.comm q = r) ∧ r ≠ Perm.id n

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

Equations

• Hex.PermGroup.Derived.seedGroup G = Hex.PermGroup.Group.ofGenerators (Hex.PermGroup.Derived.seeds G)

theorem Hex.PermGroup.Derived.seed_comm {n : Nat} (G : Group n) (p : Perm n) (hp : p ∈ G.generators) (q : Perm n) (hq : q ∈ G.generators) : Generated (seedGroup G).generators (p.comm q)

theorem Hex.PermGroup.Derived.seed_inside {n : Nat} (G : Group n) : (seedGroup G).IsSubgroup G

theorem Hex.PermGroup.Derived.seed_member {n : Nat} (G : Group n) (p : Perm n) (hp : Generated (seedGroup G).generators p) : Member G p

def Hex.PermGroup.Group.derivedCert {n : Nat} (G : Group n) : Normal.Closure G (Derived.seedGroup G)

A complete normal-closure trace starting from original generator-pair commutators. The trace proves that no extra elements were introduced.

Equations

• G.derivedCert = G.normalClosureCert (Hex.PermGroup.Derived.seedGroup G) ⋯

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

Equations

• G.derived = G.derivedCert.group

theorem Hex.PermGroup.Group.derived_inside {n : Nat} (G : Group n) : G.derived.IsSubgroup G

theorem Hex.PermGroup.Group.derived_normal {n : Nat} (G : Group n) : G.derived.isNormal G ⋯ = true

theorem Hex.PermGroup.Group.generator_comm_mem {n : Nat} (G : Group n) (p : Perm n) (hp : p ∈ G.generators) (q : Perm n) (hq : q ∈ G.generators) : Generated G.derived.generators (p.comm q)

theorem Hex.PermGroup.Group.comm_mem_derived {n : Nat} (G : Group n) (p q : Perm n) (hp : Generated G.generators p) (hq : Generated G.generators q) : Generated G.derived.generators (p.comm q)

theorem Hex.PermGroup.Group.mem_derived {n : Nat} (G : Group n) (p : Perm n) : Generated G.derived.generators p ↔ Derived.Member G p

The finite generator construction equals the subgroup generated by all element commutators, in both directions.

theorem Hex.PermGroup.Group.derived_le {n : Nat} (G N : Group n) : G.derived.IsSubgroup N ↔ ∀ (p q : Perm n), Generated G.generators p → Generated G.generators q → Generated N.generators (p.comm q)

The derived subgroup is the least subgroup containing all commutators; the candidate subgroup need not be assumed normal.

theorem Hex.PermGroup.Group.IsSubgroup.derived {n : Nat} {G H : Group n} (h : H.IsSubgroup G) : H.derived.IsSubgroup G.derived