The first Stiefel–Whitney class of a transferred line

Let L/K be a finite extension of fields in which 2 is invertible, s : L → K a nonzero K-linear functional, and a ∈ Lˣ with Kummer class x = (a) ∈ H¹(G_L, 𝔽₂). The first Stiefel–Whitney class of the Scharlau transfer of the line ⟨a⟩ is

w₁(s_*⟨a⟩) = w₁(s_*⟨1⟩) + cor(x),

where cor : H¹(G_L, 𝔽₂) → H¹(G_K, 𝔽₂) is corestriction along any K-embedding of L into a separable closure of K. For the trace of a finite separable extension this is the degree-one part of Kahn's relative Stiefel–Whitney formula for Tr_*⟨a⟩.

Since w₁ is the Kummer class of the discriminant, the formula is the discriminant identity d(s_*⟨a⟩) = d(s_*⟨1⟩) · N_{L/K}(a) (TauCeti.discr_formClass_scharlauTransfer_smul_sq) read through the Kummer isomorphism, together with the law cor (a) = (N_{L/K} a) (TauCeti.galoisCor_kummerClass).

Main results

• TauCeti.sw1Class_scharlauTransfer_mk_rankOne: w₁(s_*⟨a⟩) = w₁(s_*⟨1⟩) + cor (a) for the class-level transfer along a nonzero functional.
• TauCeti.sw1Class_traceTransfer_mk_rankOne: w₁(Tr_*⟨a⟩) = w₁(Tr_*⟨1⟩) + cor (a) for a finite separable extension.
• TauCeti.sw1Class_formClass_scharlauTransfer_smul_sq and TauCeti.sw1Class_formClass_traceTransfer_smul_sq: the same identity for the transferred forms x ↦ s(a x²) and x ↦ s(x²) on L themselves, in particular for the twisted trace forms.
• TauCeti.sw1_eq_add_galoisCor_of_equivalent_scharlauTransfer and TauCeti.sw1_eq_add_galoisCor_of_equivalent_traceTransfer: the identity read on diagonal presentations: if s_*⟨1⟩ ≅ ⟨t₁, …, tₘ⟩ and s_*⟨a⟩ ≅ ⟨b₁, …, bₙ⟩, then ∑ⱼ (bⱼ) = ∑ᵢ (tᵢ) + cor (a). This is the form in which the formula is applied to an explicit diagonalization of the two transferred forms over a fixed base field.

References

• B. Kahn, Classes de Stiefel-Whitney de formes quadratiques et de représentations galoisiennes réelles, Invent. Math. 78 (1984), 223–256, Théorème 2.

theorem TauCeti.sw1Class_scharlauTransfer_mk_rankOne {K L : Type u} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (s : L →ₗ[K] K) (hs : s ≠ 0) (a : Lˣ) : sw1Class ((RegularFormClass.scharlauTransfer s hs) ⟦⟨1, fun (x : Fin 1) => a⟩⟧) = sw1Class ((RegularFormClass.scharlauTransfer s hs) 1) + (CategoryTheory.ConcreteCategory.hom (galoisCor K L σ 1)) (kummerClass a)

The first Stiefel–Whitney class of a transferred line: for a nonzero functional s : L → K and a ∈ Lˣ, w₁(s_*⟨a⟩) = w₁(s_*⟨1⟩) + cor (a), with corestriction taken along any K-embedding σ of L into a separable closure of K.

theorem TauCeti.sw1Class_formClass_scharlauTransfer_smul_sq {K L : Type u} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (s : L →ₗ[K] K) (a : Lˣ) (ha : QuadraticMap.Nondegenerate) (h1 : QuadraticMap.Nondegenerate) : sw1Class (formClass ((↑a • QuadraticMap.sq).scharlauTransfer s) ha) = sw1Class (formClass (QuadraticMap.sq.scharlauTransfer s) h1) + (CategoryTheory.ConcreteCategory.hom (galoisCor K L σ 1)) (kummerClass a)

The first Stiefel–Whitney class of a transferred line, on the forms themselves: for a K-linear functional s : L → K and a ∈ Lˣ, the first Stiefel–Whitney classes of the regular forms x ↦ s(a x²) and x ↦ s(x²) on L differ by cor (a). Regularity of the two forms is a hypothesis.

