The wreath product C₂ ≀ C₂ and the extension 1 → C₂ → D₁₆ → C₂ ≀ C₂ → 1

The regular wreath product C₂ ≀ C₂ of the cyclic group of order two by itself is the dihedral group of order eight. This file reads it on coordinates: an element is a triple (a, b, c) of elements of ZMod 2, where (a, b) is the base function, evaluated at the identity and at the generator of the top factor, and c is the top coordinate. The multiplication is

(a, b, c) (a', b', c') = (a + a' + c (a' + b'), b + b' + c (a' + b'), c + c'),

so a top coordinate c = 1 exchanges the two base coordinates of the right factor (TauCeti.WreathC2.mk_mul_mk).

The dihedral group D₁₆ = ⟨r, f⟩ of order sixteen, Mathlib's DihedralGroup 8 with f = sr 0, maps onto C₂ ≀ C₂ by r ↦ u s = (1, 0, 1) and f ↦ s = (0, 0, 1), with kernel its centre {1, r⁴}. This makes D₁₆ a central extension of C₂ ≀ C₂ by C₂ (TauCeti.wreathD16Extension). Its factor set at the section (u s)ⁱ sʲ ↦ rⁱ fʲ is a ZMod 2-valued 2-cocycle of C₂ ≀ C₂ with trivial action, computed explicitly on coordinates by TauCeti.wreathD16Cocycle_apply.

By Kahn and Serre (references below), the class of this cocycle is the second Stiefel–Whitney class of the signed-permutation representation C₂ ≀ C₂ ⊂ O₂; that identification is not formalised here. The cocycle is the universal case of the index-two Evens norm: the graph cochain of the tautological character of the base group differs from it by an explicit coboundary (TauCeti.ContCohomology.evensGraphCochain_wreath).

Main definitions

• TauCeti.WreathC2: the regular wreath product C₂ ≀ C₂, with the constructor TauCeti.WreathC2.mk and the coordinates TauCeti.WreathC2.coordA, TauCeti.WreathC2.coordB, TauCeti.WreathC2.coordC.
• TauCeti.wreathSwap: the swap s = (0, 0, 1), the generator of the top factor.
• TauCeti.dihedralToWreath: the quotient map D₁₆ → C₂ ≀ C₂.
• TauCeti.wreathD16Extension: D₁₆ as an extension of C₂ ≀ C₂ by C₂.
• TauCeti.wreathSection: the section (u s)ⁱ sʲ ↦ rⁱ fʲ of that extension.
• TauCeti.wreathD16Cocycle: its factor set, valued in ZMod 2.

Main results

• TauCeti.WreathC2.mk_mul_mk: the multiplication on coordinates.
• TauCeti.dihedralToWreath_eq_one_iff: the kernel of D₁₆ → C₂ ≀ C₂ is {1, r⁴}.
• TauCeti.wreathSection_apply: the section on coordinates.
• TauCeti.wreathSection_mul_wreathSection: the section is multiplicative up to the factor set.
• TauCeti.wreathD16Cocycle_apply: the factor set on coordinates.
• TauCeti.wreathD16Cocycle_isCocycle: the factor set is a 2-cocycle for the trivial action.

References

• B. Kahn, Classes de Stiefel-Whitney de formes quadratiques et de représentations galoisiennes réelles, Invent. Math. 78 (1984), 223–256, th. I.4.2 and Remarque II.2.3: the dihedral group of order eight as C₂ ≀ C₂ with its tautological character, and the extension D₁₆.
• J.-P. Serre, L'invariant de Witt de la forme Tr(x²), Comment. Math. Helv. 59 (1984), 651–676.

@[reducible, inline]

abbrev TauCeti.WreathC2 : Type

The wreath product C₂ ≀ C₂, Mathlib's regular wreath product of the cyclic group of order two, written multiplicatively, by itself. It is the dihedral group of order eight; its elements are read on the coordinates TauCeti.WreathC2.coordA, TauCeti.WreathC2.coordB and TauCeti.WreathC2.coordC.

