Twisted boundaries of matrix-valued Galois cochains

For a matrix-valued one-cochain x of the absolute Galois group, its twisted boundary is

δx(g, h) = x(g) · g(x(h)) · x(gh)⁻¹.

This is the nonabelian boundary used to compare lifts of orthogonal Galois cocycles. Changing a cochain by the Galois-twisted conjugation x(g) ↦ Q⁻¹ x(g) g(Q) conjugates its boundary by the constant matrix Q. In particular, a scalar boundary is unchanged. The mod-two reading twistedBoundaryF2 records whether the boundary is the identity; when K has characteristic different from two, n is nonempty, and the boundary is a sign matrix ±1, this is its exponent.

The convention for the order of the Galois action is important: applying h to the entries and then g is the action of g * h. This is the convention of Gal(SeparableClosure K / K) and is the one needed for the descent cocycles of transferred quadratic forms.

Main definitions

• TauCeti.twistedBoundary: the matrix-valued twisted boundary.
• TauCeti.twistedBoundaryF2: its mod-two reading, the exponent of a sign boundary away from characteristic two when n is nonempty.

Main results

• TauCeti.twistedBoundary_conj: twisted conjugation conjugates the boundary by the constant matrix.
• TauCeti.twistedBoundary_conj_of_eq_scalar: a scalar boundary is invariant under twisted conjugation.
• TauCeti.twistedBoundary_conj_eq_iff: conjugation preserves a boundary commuting with the frame.
• TauCeti.twistedBoundary_neg_one_pow_mul: a sign twist changes the boundary by a coboundary.

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.

noncomputable def TauCeti.twistedBoundary {K : Type u} [Field K] {n : Type u_1} [Fintype n] [DecidableEq n] (x : AbsoluteGaloisGroup K → Matrix n n (SeparableClosure K)) (q : AbsoluteGaloisGroup K × AbsoluteGaloisGroup K) : Matrix n n (SeparableClosure K)

The twisted boundary of a matrix-valued one-cochain of the absolute Galois group: δx(g, h) = x(g) · g(x(h)) · x(gh)⁻¹.

theorem TauCeti.twistedBoundary_apply {K : Type u} [Field K] {n : Type u_1} [Fintype n] [DecidableEq n] (x : AbsoluteGaloisGroup K → Matrix n n (SeparableClosure K)) (g h : AbsoluteGaloisGroup K) : twistedBoundary x (g, h) = x g * (x h).map ⇑g * (x (g * h))⁻¹

The defining equation for the twisted boundary.

@[simp]

theorem TauCeti.twistedBoundary_one {K : Type u} [Field K] {n : Type u_1} [Fintype n] [DecidableEq n] (g h : AbsoluteGaloisGroup K) : twistedBoundary (fun (x : AbsoluteGaloisGroup K) => 1) (g, h) = 1

The twisted boundary of the constant identity cochain is the identity matrix.

theorem TauCeti.twistedBoundary_eq_one_iff {K : Type u} [Field K] {n : Type u_1} [Fintype n] [DecidableEq n] (x : AbsoluteGaloisGroup K → Matrix n n (SeparableClosure K)) (g h : AbsoluteGaloisGroup K) (hx : IsUnit (x (g * h)).det) : twistedBoundary x (g, h) = 1 ↔ x g * (x h).map ⇑g = x (g * h)

The twisted boundary is the identity exactly when the cochain satisfies the multiplicative one-cocycle equation at (g, h).

noncomputable def TauCeti.twistedBoundaryF2 {K : Type u} [Field K] {n : Type u_1} [Fintype n] [DecidableEq n] (x : AbsoluteGaloisGroup K → Matrix n n (SeparableClosure K)) (q : AbsoluteGaloisGroup K × AbsoluteGaloisGroup K) : ZMod 2

The twisted boundary read in 𝔽₂: it is 0 at the identity and 1 elsewhere. When K has characteristic different from two, n is nonempty, and the boundary is a sign matrix ±1, this is precisely its exponent.

@[simp]

theorem TauCeti.twistedBoundaryF2_eq_zero_iff {K : Type u} [Field K] {n : Type u_1} [Fintype n] [DecidableEq n] (x : AbsoluteGaloisGroup K → Matrix n n (SeparableClosure K)) (q : AbsoluteGaloisGroup K × AbsoluteGaloisGroup K) : twistedBoundaryF2 x q = 0 ↔ twistedBoundary x q = 1