theorem TauCeti.sw1Class_formClass_traceTransfer_smul_sq {K L : Type u} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (a : Lˣ) (ha : QuadraticMap.Nondegenerate) (h1 : QuadraticMap.Nondegenerate) : sw1Class (formClass (QuadraticMap.traceTransfer K (↑a • QuadraticMap.sq)) ha) = sw1Class (formClass (QuadraticMap.traceTransfer K QuadraticMap.sq) h1) + (CategoryTheory.ConcreteCategory.hom (galoisCor K L σ 1)) (kummerClass a)

The relative Stiefel–Whitney formula in degree one, on the trace forms themselves: for a finite extension L/K and a ∈ Lˣ, the first Stiefel–Whitney classes of the regular forms x ↦ Tr_{L/K}(a x²) and x ↦ Tr_{L/K}(x²) on L differ by cor (a). Regularity of the two forms is a hypothesis; it forces L/K to be separable.

theorem TauCeti.sw1_eq_add_galoisCor_of_equivalent_scharlauTransfer {K L : Type u} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (s : L →ₗ[K] K) (a : Lˣ) {m n : ℕ} {t : Fin m → Kˣ} {b : Fin n → Kˣ} (ht : QuadraticMap.Equivalent (QuadraticMap.sq.scharlauTransfer s) (QuadraticMap.weightedSumSquares K fun (i : Fin m) => ↑(t i))) (hb : QuadraticMap.Equivalent ((↑a • QuadraticMap.sq).scharlauTransfer s) (QuadraticMap.weightedSumSquares K fun (i : Fin n) => ↑(b i))) : sw1 b = sw1 t + (CategoryTheory.ConcreteCategory.hom (galoisCor K L σ 1)) (kummerClass a)

The relative Stiefel–Whitney formula in degree one, on diagonal presentations: for a K-linear functional s : L → K and a ∈ Lˣ, if the transferred forms x ↦ s(x²) and x ↦ s(a x²) on L are isometric to ⟨t₁, …, tₘ⟩ and ⟨b₁, …, bₙ⟩, then ∑ⱼ (bⱼ) = ∑ᵢ (tᵢ) + cor (a). No regularity hypothesis is needed: isometry with a diagonal form with unit coefficients already makes both transferred forms regular.

theorem TauCeti.sw1_eq_add_galoisCor_of_equivalent_traceTransfer {K L : Type u} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) (a : Lˣ) {m n : ℕ} {t : Fin m → Kˣ} {b : Fin n → Kˣ} (ht : QuadraticMap.Equivalent (QuadraticMap.traceTransfer K QuadraticMap.sq) (QuadraticMap.weightedSumSquares K fun (i : Fin m) => ↑(t i))) (hb : QuadraticMap.Equivalent (QuadraticMap.traceTransfer K (↑a • QuadraticMap.sq)) (QuadraticMap.weightedSumSquares K fun (i : Fin n) => ↑(b i))) : sw1 b = sw1 t + (CategoryTheory.ConcreteCategory.hom (galoisCor K L σ 1)) (kummerClass a)

The relative Stiefel–Whitney formula in degree one, on diagonal presentations of the trace forms: for a finite extension L/K and a ∈ Lˣ, if Tr_*⟨1⟩ ≅ ⟨t₁, …, tₘ⟩ and Tr_*⟨a⟩ ≅ ⟨b₁, …, bₙ⟩, then ∑ⱼ (bⱼ) = ∑ᵢ (tᵢ) + cor (a).

theorem TauCeti.sw1Class_traceTransfer_mk_rankOne {K L : Type u} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Invertible 2] (σ : L →ₐ[K] SeparableClosure K) [Algebra.IsSeparable K L] (a : Lˣ) : sw1Class ((RegularFormClass.traceTransfer K) ⟦⟨1, fun (x : Fin 1) => a⟩⟧) = sw1Class ((RegularFormClass.traceTransfer K) 1) + (CategoryTheory.ConcreteCategory.hom (galoisCor K L σ 1)) (kummerClass a)

The relative Stiefel–Whitney formula in degree one: for a finite separable extension L/K and a ∈ Lˣ, w₁(Tr_*⟨a⟩) = w₁(Tr_*⟨1⟩) + cor (a), with corestriction taken along any K-embedding σ of L into a separable closure of K.