def TauCeti.WreathC2.mk (a b c : ZMod 2) : WreathC2

The element of C₂ ≀ C₂ with coordinates (a, b, c): the base function takes the value a at the identity and b at the generator, and the top coordinate is c.

def TauCeti.WreathC2.coordA (g : WreathC2) : ZMod 2

The first coordinate of an element of C₂ ≀ C₂: its base function at the identity.

def TauCeti.WreathC2.coordB (g : WreathC2) : ZMod 2

The second coordinate of an element of C₂ ≀ C₂: its base function at the generator.

def TauCeti.WreathC2.coordC (g : WreathC2) : ZMod 2

The third coordinate of an element of C₂ ≀ C₂: its top coordinate.

@[simp]

theorem TauCeti.WreathC2.coordA_mk (a b c : ZMod 2) : (mk a b c).coordA = a

The first coordinate of (a, b, c) is a.

@[simp]

theorem TauCeti.WreathC2.coordB_mk (a b c : ZMod 2) : (mk a b c).coordB = b

The second coordinate of (a, b, c) is b.

@[simp]

theorem TauCeti.WreathC2.coordC_mk (a b c : ZMod 2) : (mk a b c).coordC = c

The third coordinate of (a, b, c) is c.

theorem TauCeti.WreathC2.mk_coordA_coordB_coordC (g : WreathC2) : mk g.coordA g.coordB g.coordC = g

Every element of C₂ ≀ C₂ is the element with its own coordinates.

theorem TauCeti.WreathC2.ext {g h : WreathC2} (hA : g.coordA = h.coordA) (hB : g.coordB = h.coordB) (hC : g.coordC = h.coordC) : g = h

Elements of C₂ ≀ C₂ with the same coordinates are equal.

theorem TauCeti.WreathC2.ext_iff {g h : WreathC2} : g = h ↔ g.coordA = h.coordA ∧ g.coordB = h.coordB ∧ g.coordC = h.coordC

