Frobenius reciprocity for Scharlau transfer

Scharlau transfer satisfies the projection formula: transferring the tensor product of a quadratic form over an extension with a scalar-extended form from the base is isometric to the tensor product of the transferred form with the original base form. The isometry is the canonical cancellation

V ⊗[L] (L ⊗[K] W) ≃ V ⊗[K] W.

This is the form-level Frobenius reciprocity needed to make transfer on Witt groups linear over the Witt ring of the base field.

References

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

theorem QuadraticMap.scharlauTransfer_tmul_baseChange_comp_cancelBaseChange {K : Type u_1} {L : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing K] [CommRing L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [AddCommGroup W] [Module K W] [Invertible 2] (Q : QuadraticForm L V) (R : QuadraticForm K W) (s : L →ₗ[K] K) : comp ((scharlauTransfer Q s).tmul R) ↑(LinearEquiv.restrictScalars K (TensorProduct.AlgebraTensorModule.cancelBaseChange K L L V W)) = scharlauTransfer (Q.tmul (QuadraticForm.baseChange L R)) s

Pulling the tensor product of the transferred form and a base form back along the canonical tensor cancellation gives the transfer of the tensor product with its scalar extension.

def QuadraticMap.IsometryEquiv.scharlauTransferTmulBaseChange {K : Type u_1} {L : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing K] [CommRing L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [AddCommGroup W] [Module K W] [Invertible 2] (Q : QuadraticForm L V) (R : QuadraticForm K W) (s : L →ₗ[K] K) : IsometryEquiv (QuadraticMap.scharlauTransfer (Q.tmul (QuadraticForm.baseChange L R)) s) ((QuadraticMap.scharlauTransfer Q s).tmul R)

Frobenius reciprocity for Scharlau transfer. Transferring Q tensored with the scalar extension of R is isometric to the tensor product of the transfer of Q with R. The underlying isometry is the canonical cancellation V ⊗[L] (L ⊗[K] W) ≃ V ⊗[K] W.

@[simp]

theorem QuadraticMap.IsometryEquiv.scharlauTransferTmulBaseChange_toLinearEquiv {K : Type u_1} {L : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing K] [CommRing L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [AddCommGroup W] [Module K W] [Invertible 2] (Q : QuadraticForm L V) (R : QuadraticForm K W) (s : L →ₗ[K] K) : (scharlauTransferTmulBaseChange Q R s).toLinearEquiv = LinearEquiv.restrictScalars K (TensorProduct.AlgebraTensorModule.cancelBaseChange K L L V W)

The linear equivalence underlying Frobenius reciprocity is tensor cancellation.

@[simp]

theorem QuadraticMap.IsometryEquiv.scharlauTransferTmulBaseChange_apply {K : Type u_1} {L : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing K] [CommRing L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [AddCommGroup W] [Module K W] [Invertible 2] (Q : QuadraticForm L V) (R : QuadraticForm K W) (s : L →ₗ[K] K) (x : TensorProduct L V (TensorProduct K L W)) : (scharlauTransferTmulBaseChange Q R s) x = (LinearEquiv.restrictScalars K (TensorProduct.AlgebraTensorModule.cancelBaseChange K L L V W)) x

The Frobenius-reciprocity isometry is the canonical cancellation of scalar extension.

@[simp]

theorem QuadraticMap.IsometryEquiv.scharlauTransferTmulBaseChange_symm_apply {K : Type u_1} {L : Type u_2} {V : Type u_3} {W : Type u_4} [CommRing K] [CommRing L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [AddCommGroup W] [Module K W] [Invertible 2] (Q : QuadraticForm L V) (R : QuadraticForm K W) (s : L →ₗ[K] K) (v : V) (w : W) : (scharlauTransferTmulBaseChange Q R s).symm (v ⊗ₜ[K] w) = v ⊗ₜ[L] (1 ⊗ₜ[K] w)

The inverse Frobenius-reciprocity isometry inserts the unit in the scalar-extension factor on pure tensors.