The action on the square root of two in the Pin⁺ lift

The lift pinLift depends on a square root r2 of two. Changing this root to its negative multiplies the lift of w : WreathC2 by (-1) ^ (coordC w).val: only the swap coordinate contributes. Consequently an automorphism sending r2 to (-1) ^ ε.val * r2 acts on the lift by the sign (-1) ^ (ε * coordC w).val.

pinLift_mul_map_mul_inv computes the resulting twisted factor set. In addition to the ordinary dihedral factor set, its exponent contains ε * coordC h. For the induced representation of a quadratic extension, these are the characters of two and of the extension, respectively. This is the cochain calculation that produces the cup-product correction in the Evens norm of a Kummer class.

The naturality statements hold for field homomorphisms; no topology or Galois group is needed.

References

• J.-P. Serre, L'invariant de Witt de la forme Tr(x²), Comment. Math. Helv. 59 (1984), 651–676, 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, Lemme II.2.1.

@[simp]

theorem TauCeti.map_pinT {F : Type u_1} {E : Type u_2} [Field F] [Field E] (φ : F →+* E) (r2 : F) : (pinT r2).map ⇑φ = pinT (φ r2)

The unit vector defining the swap lift is natural under field homomorphisms.

@[simp]

theorem TauCeti.pinT_neg {F : Type u_1} [Field F] (r2 : F) : pinT (-r2) = -pinT r2

Negating the square root of two negates the unit vector defining the swap lift.

@[simp]

theorem TauCeti.map_pinDihedral {F : Type u_1} {E : Type u_2} [Field F] [Field E] [NeZero 2] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (φ : F →+* E) (z : DihedralGroup 8) : ((pinDihedral hr2) z).map ⇑φ = (pinDihedral ⋯) z

The dihedral lift is natural under field homomorphisms, with the square root mapped too.

@[simp]

theorem TauCeti.map_pinLift {F : Type u_1} {E : Type u_2} [Field F] [Field E] [NeZero 2] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (φ : F →+* E) (w : WreathC2) : (pinLift hr2 w).map ⇑φ = pinLift ⋯ w

The section lift is natural under field homomorphisms, with the square root mapped too.

@[simp]

theorem TauCeti.pinLift_neg {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (w : WreathC2) : pinLift ⋯ w = (-1) ^ w.coordC.val • pinLift hr2 w

Changing the square root of two changes a section lift by the sign of its swap coordinate.

theorem TauCeti.map_pinLift_of_map_root {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (φ : F →+* F) (ε : ZMod 2) (hφ : φ r2 = (-1) ^ ε.val * r2) (w : WreathC2) : (pinLift hr2 w).map ⇑φ = (-1) ^ (ε * w.coordC).val • pinLift hr2 w

If a field endomorphism changes the square root of two by a sign, its action on the lift is that sign raised to the swap coordinate.

theorem TauCeti.pinLift_mul_map_mul_inv {F : Type u_1} [Field F] [NeZero 2] {r2 : F} (hr2 : r2 ^ 2 = 2) (φ : F →+* F) (ε : ZMod 2) (hφ : φ r2 = (-1) ^ ε.val * r2) (g h : WreathC2) : pinLift hr2 g * (pinLift hr2 h).map ⇑φ * (pinLift hr2 (g * h))⁻¹ = (-1) ^ (wreathD16Cocycle (g, h) + ε * h.coordC).val • 1

The twisted factor set of the section lift is the dihedral factor set plus the product of the sign of the square root of two with the swap coordinate of the second argument.