Documentation

TauCeti.FieldTheory.GaloisCohomology.MuTwo.TwistedBoundary

The twisted boundary of the Pin⁺ lift of a Kummer representation #

Let K be a field in which 2 ≠ 0, let L/K be a quadratic extension with an embedding σ : L → Kˢ, let a ∈ Lˣ, and let ρ_a = Ind α_a : G_K → C₂ ≀ C₂ be the representation induced from the Kummer character of a on G_L (TauCeti.kummerInd). Through the signed-permutation representation C₂ ≀ C₂ ⊂ O₂, it is the action of G_K on the roots of X² − σ a and of its conjugate. For a square root r2 of 2 in Kˢ, composing ρ_a with the lift TauCeti.pinLift : C₂ ≀ C₂ → D₁₆ ⊂ M₂(Kˢ) gives a lift \tilde{ρ}_a of ρ_a to Pin⁺ (TauCeti.kummerIndLift).

The matrix \tilde{ρ}_a(g) has entries in Kˢ, on which G_K acts, so \tilde{ρ}_a has a twisted boundary δ(\tilde{ρ}_a)(g, h) = \tilde{ρ}_a(g) · g(\tilde{ρ}_a(h)) · \tilde{ρ}_a(g h)⁻¹ (TauCeti.twistedBoundary). Two signs enter it. The factor set of pinLift is the D₁₆ extension cocycle c_{D₁₆}; and g fixes e₁ and e₂ but sends t = (e₁ − e₂)/√2 to ±t according to the sign rootSign r2 g of √2, so it multiplies pinLift w by (−1)^{rootSign r2 g · c(w)}, where c(w) is the swap coordinate of w (TauCeti.map_pinLift_galois). The swap coordinate of ρ_a(h) is the character of G_K with kernel G_L, which is rootSign (σ x) h for any x ∈ L ∖ K (TauCeti.coordC_kummerInd, in TauCeti.FieldTheory.GaloisCohomology.MuTwo.EvensNorm). Hence, as an identity of matrices,

δ(\tilde{ρ}_a)(g, h) = (−1)^{c_{D₁₆}(ρ_a g, ρ_a h) + rootSign √2 g · rootSign x h}

(TauCeti.twistedBoundary_kummerIndLift): for x a square root of the discriminant d of L/K, this is δ(\tilde{ρ}_a) = ρ_a^* c_{D₁₆} + (2) ∪ (d) at cochain level. The 𝔽₂-reading of the twisted boundary (TauCeti.twistedBoundaryF2) records its exponent (TauCeti.twistedBoundaryF2_kummerIndLift).

This is the cochain identity by which Serre's second proof of his Théorème 1′ compares the Evens norm N^{Ev}((a)), the class of ρ_a^* c_{D₁₆}, with the second Stiefel–Whitney class of the trace form Tr_*⟨a⟩: the correction (2) ∪ (d) involves the discriminant of L/K, and not that of Tr_*⟨a⟩.

Main definitions #

Main results #

References #

The Galois action on the lift #

source
theorem TauCeti.map_pinLift_galois {K : Type u} [Field K] [NeZero 2] {r2 : SeparableClosure K} (hr2 : r2 ^ 2 = 2) (g : AbsoluteGaloisGroup K) (w : WreathC2) :
(pinLift hr2 w).map ⇑g = (-1) ^ (rootSign r2 g * w.coordC).val * pinLift hr2 w

The Galois action on the lift pinLift: g ∈ G_K fixes e₁ and e₂ and sends t = (e₁ − e₂)/√2 to (−1)^{rootSign r2 g} t, since g r2 = ±r2; so it multiplies pinLift w by (−1)^{rootSign r2 g · c(w)}, where c(w) is the top coordinate of w, which counts the factors t.

Frame changes and sign twists #

source
theorem TauCeti.twistedBoundary_pinDiagonalLift_rootSign {K : Type u} [Field K] {c : Fin 2 → SeparableClosure K} {w : Fin 2 → K} (hc : ∀ (i : Fin 2), c i ^ 2 = (algebraMap K (SeparableClosure K)) (w i)) (g h : AbsoluteGaloisGroup K) :
twistedBoundary (fun (g : AbsoluteGaloisGroup K) => pinDiagonalLift fun (i : Fin 2) => rootSign (c i) g) (g, h) = (-1) ^ (rootSign (c 1) g * rootSign (c 0) h).val

