The two-by-two wreath product in the symmetric group on four points

The imprimitive action of the cyclic group of order two, wreath itself, permutes four points. Its faithful image has order eight and index three in S₄, hence is a Sylow two-subgroup, and it carries the transitive-group label 4T3 of the dihedral group of order eight. The action is not primitive: its two fibres of two points are nontrivial blocks. We write the cyclic group as Multiplicative (ZMod 2): its group law is addition modulo two.

noncomputable def TauCeti.wreathTwoToPermFour : WreathProduct (Multiplicative (ZMod 2)) (Fin 2) →* Equiv.Perm (Fin 4)

The imprimitive action of C₂ ≀ S₂ on two blocks of two points, transported to Fin 4.

Equations

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

theorem TauCeti.wreathTwoToPermFour_injective : Function.Injective ⇑wreathTwoToPermFour

The imprimitive action on four points is faithful.

theorem TauCeti.not_isPreprimitive_range_wreathTwoToPermFour : ¬MulAction.IsPreprimitive (↥wreathTwoToPermFour.range) (Fin 4)

The imprimitive action of C₂ ≀ S₂ on four points is not primitive: its two fibres of two points are nontrivial blocks.

theorem TauCeti.natCard_range_wreathTwoToPermFour : Nat.card ↥wreathTwoToPermFour.range = 8

The image of C₂ ≀ S₂ in S₄ has order eight.

@[simp]

theorem TauCeti.index_range_wreathTwoToPermFour : wreathTwoToPermFour.range.index = 3

The image of C₂ ≀ S₂ has index three in S₄.

noncomputable def TauCeti.wreathTwoSylowFour : Sylow 2 (Equiv.Perm (Fin 4))

The image of C₂ ≀ S₂ is a Sylow two-subgroup of S₄.

Equations

• TauCeti.wreathTwoSylowFour = TauCeti.wreathTwoSylowFour._proof_1✝.toSylow TauCeti.wreathTwoSylowFour._proof_2✝

@[simp]

theorem TauCeti.wreathTwoSylowFour_toSubgroup : ↑wreathTwoSylowFour = wreathTwoToPermFour.range

noncomputable def TauCeti.wreathTwoSylowFourEquiv : WreathProduct (Multiplicative (ZMod 2)) (Fin 2) ≃* ↥↑wreathTwoSylowFour

The two-by-two wreath product is canonically isomorphic to its Sylow image in S₄.

Equations

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

@[simp]

theorem TauCeti.coe_wreathTwoSylowFourEquiv (w : WreathProduct (Multiplicative (ZMod 2)) (Fin 2)) : ↑(wreathTwoSylowFourEquiv w) = wreathTwoToPermFour w

The Sylow isomorphism agrees with the imprimitive permutation action.

theorem TauCeti.transitiveGroupLabel_wreathTwoToPermFour : TransitiveGroupLabel ⟨2, transitiveGroupLabel_wreathTwoToPermFour._proof_1⟩ wreathTwoToPermFour.range

The Sylow image of the two-by-two wreath product has the transitive-group label 4T3.