The discriminant of a transferred line

Let L/K be a finite extension and s : L → K a K-linear functional. The Scharlau transfer of the line ⟨a⟩ over L is the form x ↦ s(a x²) on L regarded as a K-space, with Gram matrix (s(a bᵢ bⱼ))ᵢⱼ in a basis b. Since s(a bᵢ bⱼ) = s(bᵢ · a bⱼ), that matrix is the Gram matrix of s_*⟨1⟩ multiplied by the matrix of multiplication by a, whose determinant is the norm of a. Hence

d(s_*⟨a⟩) = d(s_*⟨1⟩) · N_{L/K}(a)   modulo squares.

Read through the Kummer isomorphism, this is the degree-one case of the relative Stiefel–Whitney formula for the transfer.

Main results

• QuadraticMap.discr_scharlauTransfer_smul_sq: the Gram determinant of s_*⟨a⟩ in any basis is N_{L/K}(a) times that of s_*⟨1⟩.
• TauCeti.discr_formClass_scharlauTransfer_smul_sq: the discriminant of s_*⟨a⟩ is that of s_*⟨1⟩ plus the square class of N_{L/K}(a).
• TauCeti.RegularFormClass.discr_scharlauTransfer_mk_rankOne: the same identity on isometry classes, for the class-level transfer of the class ⟨a⟩.

References

• W. Scharlau, Quadratic and Hermitian Forms (1985), Chapter 2, §5.
• 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 QuadraticMap.discr_scharlauTransfer_smul_sq {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] [Algebra K L] [Invertible 2] {ι : Type u_3} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι K L) (s : L →ₗ[K] K) (a : L) : QuadraticForm.discr b ((a • sq).scharlauTransfer s) = (Algebra.norm K) a * QuadraticForm.discr b (sq.scharlauTransfer s)

The Gram determinant of a transferred line: in any basis of L over K, the Gram determinant of x ↦ s(a x²) is N_{L/K}(a) times the Gram determinant of x ↦ s(x²).

theorem TauCeti.discr_formClass_scharlauTransfer_smul_sq {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (s : L →ₗ[K] K) (a : Lˣ) (ha : QuadraticMap.Nondegenerate) (h1 : QuadraticMap.Nondegenerate) : (formClass ((↑a • QuadraticMap.sq).scharlauTransfer s) ha).discr = (formClass (QuadraticMap.sq.scharlauTransfer s) h1).discr + squareClass ((Algebra.normUnits K) a)

The discriminant of a transferred line: d(s_*⟨a⟩) = d(s_*⟨1⟩) + [N_{L/K}(a)] in the additively written square-class group of K, for the transferred forms x ↦ s(a x²) and x ↦ s(x²) on L regarded as a K-space.

theorem TauCeti.RegularFormClass.discr_scharlauTransfer_mk_rankOne {K : Type u_1} {L : Type u_2} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (s : L →ₗ[K] K) (hs : s ≠ 0) (a : Lˣ) : ((scharlauTransfer s hs) ⟦⟨1, fun (x : Fin 1) => a⟩⟧).discr = ((scharlauTransfer s hs) 1).discr + squareClass ((Algebra.normUnits K) a)

The discriminant of the transfer of ⟨a⟩: d(s_*⟨a⟩) = d(s_*⟨1⟩) + [N_{L/K}(a)] on isometry classes.