31.4. Normal structure and products
The complete derived-series result retains and checks every derived subgroup.
The four-point imprimitive C₂ wr C₂ action exposes both factor embeddings and
has order eight.
def symmetric4 : Group 4 := Group.ofGenerators
#[⟨#v[1, 0, 2, 3], ⊢ #v[1, 0, 2, 3].toList.Nodup All goals completed! 🐙, ⊢ ∀ (i : Fin 4), i ∈ #v[1, 0, 2, 3].toList All goals completed! 🐙⟩, rotation]
def derivedOrders :=
symmetric4.derivedSeries.certificate.orders symmetric4
#guard derivedOrders = [24, 12, 4, 1]
def c2Swap : Perm 2 := ⟨#v[1, 0], ⊢ #v[1, 0].toList.Nodup All goals completed! 🐙, ⊢ ∀ (i : Fin 2), i ∈ #v[1, 0].toList All goals completed! 🐙⟩
def c2 : Group 2 := Group.ofGenerators #[c2Swap]
def c2wr2 := c2.wreathProduct c2 (⊢ 0 < 2 All goals completed! 🐙)
#guard c2wr2.order = 8
#guard c2wr2.generators.size = 3
def c2Element : Element c2 :=
⟨c2Swap, .generator (⊢ c2Swap ∈ c2.generators All goals completed! 🐙)⟩
def baseCopy :=
WreathProduct.copy c2 (⊢ 0 < 2 All goals completed! 🐙) 0 c2Element
def topCopy :=
WreathProduct.inr c2 (⊢ 0 < 2 All goals completed! 🐙) c2Element
#guard baseCopy != topCopy
def baseTopIsId : Bool :=
WreathProduct.top (⊢ 0 < 2 All goals completed! 🐙) baseCopy == Element.id c2
#guard baseTopIsId
#guard WreathProduct.top (⊢ 0 < 2 All goals completed! 🐙) topCopy = c2Element
end HexPermGroupChapter