The mod-two twisted boundary vanishes exactly when the matrix boundary is the identity.

@[simp]

theorem TauCeti.twistedBoundaryF2_eq_one_iff {K : Type u} [Field K] {n : Type u_1} [Fintype n] [DecidableEq n] (x : AbsoluteGaloisGroup K → Matrix n n (SeparableClosure K)) (q : AbsoluteGaloisGroup K × AbsoluteGaloisGroup K) : twistedBoundaryF2 x q = 1 ↔ twistedBoundary x q ≠ 1

The mod-two twisted boundary is 1 exactly when the matrix boundary is not the identity.

theorem TauCeti.twistedBoundaryF2_eq_of_eq_sign {K : Type u} [Field K] {n : Type u_1} [Fintype n] [DecidableEq n] [Nonempty n] [NeZero 2] (x : AbsoluteGaloisGroup K → Matrix n n (SeparableClosure K)) (q : AbsoluteGaloisGroup K × AbsoluteGaloisGroup K) (e : ZMod 2) (hx : twistedBoundary x q = (-1) ^ e.val • 1) : twistedBoundaryF2 x q = e

For a sign boundary, the mod-two twisted boundary recovers its exponent.

theorem TauCeti.twistedBoundary_conj {K : Type u} [Field K] {n : Type u_1} [Fintype n] [DecidableEq n] (x : AbsoluteGaloisGroup K → Matrix n n (SeparableClosure K)) (Q : Matrix n n (SeparableClosure K)) (hQ : IsUnit Q.det) (g h : AbsoluteGaloisGroup K) : twistedBoundary (fun (j : AbsoluteGaloisGroup K) => Q⁻¹ * x j * Q.map ⇑j) (g, h) = Q⁻¹ * twistedBoundary x (g, h) * Q

Twisted conjugation of a cochain conjugates its boundary by the constant matrix.

theorem TauCeti.twistedBoundary_conj_of_eq_scalar {K : Type u} [Field K] {n : Type u_1} [Fintype n] [DecidableEq n] (x : AbsoluteGaloisGroup K → Matrix n n (SeparableClosure K)) (Q : Matrix n n (SeparableClosure K)) (hQ : IsUnit Q.det) (g h : AbsoluteGaloisGroup K) (a : SeparableClosure K) (hx : twistedBoundary x (g, h) = a • 1) : twistedBoundary (fun (j : AbsoluteGaloisGroup K) => Q⁻¹ * x j * Q.map ⇑j) (g, h) = a • 1

A scalar twisted boundary is unchanged by twisted conjugation.

theorem TauCeti.twistedBoundary_conj_eq_iff {K : Type u} [Field K] {n : Type u_1} [Fintype n] [DecidableEq n] (x : AbsoluteGaloisGroup K → Matrix n n (SeparableClosure K)) {Q S : Matrix n n (SeparableClosure K)} (hQ : IsUnit Q.det) (hS : Commute S Q) (q : AbsoluteGaloisGroup K × AbsoluteGaloisGroup K) : twistedBoundary (fun (g : AbsoluteGaloisGroup K) => Q⁻¹ * x g * Q.map ⇑g) q = S ↔ twistedBoundary x q = S

A change of frame does not change a twisted boundary commuting with it: for an invertible matrix Q and a matrix S commuting with Q (for instance a scalar such as a sign (−1)^n), the twisted boundary of g ↦ Q⁻¹ · x(g) · g(Q) is S exactly where that of x is.

theorem TauCeti.twistedBoundary_neg_one_pow_mul {K : Type u} [Field K] {n : Type u_1} [Fintype n] [DecidableEq n] (x : AbsoluteGaloisGroup K → Matrix n n (SeparableClosure K)) (ψ : AbsoluteGaloisGroup K → ZMod 2) (g h : AbsoluteGaloisGroup K) : twistedBoundary (fun (g : AbsoluteGaloisGroup K) => (-1) ^ (ψ g).val * x g) (g, h) = (-1) ^ (ψ h - ψ (g * h) + ψ g).val * twistedBoundary x (g, h)

A sign twist changes the twisted boundary by a coboundary: multiplying a cochain x by the signs (−1)^{ψ(g)} multiplies its twisted boundary by (−1)^{∂ψ}, where ∂ψ(g, h) = ψ(h) − ψ(g h) + ψ(g) is the coboundary of ψ : G_K → 𝔽₂.