theorem TauCeti.WreathC2.mk_inj {a b c a' b' c' : ZMod 2} : mk a b c = mk a' b' c' ↔ a = a' ∧ b = b' ∧ c = c'

Two elements given by coordinates are equal exactly when their coordinates are.

@[simp]

theorem TauCeti.WreathC2.mk_zero : mk 0 0 0 = 1

The identity of C₂ ≀ C₂ is (0, 0, 0).

@[simp]

theorem TauCeti.WreathC2.coordA_one : coordA 1 = 0

The first coordinate of the identity is 0.

@[simp]

theorem TauCeti.WreathC2.coordB_one : coordB 1 = 0

The second coordinate of the identity is 0.

@[simp]

theorem TauCeti.WreathC2.coordC_one : coordC 1 = 0

The third coordinate of the identity is 0.

theorem TauCeti.WreathC2.mk_mul_mk (a b c a' b' c' : ZMod 2) : mk a b c * mk a' b' c' = mk (a + a' + c * (a' + b')) (b + b' + c * (a' + b')) (c + c')

The multiplication of C₂ ≀ C₂ on coordinates: the top coordinate of the left factor exchanges the two base coordinates of the right factor.

@[simp]

theorem TauCeti.WreathC2.coordA_mul (g h : WreathC2) : (g * h).coordA = g.coordA + h.coordA + g.coordC * (h.coordA + h.coordB)

The first coordinate of a product.

@[simp]

theorem TauCeti.WreathC2.coordB_mul (g h : WreathC2) : (g * h).coordB = g.coordB + h.coordB + g.coordC * (h.coordA + h.coordB)

The second coordinate of a product.

@[simp]

theorem TauCeti.WreathC2.coordC_mul (g h : WreathC2) : (g * h).coordC = g.coordC + h.coordC

The third coordinate is additive: it is the projection to the top factor.

theorem TauCeti.WreathC2.inv_mk (a b c : ZMod 2) : (mk a b c)⁻¹ = mk (a + c * (a + b)) (b + c * (a + b)) c

The inverse on coordinates: (a, b, 0) is its own inverse, and (a, b, 1)⁻¹ = (b, a, 1).

@[simp]

theorem TauCeti.WreathC2.coordA_inv (g : WreathC2) : g⁻¹.coordA = g.coordA + g.coordC * (g.coordA + g.coordB)

The first coordinate of an inverse.

@[simp]

theorem TauCeti.WreathC2.coordB_inv (g : WreathC2) : g⁻¹.coordB = g.coordB + g.coordC * (g.coordA + g.coordB)

The second coordinate of an inverse.

@[simp]

theorem TauCeti.WreathC2.coordC_inv (g : WreathC2) : g⁻¹.coordC = g.coordC

The third coordinate of an inverse.

def TauCeti.wreathBase : Subgroup WreathC2

The base group C₂ × C₂ of C₂ ≀ C₂, the kernel of the projection to the top factor: the elements with third coordinate 0. It has index two (TauCeti.index_wreathBase).

theorem TauCeti.mem_wreathBase_iff {g : WreathC2} : g ∈ wreathBase ↔ g.coordC = 0

The base group consists of the elements with third coordinate 0.

theorem TauCeti.notMem_wreathBase_iff {g : WreathC2} : g ∉ wreathBase ↔ g.coordC = 1

The elements outside the base group are those with third coordinate 1.

def TauCeti.wreathSwap : WreathC2

The swap s = (0, 0, 1) of C₂ ≀ C₂, the generator of the top factor. It lies outside the base group, and multiplying by it on the left exchanges the two base coordinates.

@[simp]

theorem TauCeti.coordA_wreathSwap : wreathSwap.coordA = 0

The first coordinate of the swap is 0.

@[simp]

theorem TauCeti.coordB_wreathSwap : wreathSwap.coordB = 0

The second coordinate of the swap is 0.

@[simp]

theorem TauCeti.coordC_wreathSwap : wreathSwap.coordC = 1

The third coordinate of the swap is 1.

theorem TauCeti.wreathSwap_notMem_wreathBase : wreathSwap ∉ wreathBase

The swap lies outside the base group.

theorem TauCeti.index_wreathBase : wreathBase.index = 2

The base group of C₂ ≀ C₂ has index two.

def TauCeti.wreathTautological : ↥wreathBase →* Multiplicative (ZMod 2)

The tautological character of the base group of C₂ ≀ C₂, its first coordinate.

@[simp]

theorem TauCeti.toAdd_wreathTautological (g : ↥wreathBase) : Multiplicative.toAdd (wreathTautological g) = (↑g).coordA

The tautological character of an element of the base group is its first coordinate.

def TauCeti.dihedralToWreath : DihedralGroup 8 →* WreathC2

The quotient map D₁₆ → C₂ ≀ C₂, r ↦ u s = (1, 0, 1) and f = sr 0 ↦ s = (0, 0, 1). Its kernel is the centre {1, r⁴} of D₁₆ (TauCeti.dihedralToWreath_eq_one_iff).

theorem TauCeti.dihedralToWreath_r_one : dihedralToWreath (DihedralGroup.r 1) = WreathC2.mk 1 0 1

The rotation r of D₁₆ maps to u s = (1, 0, 1).

theorem TauCeti.dihedralToWreath_sr_zero : dihedralToWreath (DihedralGroup.sr 0) = wreathSwap

The reflection f = sr 0 of D₁₆ maps to the swap s = (0, 0, 1).

theorem TauCeti.dihedralToWreath_eq_one_iff (x : DihedralGroup 8) : dihedralToWreath x = 1 ↔ x = 1 ∨ x = DihedralGroup.r 4

The kernel of D₁₆ → C₂ ≀ C₂ is the centre {1, r⁴}.

theorem TauCeti.dihedralToWreath_surjective : Function.Surjective ⇑dihedralToWreath

D₁₆ → C₂ ≀ C₂ is surjective.

def TauCeti.wreathD16Extension : GroupExtension (Multiplicative (ZMod 2)) (DihedralGroup 8) WreathC2

D₁₆ as an extension of C₂ ≀ C₂ by C₂: the kernel C₂ is included as the centre {1, r⁴} of D₁₆, and the projection is TauCeti.dihedralToWreath. The extension is central.

@[simp]

theorem TauCeti.wreathD16Extension_rightHom : wreathD16Extension.rightHom = dihedralToWreath

The projection of TauCeti.wreathD16Extension is TauCeti.dihedralToWreath.

theorem TauCeti.wreathD16Extension_inl_apply (x : Multiplicative (ZMod 2)) : wreathD16Extension.inl x = DihedralGroup.r (4 * ↑(Multiplicative.toAdd x).val)

The kernel of TauCeti.wreathD16Extension is included as x ↦ r^{4x}.

def TauCeti.wreathSection : wreathD16Extension.Section

The section (u s)ⁱ sʲ ↦ rⁱ fʲ of D₁₆ → C₂ ≀ C₂, for 0 ≤ i < 4 and 0 ≤ j < 2, with u s = (1, 0, 1), s = (0, 0, 1) and f = sr 0. It sends the identity to the identity.

theorem TauCeti.wreathSection_apply (g : WreathC2) : wreathSection g = if g.coordC = 0 then if g.coordA = 0 then if g.coordB = 0 then DihedralGroup.r 0 else DihedralGroup.sr 5 else if g.coordB = 0 then DihedralGroup.sr 7 else DihedralGroup.r 2 else if g.coordA = 0 then if g.coordB = 0 then DihedralGroup.sr 0 else DihedralGroup.r 3 else if g.coordB = 0 then DihedralGroup.r 1 else DihedralGroup.sr 6

The section on coordinates. With g = (a, b, c), σ g is the element rⁱ fʲ of D₁₆ lifting g = (u s)ⁱ sʲ, written in Mathlib's r/sr normal form (f = sr 0).

@[simp]

theorem TauCeti.dihedralToWreath_wreathSection (g : WreathC2) : dihedralToWreath (wreathSection g) = g

The section is a right inverse of D₁₆ → C₂ ≀ C₂.

theorem TauCeti.wreathSection_one : wreathSection 1 = 1

The section is normalized: it sends the identity to the identity.

noncomputable def TauCeti.wreathD16Cocycle (q : WreathC2 × WreathC2) : ZMod 2

The D₁₆ extension cocycle c_{D₁₆}: the factor set σ g · σ h · σ (g h)⁻¹ ∈ {1, r⁴} ≅ C₂ of the section σ = TauCeti.wreathSection of TauCeti.wreathD16Extension, read in ZMod 2. Its value on coordinates is TauCeti.wreathD16Cocycle_apply.

theorem TauCeti.wreathSection_mul_wreathSection (g h : WreathC2) : wreathSection g * wreathSection h = DihedralGroup.r (4 * ↑(wreathD16Cocycle (g, h)).val) * wreathSection (g * h)

The section is multiplicative up to the factor set: σ g · σ h = r^{4 c(g, h)} · σ (g h).

theorem TauCeti.wreathD16Cocycle_apply (g h : WreathC2) : wreathD16Cocycle (g, h) = g.coordA * h.coordB + g.coordC * (h.coordA + h.coordB) + g.coordA * g.coordC * (h.coordA + h.coordB) + g.coordC * h.coordA * h.coordB

The D₁₆ extension cocycle on coordinates. With g = (a, b, c) and h = (a', b', c'), c_{D₁₆} (g, h) = a b' + c (a' + b') + a c (a' + b') + c a' b'.

theorem TauCeti.wreathD16Cocycle_isCocycle (g h j : WreathC2) : wreathD16Cocycle (g * h, j) + wreathD16Cocycle (g, h) = wreathD16Cocycle (h, j) + wreathD16Cocycle (g, h * j)

The D₁₆ extension cocycle is a 2-cocycle, in the trivial-action form of groupCohomology.IsCocycle₂; the action is trivial because the extension is central.