Scharlau transfer of isometry classes

Scharlau transfer along a nonzero linear functional carries regular quadratic forms over a finite field extension to regular quadratic forms over the base field. Since transfer preserves isometries and orthogonal sums, it induces an additive map on isometry classes. This file constructs that map and records its values on forms, its rank, and its identity and tower laws.

The class-level construction is the input for the transfer on Witt rings. It also lets results about a transferred form be stated without choosing a diagonalization.

Main definitions

• TauCeti.RegularFormClass.scharlauTransfer: Scharlau transfer as an additive homomorphism on isometry classes of regular forms.
• TauCeti.RegularFormClass.traceTransfer: the specialization to the algebra trace of a finite separable extension.

Main results

• TauCeti.RegularFormClass.scharlauTransfer_formClass: transfer of the class of a regular form is the class of its transferred form.
• TauCeti.RegularFormClass.rank_scharlauTransfer: transfer multiplies rank by the degree of the field extension.
• TauCeti.RegularFormClass.scharlauTransfer_id: transfer along the identity is the identity.
• TauCeti.RegularFormClass.scharlauTransfer_comp: transfers compose in a tower.
• TauCeti.RegularFormClass.traceTransfer_formClass: trace transfer agrees with the form-level trace transfer.

References

• W. Scharlau, Quadratic and Hermitian Forms (1985), Chapter 2, §5.
• T. Y. Lam, Introduction to Quadratic Forms over Fields (2005), Chapter VII, §1.

noncomputable def TauCeti.RegularFormClass.scharlauTransfer {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (s : L →ₗ[K] K) (hs : s ≠ 0) : RegularFormClass L →+ RegularFormClass K

Scharlau transfer of isometry classes. Transfer along a nonzero K-linear functional s : L → K is an additive homomorphism from regular-form classes over L to regular-form classes over K.

@[simp]

theorem TauCeti.RegularFormClass.scharlauTransfer_mk {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (s : L →ₗ[K] K) (hs : s ≠ 0) (p : RegularFormPresentation L) : (scharlauTransfer s hs) ⟦p⟧ = formClass (QuadraticMap.scharlauTransfer (presentedForm p) s) ⋯

Scharlau transfer of classes is computed on a diagonal presentation by transferring its presented form.

@[simp]

theorem TauCeti.RegularFormClass.scharlauTransfer_formClass {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] {V : Type w} [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [FiniteDimensional L V] (s : L →ₗ[K] K) (hs : s ≠ 0) (Q : QuadraticForm L V) (hQ : QuadraticMap.Nondegenerate) : (scharlauTransfer s hs) (formClass Q hQ) = formClass (QuadraticMap.scharlauTransfer Q s) ⋯

The transfer of the isometry class of a regular form is the isometry class of its transfer. This is the class-level form of QuadraticMap.Equivalent.scharlauTransfer.

@[simp]

theorem TauCeti.RegularFormClass.rank_scharlauTransfer {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (s : L →ₗ[K] K) (hs : s ≠ 0) (x : RegularFormClass L) : ((scharlauTransfer s hs) x).rank = Module.finrank K L * x.rank

Scharlau transfer multiplies the rank of an isometry class by the degree of the field extension.

@[simp]

theorem TauCeti.RegularFormClass.scharlauTransfer_id {K : Type u} [Field K] [Invertible 2] : scharlauTransfer LinearMap.id ⋯ = AddMonoidHom.id (RegularFormClass K)

Scharlau transfer along the identity functional is the identity on isometry classes.

@[simp]

theorem TauCeti.RegularFormClass.scharlauTransfer_comp {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] {E : Type w} [Field E] [Algebra L E] [Algebra K E] [IsScalarTower K L E] [FiniteDimensional L E] (s : L →ₗ[K] K) (hs : s ≠ 0) (t : E →ₗ[L] L) (ht : t ≠ 0) : (scharlauTransfer s hs).comp (scharlauTransfer t ht) = scharlauTransfer (s ∘ₗ ↑K t) ⋯

Scharlau transfers compose in a tower of finite field extensions.

Transfer along the trace

noncomputable def TauCeti.RegularFormClass.traceTransfer (K : Type u) {L : Type v} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Algebra.IsSeparable K L] : RegularFormClass L →+ RegularFormClass K

Trace transfer on isometry classes, defined using the nonzero algebra trace of a finite separable field extension.

theorem TauCeti.RegularFormClass.traceTransfer_eq_scharlauTransfer {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Algebra.IsSeparable K L] (x : RegularFormClass L) : (traceTransfer K) x = (scharlauTransfer (Algebra.trace K L) ⋯) x

Class-level trace transfer is Scharlau transfer along the algebra trace.

@[simp]

theorem TauCeti.RegularFormClass.traceTransfer_formClass {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Algebra.IsSeparable K L] {V : Type w} [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [FiniteDimensional L V] (Q : QuadraticForm L V) (hQ : QuadraticMap.Nondegenerate) : (traceTransfer K) (formClass Q hQ) = formClass (QuadraticMap.traceTransfer K Q) ⋯

Trace transfer of the class of a regular form is the class of its form-level trace transfer.

@[simp]

theorem TauCeti.RegularFormClass.rank_traceTransfer {K : Type u} {L : Type v} [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] [Algebra.IsSeparable K L] (x : RegularFormClass L) : ((traceTransfer K) x).rank = Module.finrank K L * x.rank

Trace transfer multiplies rank by the degree of the field extension.