Frobenius reciprocity for Scharlau transfer of isometry classes

Form-level Frobenius reciprocity descends to isometry classes: transfer of a class over the extension multiplied by a scalar-extended class from the base field is the transfer multiplied by the original base class. Applying this to the hyperbolic class, which is its own scalar extension, computes the transfer of a hyperbolic plane as [L : K] hyperbolic planes over the base field.

Both results are statements about regular-form classes only. They are the input for the descent of transfer to Witt rings, where the second one shows that the hyperbolic ideal is preserved.

Main results

• TauCeti.RegularFormClass.scharlauTransfer_mul_baseChange: Frobenius reciprocity on regular form classes.
• TauCeti.RegularFormClass.scharlauTransfer_hyperbolicClass: transfer of a hyperbolic plane is a sum of [L : K] hyperbolic planes.

References

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

@[simp]

theorem TauCeti.RegularFormClass.scharlauTransfer_mul_baseChange {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) (y : RegularFormClass K) : (scharlauTransfer s hs) (x * baseChange L y) = (scharlauTransfer s hs) x * y

Frobenius reciprocity on regular-form classes. Transfer of a class over L multiplied by a scalar-extended class from K is the transfer multiplied by the original base class.

@[simp]

theorem TauCeti.RegularFormClass.scharlauTransfer_hyperbolicClass {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) : (scharlauTransfer s hs) (hyperbolicClass L) = Module.finrank K L • hyperbolicClass K

Transfer of a hyperbolic plane over L is a sum of [L : K] hyperbolic planes over K. This is the hyperbolic-preservation statement that makes transfer descend to Witt rings.