The Pin⁺ model of the plane and the lift of C₂ ≀ C₂ to D₁₆

Over a field F with 2 ≠ 0, the Clifford algebra of the plane F² with the unit form ⟨1, 1⟩ is the matrix algebra M₂(F), with generators e₁ = diag(1, −1) and e₂ = [[0, 1], [1, 0]] (TauCeti.pinE1, TauCeti.pinE2): they satisfy e₁² = e₂² = +1 and e₁ e₂ = −e₂ e₁, so that the vector y₀ e₁ + y₁ e₂ (TauCeti.pinVec) squares to y₀² + y₁². The generators and their transport along ring homomorphisms are defined over arbitrary rings. An orthogonal matrix x acts on these vectors by the twisted adjoint action v ↦ det(x) · x v xᵀ; a Pin⁺ lift of w is an orthogonal x whose twisted action is w (TauCeti.IsPinLift). With the sign, a unit vector lifts its own reflection (TauCeti.isPinLift_pinVec). Lifts multiply, invert and are carried by ring homomorphisms, such as a Galois action on the entries; an orthogonal x lifts exactly one w (TauCeti.IsPinLift.unique), and over a domain in which 2 ≠ 0 two lifts of the same w differ by a sign (TauCeti.IsPinLift.eq_or_eq_neg). The sign matrix diag((−1)^{ε₀}, (−1)^{ε₁}) has the diagonal lift e₁^{ε₀} e₂^{ε₁} (TauCeti.pinDiagonalLift), whose products carry the sign (−1)^{ε₁ ε'₀} (TauCeti.pinDiagonalLift_mul).

The wreath product C₂ ≀ C₂ acts on F² by signed permutations (TauCeti.wreathSignedPerm). For a square root r2 of 2, the unit vector t = (e₁ − e₂)/√2 (TauCeti.pinT) lifts the swap, e₁ t = r2⁻¹ · [[1, −1], [1, 1]] has order 8 (over ℝ with r2 = √2 > 0 it is the rotation by π/4), and r ↦ e₁ t, f ↦ t is a homomorphism TauCeti.pinDihedral from the dihedral group D₁₆ of order sixteen into M₂(F). It lies over the quotient map D₁₆ → C₂ ≀ C₂ (TauCeti.isPinLift_pinDihedral), and through the section TauCeti.wreathSection it gives a lift TauCeti.pinLift of C₂ ≀ C₂ whose factor set is the D₁₆ extension cocycle c_{D₁₆} read as a sign (TauCeti.pinLift_mul_mul_inv).

The signs matter. With e_i² = +1 the lift of C₂ ≀ C₂ is the dihedral group D₁₆ of Pin⁺ and not the quaternion group Q₁₆; this is the convention of Mathlib's CliffordAlgebra for the form ⟨1, 1⟩, but not that of CliffordAlgebra.pinGroup, a vector in which has Q v = −1. The model is therefore stated in explicit matrices. It is the model in which Serre's second proof of his Théorème 1′ computes the Evens norm of a Kummer class, at n = 2.

Main definitions

• TauCeti.pinE1, TauCeti.pinE2: the Clifford generators of M₂(R).
• TauCeti.pinVec: the vector y₀ e₁ + y₁ e₂, as a linear map.
• TauCeti.IsPinLift: x is a Pin⁺ lift of w.
• TauCeti.pinDiagonalLift: the lift e₁^{ε₀} e₂^{ε₁} of a diagonal sign matrix.
• TauCeti.wreathSignedPerm: the signed-permutation representation (a, b, c) ↦ diag((−1)^a, (−1)^b) · e₂^c of C₂ ≀ C₂.
• TauCeti.pinT: the unit vector (e₁ − e₂)/√2.
• TauCeti.pinDihedral: the homomorphism D₁₆ → M₂(F), r ↦ e₁ t, f ↦ t.
• TauCeti.pinLift: the lift C₂ ≀ C₂ → M₂(F) through TauCeti.wreathSection.

Main results

• TauCeti.pinE1_mul_self, TauCeti.pinE2_mul_self, TauCeti.pinE1_mul_pinE2, TauCeti.pinVec_mul_self: the Clifford relations.
• TauCeti.isPinLift_pinVec: a unit vector lifts its own reflection.
• TauCeti.isPinLift_iff: a lift is checked on the generators e₁ and e₂.
• TauCeti.wreathSignedPerm_mem_orthogonalGroup: the signed permutations are orthogonal.
• TauCeti.IsPinLift.mul, TauCeti.IsPinLift.inv, TauCeti.IsPinLift.map: lifts multiply, invert, and are natural in the coefficient ring.
• TauCeti.IsPinLift.unique, TauCeti.IsPinLift.eq_or_eq_neg: a lift determines what it lifts, and two lifts of the same matrix differ by a sign.
• TauCeti.isPinLift_pinDiagonalLift, TauCeti.pinDiagonalLift_mul: the diagonal lift and its factor set (−1)^{ε₁ ε'₀}; it is defined over the prime ring (TauCeti.map_pinDiagonalLift).
• TauCeti.pinE1_mul_pinT_pow_four: (e₁ t)⁴ = −1.
• TauCeti.isPinLift_pinDihedral: pinDihedral z lifts the signed permutation of the image of z in C₂ ≀ C₂.
• TauCeti.pinLift_mul_pinLift and TauCeti.pinLift_mul_mul_inv: the factor set of pinLift is (−1)^{c_{D₁₆}}.

References

• J.-P. Serre, L'invariant de Witt de la forme Tr(x²), Comment. Math. Helv. 59 (1984), 651–676: the groups Pin⁺, and the second proof of Théorème 1′.
• B. Kahn, Classes de Stiefel-Whitney de formes quadratiques et de représentations galoisiennes réelles, Invent. Math. 78 (1984), 223–256: the extension D₁₆ of C₂ ≀ C₂.

def TauCeti.pinE1 {R : Type u_1} [Ring R] : Matrix (Fin 2) (Fin 2) R

The first Clifford generator e₁ = diag(1, −1) of M₂(R).

def TauCeti.pinE2 {R : Type u_1} [Ring R] : Matrix (Fin 2) (Fin 2) R

The second Clifford generator e₂ = [[0, 1], [1, 0]] of M₂(R), which is also the permutation matrix of the swap.

theorem TauCeti.pinE1_def {R : Type u_1} [Ring R] : pinE1 = !![1, 0; 0, -1]

The entries of e₁.

theorem TauCeti.pinE2_def {R : Type u_1} [Ring R] : pinE2 = !![0, 1; 1, 0]

The entries of e₂.

@[simp]

theorem TauCeti.pinE1_mul_self {R : Type u_1} [Ring R] : pinE1 * pinE1 = 1

e₁² = +1: with this sign the lift of C₂ ≀ C₂ is D₁₆ and not Q₁₆.

@[simp]

theorem TauCeti.pinE2_mul_self {R : Type u_1} [Ring R] : pinE2 * pinE2 = 1

e₂² = +1.

theorem TauCeti.pinE1_mul_pinE2 {R : Type u_1} [Ring R] : pinE1 * pinE2 = -(pinE2 * pinE1)

e₁ e₂ = −e₂ e₁.

theorem TauCeti.pinE2_mul_diagonal {R : Type u_1} [Ring R] (d : Fin 2 → R) : pinE2 * Matrix.diagonal d = Matrix.diagonal ![d 1, d 0] * pinE2

Conjugating a diagonal matrix by the swap e₂ exchanges its two entries.

def TauCeti.wreathSignedPerm {R : Type u_1} [Ring R] : WreathC2 →* Matrix (Fin 2) (Fin 2) R

The signed-permutation representation of C₂ ≀ C₂, (a, b, c) ↦ diag((−1)^a, (−1)^b) · e₂^c: the base coordinates are signs and the top coordinate swaps the two coordinates of R². Its value on coordinates is TauCeti.wreathSignedPerm_mk.

theorem TauCeti.wreathSignedPerm_apply {R : Type u_1} [Ring R] (g : WreathC2) : wreathSignedPerm g = Matrix.diagonal ![(-1) ^ g.coordA.val, (-1) ^ g.coordB.val] * pinE2 ^ g.coordC.val

The signed permutation of g is diag((−1)^a, (−1)^b) · e₂^c on its coordinates.

@[simp]

theorem TauCeti.wreathSignedPerm_mk {R : Type u_1} [Ring R] (a b c : ZMod 2) : wreathSignedPerm (WreathC2.mk a b c) = Matrix.diagonal ![(-1) ^ a.val, (-1) ^ b.val] * pinE2 ^ c.val

The signed permutation of (a, b, c) is diag((−1)^a, (−1)^b) · e₂^c.

@[simp]

theorem TauCeti.wreathSignedPerm_wreathSwap {R : Type u_1} [Ring R] : wreathSignedPerm wreathSwap = pinE2

The swap s = (0, 0, 1) acts as the permutation matrix e₂.

def TauCeti.pinDiagonalLift {R : Type u_1} [Ring R] (ε : Fin 2 → ZMod 2) : Matrix (Fin 2) (Fin 2) R

The diagonal lift e₁^{ε₀} e₂^{ε₁} of the sign matrix diag((−1)^{ε₀}, (−1)^{ε₁}) (TauCeti.isPinLift_pinDiagonalLift).

theorem TauCeti.pinDiagonalLift_def {R : Type u_1} [Ring R] (ε : Fin 2 → ZMod 2) : pinDiagonalLift ε = pinE1 ^ (ε 0).val * pinE2 ^ (ε 1).val

The diagonal lift of ε is e₁^{ε₀} e₂^{ε₁}.

@[simp]

theorem TauCeti.pinDiagonalLift_zero {R : Type u_1} [Ring R] : pinDiagonalLift 0 = 1

The diagonal lift of the trivial sign is the identity.

@[simp]

theorem TauCeti.pinDiagonalLift_mul {R : Type u_1} [Ring R] (ε ε' : Fin 2 → ZMod 2) : pinDiagonalLift ε * pinDiagonalLift ε' = (-1) ^ (ε 1 * ε' 0).val * pinDiagonalLift (ε + ε')

The product of two diagonal lifts, e₁^a e₂^b · e₁^{a'} e₂^{b'} = (−1)^{b a'} e₁^{a + a'} e₂^{b + b'}: this is where e₁² = e₂² = +1 and e₁ e₂ = −e₂ e₁ enter.

@[simp]

theorem TauCeti.map_pinE1 {R : Type u_1} [Ring R] {S : Type u_2} [Ring S] (φ : R →+* S) : pinE1.map ⇑φ = pinE1

The generator e₁ is defined over the prime ring.

@[simp]

theorem TauCeti.map_pinE2 {R : Type u_1} [Ring R] {S : Type u_2} [Ring S] (φ : R →+* S) : pinE2.map ⇑φ = pinE2

The generator e₂ is defined over the prime ring.

@[simp]

theorem TauCeti.map_pinDiagonalLift {R : Type u_1} [Ring R] {S : Type u_2} [Ring S] (φ : R →+* S) (ε : Fin 2 → ZMod 2) : (pinDiagonalLift ε).map ⇑φ = pinDiagonalLift ε

The diagonal lift is defined over the prime ring.

def TauCeti.pinVec {R : Type u_1} [CommRing R] : (Fin 2 → R) →ₗ[R] Matrix (Fin 2) (Fin 2) R

The vector y₀ e₁ + y₁ e₂ of the plane R² inside its Clifford model M₂(R).

theorem TauCeti.pinVec_apply {R : Type u_1} [CommRing R] (y : Fin 2 → R) : pinVec y = y 0 • pinE1 + y 1 • pinE2

The vector pinVec y is y₀ e₁ + y₁ e₂.

theorem TauCeti.pinVec_eq {R : Type u_1} [CommRing R] (y : Fin 2 → R) : pinVec y = !![y 0, y 1; y 1, -y 0]

The vector y₀ e₁ + y₁ e₂ is the symmetric matrix [[y₀, y₁], [y₁, −y₀]].

theorem TauCeti.pinVec_injective {R : Type u_1} [CommRing R] : Function.Injective ⇑pinVec

A vector of the Clifford model determines its coordinates.

@[simp]

theorem TauCeti.pinVec_mul_self {R : Type u_1} [CommRing R] (y : Fin 2 → R) : pinVec y * pinVec y = (y ⬝ᵥ y) • 1

The Clifford relation v² = q(v) · 1 for the unit form q(y) = y₀² + y₁².

theorem TauCeti.pinVec_mul_add_pinVec_mul {R : Type u_1} [CommRing R] (y z : Fin 2 → R) : pinVec y * pinVec z + pinVec z * pinVec y = (2 * y ⬝ᵥ z) • 1

The polarized Clifford relation u v + v u = 2 ⟨u, v⟩ · 1.

@[simp]

theorem TauCeti.pinVec_transpose {R : Type u_1} [CommRing R] (y : Fin 2 → R) : (pinVec y).transpose = pinVec y

The vectors of the Clifford model are symmetric matrices.

theorem TauCeti.wreathSignedPerm_mem_orthogonalGroup {R : Type u_1} [CommRing R] (g : WreathC2) : wreathSignedPerm g ∈ Matrix.orthogonalGroup (Fin 2) R

The signed permutations are orthogonal: diag((−1)^a, (−1)^b) · e₂^c has orthonormal rows.

@[simp]

theorem TauCeti.det_pinVec {R : Type u_1} [CommRing R] (y : Fin 2 → R) : (pinVec y).det = -(y ⬝ᵥ y)

The determinant of the vector y is −q(y) = −(y₀² + y₁²).

structure TauCeti.IsPinLift {R : Type u_1} [CommRing R] (x w : Matrix (Fin 2) (Fin 2) R) : Prop

x is a Pin⁺ lift of w: x is orthogonal and its twisted adjoint action v ↦ det(x) · x v xᵀ on the vectors TauCeti.pinVec y is w. Over a field an orthogonal 2 × 2 matrix is even when its determinant is 1 and odd when it is −1, so this action is v ↦ (−1)^{|x|} x v x⁻¹; without the sign, e₁ would act as diag(1, −1), the reflection in the wrong line.

This is not Mathlib's CliffordAlgebra.pinGroup: a vector in that group has Q v = −1 and squares to −1, which lifts C₂ ≀ C₂ to the quaternion group Q₁₆ rather than to D₁₆.

• mem_orthogonalGroup : x ∈ Matrix.orthogonalGroup (Fin 2) R

  A Pin⁺ lift is orthogonal.

• det_smul_mul_pinVec_mul_transpose (y : Fin 2 → R) : x.det • (x * pinVec y * x.transpose) = pinVec (w.mulVec y)

  The twisted adjoint action of a Pin⁺ lift of w on vectors is w.

theorem TauCeti.IsPinLift.one {R : Type u_1} [CommRing R] : IsPinLift 1 1

The identity lifts the identity.

theorem TauCeti.IsPinLift.mul {R : Type u_1} [CommRing R] {x w x' w' : Matrix (Fin 2) (Fin 2) R} (h : IsPinLift x w) (h' : IsPinLift x' w') : IsPinLift (x * x') (w * w')

Lifts multiply.

theorem TauCeti.IsPinLift.pow {R : Type u_1} [CommRing R] {x w : Matrix (Fin 2) (Fin 2) R} (h : IsPinLift x w) (n : ℕ) : IsPinLift (x ^ n) (w ^ n)

Lifts are compatible with powers.

theorem TauCeti.isPinLift_pinVec {R : Type u_1} [CommRing R] {u : Fin 2 → R} (hu : u ⬝ᵥ u = 1) : IsPinLift (pinVec u) (1 - 2 • Matrix.vecMulVec u u)

A unit vector lifts its own reflection v ↦ v − 2 ⟨u, v⟩ u: the vector u squares to 1, has determinant −1, and u v u = 2 ⟨u, v⟩ u − v by the Clifford relation.

theorem TauCeti.isPinLift_pinE1 {R : Type u_1} [CommRing R] : IsPinLift pinE1 (Matrix.diagonal ![-1, 1])

e₁ lifts diag(−1, 1), the reflection in the second coordinate axis.

theorem TauCeti.isPinLift_pinE2 {R : Type u_1} [CommRing R] : IsPinLift pinE2 (Matrix.diagonal ![1, -1])

e₂ lifts diag(1, −1), the reflection in the first coordinate axis.

theorem TauCeti.isPinLift_pinDiagonalLift {R : Type u_1} [CommRing R] (ε : Fin 2 → ZMod 2) : IsPinLift (pinDiagonalLift ε) (Matrix.diagonal fun (i : Fin 2) => (-1) ^ (ε i).val)

The diagonal lift e₁^{ε₀} e₂^{ε₁} lifts diag((−1)^{ε₀}, (−1)^{ε₁}), since e₁ lifts diag(−1, 1) and e₂ lifts diag(1, −1).

theorem TauCeti.isPinLift_iff {R : Type u_1} [CommRing R] {x w : Matrix (Fin 2) (Fin 2) R} : IsPinLift x w ↔ x ∈ Matrix.orthogonalGroup (Fin 2) R ∧ x.det • (x * pinE1 * x.transpose) = pinVec (w.transpose 0) ∧ x.det • (x * pinE2 * x.transpose) = pinVec (w.transpose 1)

A Pin⁺ lift is checked on the two generators: x lifts w if and only if x is orthogonal and its twisted action sends e₁ and e₂ to the vectors of the two columns of w.

theorem TauCeti.IsPinLift.unique {R : Type u_1} [CommRing R] {x w w' : Matrix (Fin 2) (Fin 2) R} (h : IsPinLift x w) (h' : IsPinLift x w') : w = w'

The target of a Pin⁺ lift is unique: an orthogonal x has only one twisted action.

theorem TauCeti.IsPinLift.inv {R : Type u_1} [CommRing R] {x w : Matrix (Fin 2) (Fin 2) R} (h : IsPinLift x w) : IsPinLift x⁻¹ w⁻¹

Lifts invert: the inverse x⁻¹ = xᵀ of a lift of w lifts w⁻¹.

@[simp]

theorem TauCeti.map_pinVec {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (φ : R →+* S) (y : Fin 2 → R) : (pinVec y).map ⇑φ = pinVec (⇑φ ∘ y)

The vector y₀ e₁ + y₁ e₂ is natural in the coefficient ring.

theorem TauCeti.IsPinLift.map {R : Type u_1} [CommRing R] {S : Type u_2} [CommRing S] (φ : R →+* S) {x w : Matrix (Fin 2) (Fin 2) R} (h : IsPinLift x w) : IsPinLift (x.map ⇑φ) (w.map ⇑φ)

Lifts are carried by ring homomorphisms, in particular by a Galois action on the entries.

theorem TauCeti.IsPinLift.eq_or_eq_neg {R : Type u_1} [CommRing R] [IsDomain R] [NeZero 2] {x x' w : Matrix (Fin 2) (Fin 2) R} (h : IsPinLift x w) (h' : IsPinLift x' w) : x' = x ∨ x' = -x

Two Pin⁺ lifts of the same w differ by a sign: x' x⁻¹ lifts the identity, hence is ±1.

noncomputable def TauCeti.pinT {F : Type u_1} [Field F] (r2 : F) : Matrix (Fin 2) (Fin 2) F

The unit vector t = (e₁ − e₂)/√2 of the Clifford model, for a square root r2 of 2. Its reflection is the swap of the two coordinates (TauCeti.isPinLift_pinT).

theorem TauCeti.pinT_def {F : Type u_1} [Field F] (r2 : F) : pinT r2 = r2⁻¹ • (pinE1 - pinE2)

t = r2⁻¹ (e₁ − e₂).

@[simp]

theorem TauCeti.pinT_mul_self {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) : pinT r2 * pinT r2 = 1

t² = +1.

theorem TauCeti.isPinLift_pinT {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) : IsPinLift (pinT r2) pinE2

t lifts the swap e₂, its reflection.

theorem TauCeti.pinE1_mul_pinT_pow_four {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) : (pinE1 * pinT r2) ^ 4 = -1

(e₁ t)⁴ = −1, since e₁ t = r2⁻¹ · [[1, −1], [1, 1]] squares to [[0, −1], [1, 0]]. So e₁ t has order 8, the characteristic not being two; over ℝ with r2 = √2 > 0 it is the rotation by π/4.

noncomputable def TauCeti.pinDihedral {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) : DihedralGroup 8 →* Matrix (Fin 2) (Fin 2) F

The dihedral group D₁₆ in M₂(F), on Mathlib's DihedralGroup 8: r ↦ e₁ t, of order 8 (the rotation by π/4 over ℝ with r2 = √2 > 0), and f = sr 0 ↦ t, so that r i ↦ (e₁ t)^i and sr i ↦ t (e₁ t)^i (TauCeti.pinDihedral_r, TauCeti.pinDihedral_sr). It is TauCeti.dihedralHom at the two involutions t and t e₁ t, whose product e₁ t satisfies (e₁ t)⁸ = 1 by TauCeti.pinE1_mul_pinT_pow_four.

@[simp]

theorem TauCeti.pinDihedral_r {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (i : ZMod 8) : (pinDihedral hr2) (DihedralGroup.r i) = (pinE1 * pinT r2) ^ i.val

The rotation r i maps to (e₁ t)^i.

@[simp]

theorem TauCeti.pinDihedral_sr {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (i : ZMod 8) : (pinDihedral hr2) (DihedralGroup.sr i) = pinT r2 * (pinE1 * pinT r2) ^ i.val

The reflection sr i maps to t (e₁ t)^i.

theorem TauCeti.pinDihedral_r_four {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) : (pinDihedral hr2) (DihedralGroup.r 4) = -1

The central element r⁴ of D₁₆ maps to −1.

theorem TauCeti.isPinLift_pinDihedral {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (z : DihedralGroup 8) : IsPinLift ((pinDihedral hr2) z) (wreathSignedPerm (dihedralToWreath z))

D₁₆ lies over C₂ ≀ C₂: pinDihedral z is a Pin⁺ lift of the signed permutation of the image of z under TauCeti.dihedralToWreath.

noncomputable def TauCeti.pinLift {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (g : WreathC2) : Matrix (Fin 2) (Fin 2) F

The lift of C₂ ≀ C₂ into D₁₆ through the section TauCeti.wreathSection, (u s)ⁱ sʲ ↦ (e₁ t)ⁱ tʲ. It lifts the signed permutations (TauCeti.isPinLift_pinLift), and its factor set is (−1)^{c_{D₁₆}} (TauCeti.pinLift_mul_mul_inv).

theorem TauCeti.pinLift_def {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (g : WreathC2) : pinLift hr2 g = (pinDihedral hr2) (wreathSection g)

pinLift g is the image under TauCeti.pinDihedral of the section value wreathSection g.

@[simp]

theorem TauCeti.pinLift_one {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) : pinLift hr2 1 = 1

The lift is normalized.

theorem TauCeti.isPinLift_pinLift {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (g : WreathC2) : IsPinLift (pinLift hr2 g) (wreathSignedPerm g)

pinLift g is a Pin⁺ lift of the signed permutation of g.

theorem TauCeti.pinLift_mul_pinLift {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (g h : WreathC2) : pinLift hr2 g * pinLift hr2 h = (-1) ^ (wreathD16Cocycle (g, h)).val * pinLift hr2 (g * h)

pinLift is multiplicative up to the sign (−1)^{c_{D₁₆}}: pinLift g · pinLift h = (−1)^{c_{D₁₆}(g, h)} · pinLift (g h), the image of TauCeti.wreathSection_mul_wreathSection under TauCeti.pinDihedral, which sends r⁴ to −1.

theorem TauCeti.pinLift_mul_mul_inv {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (g h : WreathC2) : pinLift hr2 g * pinLift hr2 h * (pinLift hr2 (g * h))⁻¹ = (-1) ^ (wreathD16Cocycle (g, h)).val

The factor set of pinLift is c_{D₁₆}, the D₁₆ extension cocycle TauCeti.wreathD16Cocycle read as a sign: pinLift g · pinLift h · pinLift (g h)⁻¹ = (−1)^{c_{D₁₆}(g, h)}.