The twisted boundary of a diagonal lift of Kummer characters is a cup product: if c₀², c₁² ∈ K, the twisted boundary of g ↦ e₁^{rootSign c₀ g} e₂^{rootSign c₁ g} is (g, h) ↦ (−1)^{rootSign c₁ g · rootSign c₀ h}, the sign of the cup product of the Kummer characters of c₁² and c₀².

The lift of the Kummer representation #

source
noncomputable def TauCeti.kummerIndLift {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [NeZero 2] (σ : 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) (g : AbsoluteGaloisGroup K) :
Matrix (Fin 2) (Fin 2) (SeparableClosure K)

The lift \tilde{ρ}_a = pinLift ∘ ρ_a of the representation ρ_a = kummerInd σ hdeg a r hr s hs into D₁₆ ⊂ M₂(Kˢ), for a square root r2 of 2 in Kˢ.

Instances For
    source
    theorem TauCeti.kummerIndLift_def {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [NeZero 2] (σ : 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) (g : AbsoluteGaloisGroup K) :
    kummerIndLift σ hdeg a r hr s hs hr2 g = pinLift hr2 ((kummerInd σ hdeg a r hr s hs) g)

    \tilde{ρ}_a(g) is the pinLift of ρ_a(g).

    source
    theorem TauCeti.twistedBoundary_kummerIndLift {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [NeZero 2] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) {x : L} (hx : x ∉ Set.range ⇑(algebraMap K L)) (a : Lˣ) (r : SeparableClosure K) (hr : r ^ 2 = σ ↑a) (s : AbsoluteGaloisGroup K) (hs : s ∉ galoisSubgroup K L σ) {r2 : SeparableClosure K} (hr2 : r2 ^ 2 = 2) (g h : AbsoluteGaloisGroup K) :
    twistedBoundary (kummerIndLift σ hdeg a r hr s hs hr2) (g, h) = (-1) ^ (wreathD16Cocycle ((kummerInd σ hdeg a r hr s hs) g, (kummerInd σ hdeg a r hr s hs) h) + rootSign r2 g * rootSign (σ x) h).val

    δ(\tilde{ρ}_a) = ρ_a^* c_{D₁₆} + (2) ∪ (d) at cochain level, as an identity of matrices: δ(\tilde{ρ}_a)(g, h) = (−1)^{c_{D₁₆}(ρ_a g, ρ_a h) + rootSign √2 g · rootSign x h} for a generator x of L = K(x), such as a square root of the discriminant d. The factor set of pinLift is c_{D₁₆} (TauCeti.pinLift_mul_mul_inv), g twists pinLift w by the sign (−1)^{rootSign √2 g · c(w)} (TauCeti.map_pinLift_galois), and the top coordinate of ρ_a h is rootSign (σ x) h (TauCeti.coordC_kummerInd). This (2) ∪ (d) is Serre's (2)(d_E): it is the discriminant of L/K that enters, and not that of Tr_*⟨a⟩.

    source
    theorem TauCeti.twistedBoundaryF2_kummerIndLift {K : Type u} [Field K] {L : Type u} [Field L] [Algebra K L] [FiniteDimensional K L] [NeZero 2] (σ : L →ₐ[K] SeparableClosure K) (hdeg : Module.finrank K L = 2) {x : L} (hx : x ∉ Set.range ⇑(algebraMap K L)) (a : Lˣ) (r : SeparableClosure K) (hr : r ^ 2 = σ ↑a) (s : AbsoluteGaloisGroup K) (hs : s ∉ galoisSubgroup K L σ) {r2 : SeparableClosure K} (hr2 : r2 ^ 2 = 2) (g h : AbsoluteGaloisGroup K) :
    twistedBoundaryF2 (kummerIndLift σ hdeg a r hr s hs hr2) (g, h) = wreathD16Cocycle ((kummerInd σ hdeg a r hr s hs) g, (kummerInd σ hdeg a r hr s hs) h) + rootSign r2 g * rootSign (σ x) h

    δ(\tilde{ρ}_a) = ρ_a^* c_{D₁₆} + (2) ∪ (d) at cochain level, in 𝔽₂: the twisted boundary of \tilde{ρ}_a, read in 𝔽₂, is c_{D₁₆}(ρ_a g, ρ_a h) + rootSign √2 g · rootSign x h.