Documentation

TauCeti.FieldTheory.QuadraticForm.StiefelWhitney.Evens.Kummer.TwistedBoundary

The twisted boundary of the Kummer lift in a diagonal frame #

Let L/K be a separable quadratic extension, σ : L → Kˢ a K-embedding, a ∈ Lˣ, and let ρ_a : G_K → C₂ ≀ C₂ ⊂ O₂(Kˢ) be the signed-permutation representation of TauCeti.kummerInd. For a square root √2 ∈ Kˢ of 2, its lift \tilde{ρ}_a = pinLift ∘ ρ_a into Pin⁺ (TauCeti.kummerIndLift) has a twisted boundary δ(\tilde{ρ}_a) with values ±1 (TauCeti.twistedBoundary).

Let (y₀, y₁) be an orthogonal basis of the transferred form Tr_*⟨a⟩, with values w_j = Tr_{L/K}(a y_j²), and let c_j ∈ Kˢ be square roots of the w_j. The frame P of y (TauCeti.kummerFrame) conjugates ρ_a into the diagonal cocycle of the Kummer characters of w₀ and w₁ (TauCeti.kummerFrame_conj). This file transports that diagonalization to the twisted boundary:

δ(\tilde{ρ}_a)(g, h) = rootSign c₁ g · rootSign c₀ h + ∂ψ(g, h)

in 𝔽₂, for a continuous ψ : G_K → 𝔽₂ (TauCeti.twistedBoundaryF2_kummerIndLift_cohomologous), that is, δ(\tilde{ρ}_a) is cohomologous to the cup product (w₁) ∪ (w₀) at cochain level.

The argument is Serre's. P has a Pin⁺ lift \tilde{P} (TauCeti.exists_isPinLift), and changing frame by \tilde{P} conjugates the twisted boundary by \tilde{P} (TauCeti.twistedBoundary_conj), which leaves the scalar δ(\tilde{ρ}_a) unchanged. The conjugated cochain g ↦ \tilde{P}⁻¹ \tilde{ρ}_a(g) g(\tilde{P}) and the diagonal lift g ↦ e₁^{rootSign c₀ g} e₂^{rootSign c₁ g} both lift the diagonal cocycle, so they differ by a sign (−1)^{ψ(g)} (TauCeti.IsPinLift.eq_or_eq_neg), which is locally constant in g. The twisted boundary of the diagonal lift is the cup product (TauCeti.twistedBoundary_pinDiagonalLift_rootSign) and the sign changes it by ∂ψ (TauCeti.twistedBoundary_neg_one_pow_mul).

Together with TauCeti.twistedBoundaryF2_kummerIndLift, this shows that the pullback ρ_a^* c_{D₁₆}, whose class is the Evens norm N^{Ev}((a)), is cohomologous to (w₁) ∪ (w₀) + (2) ∪ (d).

Main results #

References #

theorem TauCeti.twistedBoundaryF2_kummerIndLift_cohomologous {K : Type u} [Field K] [NeZero 2] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) (a : Lˣ) (r : SeparableClosure K) (hr : r ^ 2 = σ ↑a) (s : AbsoluteGaloisGroup K) (hs : s ∉ galoisSubgroup K L σ) {r2 : SeparableClosure K} (hr2 : r2 ^ 2 = 2) (y : Fin 2 → L) (hy : (Algebra.trace K L) (↑a * y 0 * y 1) = 0) (c : Fin 2 → SeparableClosure K) (hc : ∀ (i : Fin 2), c i ^ 2 = (algebraMap K (SeparableClosure K)) ((Algebra.trace K L) (↑a * y i ^ 2))) (hc0 : ∀ (i : Fin 2), c i ≠ 0) :
∃ (ψ : AbsoluteGaloisGroup K → ZMod 2), Continuous ψ ∧ ∀ (g h : AbsoluteGaloisGroup K), twistedBoundaryF2 (kummerIndLift σ hdeg a r hr s hs hr2) (g, h) = rootSign (c 1) g * rootSign (c 0) h + (ψ h - ψ (g * h) + ψ g)

The twisted boundary of the Kummer lift is cohomologous to a cup product. Let y be an orthogonal basis of Tr_*⟨a⟩, with values w_j = Tr_{L/K}(a y_j²), and let c_j ∈ Kˢ be nonzero square roots of the w_j. Then there is a continuous ψ : G_K → 𝔽₂ with δ(\tilde{ρ}_a)(g, h) = rootSign c₁ g · rootSign c₀ h + (ψ h − ψ (g h) + ψ g) in 𝔽₂: the twisted boundary of \tilde{ρ}_a = kummerIndLift σ hdeg a r hr s hs hr2 is cohomologous to the cup product (w₁) ∪ (w₀) at cochain level.