Trace transfer in a quadratic algebra

If x generates a degree-two algebra over a field and x² = d, the basis (1, x) identifies the trace transfer of the unit line with ⟨2, 2d⟩. This supplies the general degree-two version of the trace-form calculation, with an explicit isometry whose coordinates can be used to compute invariants of transferred forms.

The trace of x vanishes by Algebra.IsQuadraticExtension.trace_eq_zero_of_sq_eq, which also covers split and nonreduced algebras.

For a quadratic field extension the file also diagonalizes the twisted trace forms Tr_*⟨a⟩ : y ↦ Tr (a y²), the transfers of the rank-one forms ⟨a⟩ that Kahn's formula for the Stiefel–Whitney classes of a transferred form evaluates. There are two cases.

• If Tr a ≠ 0, Kahn's basis (1, x / a) is orthogonal, and Tr_*⟨a⟩ ≅ ⟨Tr a, d · Tr a / N a⟩ (equivalent_traceTransfer_smul_sq_weightedSumSquares_of_sq).
• If Tr a = 0 and a ≠ 0, then 1 and a⁻¹ are isotropic and Tr_*⟨a⟩ is the hyperbolic plane (equivalent_traceTransfer_smul_sq_hyperbolicPlane).

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.

theorem TauCeti.traceTransfer_sq_basisRepr {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {x : L} {d : K} (hfin : Module.finrank K L = 2) (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) d) : QuadraticMap.basisRepr (QuadraticMap.traceTransfer K QuadraticMap.sq) (quadraticExtensionBasis K L hx hfin) = QuadraticMap.weightedSumSquares K ![2, 2 * d]

In square-root coordinates, the trace transfer of the unit line is ⟨2, 2d⟩.

noncomputable def TauCeti.traceTransferSqIsometryEquivWeightedSumSquaresOfSq {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {x : L} {d : K} (hfin : Module.finrank K L = 2) (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) d) : QuadraticMap.IsometryEquiv (QuadraticMap.traceTransfer K QuadraticMap.sq) (QuadraticMap.weightedSumSquares K ![2, 2 * d])

The square-root coordinate map is an isometry from the transferred unit line to the diagonal form ⟨2, 2d⟩.

@[simp]

theorem TauCeti.traceTransferSqIsometryEquivWeightedSumSquaresOfSq_apply {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {x : L} {d : K} (hfin : Module.finrank K L = 2) (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) d) (z : L) : (traceTransferSqIsometryEquivWeightedSumSquaresOfSq hfin hx hx2) z = (quadraticExtensionBasis K L hx hfin).equivFun z

The isometry uses coordinates in the square-root basis.

@[simp]

theorem TauCeti.traceTransferSqIsometryEquivWeightedSumSquaresOfSq_symm_apply {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {x : L} {d : K} (hfin : Module.finrank K L = 2) (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) d) (v : Fin 2 → K) : (traceTransferSqIsometryEquivWeightedSumSquaresOfSq hfin hx hx2).symm v = (quadraticExtensionBasis K L hx hfin).equivFun.symm v

The inverse isometry reconstructs an element from its square-root coordinates.

theorem TauCeti.equivalent_traceTransfer_sq_weightedSumSquares_of_sq {K : Type u_1} {L : Type u_2} [Field K] [CommRing L] [Algebra K L] {x : L} {d : K} (hfin : Module.finrank K L = 2) (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) d) : QuadraticMap.Equivalent (QuadraticMap.traceTransfer K QuadraticMap.sq) (QuadraticMap.weightedSumSquares K ![2, 2 * d])

The trace transfer of the unit line in a degree-two algebra generated by x² = d is equivalent to ⟨2, 2d⟩.

theorem TauCeti.equivalent_traceTransfer_smul_sq_weightedSumSquares_of_sq {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] [Invertible 2] {x : L} {d : K} (hfin : Module.finrank K L = 2) (hx : x ∉ Set.range ⇑(algebraMap K L)) (hx2 : x ^ 2 = (algebraMap K L) d) {a : L} (htr : (Algebra.trace K L) a ≠ 0) : QuadraticMap.Equivalent (QuadraticMap.traceTransfer K (a • QuadraticMap.sq)) (QuadraticMap.weightedSumSquares K ![(Algebra.trace K L) a, d * (Algebra.trace K L) a / (Algebra.norm K) a])

Kahn's basis. Let x ∉ K generate a quadratic extension L/K with x² = d, and let a : L have nonzero trace. Then 1 and x / a are orthogonal for the twisted trace form Tr_*⟨a⟩ : y ↦ Tr (a y²), with values Tr a and Tr (d / a) = d · Tr a / N a, so Tr_*⟨a⟩ ≅ ⟨Tr a, d · Tr a / N a⟩.

The hypothesis Tr a ≠ 0 cannot be dropped: at Tr a = 0 both entries vanish, while for a ≠ 0 the form is the hyperbolic plane (equivalent_traceTransfer_smul_sq_hyperbolicPlane).

theorem TauCeti.equivalent_traceTransfer_smul_sq_hyperbolicPlane {K : Type u_3} {L : Type u_4} [Field K] [Field L] [Algebra K L] [Invertible 2] (hfin : Module.finrank K L = 2) {a : L} (ha : a ≠ 0) (htr : (Algebra.trace K L) a = 0) : QuadraticMap.Equivalent (QuadraticMap.traceTransfer K (a • QuadraticMap.sq)) (hyperbolicPlane K)

The twisted trace form at trace zero. If L/K is a quadratic extension and a ≠ 0 has trace zero, then Tr_*⟨a⟩ : y ↦ Tr (a y²) is the hyperbolic plane. Indeed 1 and a⁻¹ are isotropic, as Tr (a⁻¹) = Tr a / N a = 0, and their polar pairing is 2 Tr 1 = 4.