Scharlau transfer of quadratic forms

The Scharlau transfer along a linear functional s : L →ₗ[K] K is the composite s ∘ Q, on the underlying K-space. It is built from Mathlib's LinearMap.compQuadraticMap'. It commutes with orthogonal sums and composition of functionals, and carries isometries over L to isometries over K.

For a field over a commutative ring in which two is invertible, a nonzero functional preserves the radical, after restriction of scalars, and hence preserves and reflects nondegeneracy. Neither finiteness nor separability is needed for this assertion. Finiteness is needed to compare arbitrary nonzero functionals, and separability makes the trace a nonzero choice. The dimension of the transferred space is given by Module.finrank_mul_finrank.

This is the form-level construction used to transfer isometry classes and Witt classes. Transfer is additive; it is not in general multiplicative on Witt rings.

References

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

def QuadraticMap.scharlauTransfer {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommSemiring K] [CommSemiring L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] (Q : QuadraticForm L V) (s : L →ₗ[K] K) : QuadraticForm K V

The Scharlau transfer of Q along s, on the underlying space over the smaller ring. Nonzeroness of s is required for preservation of regularity, not for this definition.

@[simp]

theorem QuadraticMap.scharlauTransfer_apply {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommSemiring K] [CommSemiring L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] (Q : QuadraticForm L V) (s : L →ₗ[K] K) (x : V) : (scharlauTransfer Q s) x = s (Q x)

@[simp]

theorem QuadraticMap.scharlauTransfer_zero {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommSemiring K] [CommSemiring L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] (s : L →ₗ[K] K) : scharlauTransfer 0 s = 0

The zero form transfers to the zero form.

@[simp]

theorem QuadraticMap.scharlauTransfer_zero_functional {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommSemiring K] [CommSemiring L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] (Q : QuadraticForm L V) : scharlauTransfer Q 0 = 0

Transfer along the zero functional is zero.

@[simp]

theorem QuadraticMap.scharlauTransfer_add {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommSemiring K] [CommSemiring L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] (Q R : QuadraticForm L V) (s : L →ₗ[K] K) : scharlauTransfer (Q + R) s = scharlauTransfer Q s + scharlauTransfer R s

Transfer preserves addition of forms.

@[simp]

theorem QuadraticMap.scharlauTransfer_smul {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommSemiring K] [CommSemiring L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] (Q : QuadraticForm L V) (s : L →ₗ[K] K) (c : K) : scharlauTransfer (c • Q) s = c • scharlauTransfer Q s

Transfer commutes with scaling by an element of the smaller ring.

@[simp]

theorem QuadraticMap.scharlauTransfer_id {L : Type u_2} {V : Type u_3} [CommSemiring L] [AddCommMonoid V] [Module L V] (Q : QuadraticForm L V) : scharlauTransfer Q LinearMap.id = Q

Transfer along the identity functional leaves a form unchanged.

@[simp]

theorem QuadraticMap.scharlauTransfer_prod {K : Type u_1} {L : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring K] [CommSemiring L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] [AddCommMonoid W] [Module L W] [Module K W] [IsScalarTower K L W] (Q : QuadraticForm L V) (R : QuadraticForm L W) (s : L →ₗ[K] K) : (prod Q R).scharlauTransfer s = prod (scharlauTransfer Q s) (scharlauTransfer R s)

Transfer commutes with orthogonal sum.

@[simp]

theorem QuadraticMap.scharlauTransfer_comp {K : Type u_1} {L : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring K] [CommSemiring L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] [AddCommMonoid W] [Module L W] [Module K W] [IsScalarTower K L W] (Q : QuadraticForm L V) (s : L →ₗ[K] K) (f : W →ₗ[L] V) : (comp Q f).scharlauTransfer s = comp (scharlauTransfer Q s) (↑K f)

Transfer commutes with pullback along an L-linear map, viewed as a K-linear map.

theorem QuadraticMap.scharlauTransfer_comp_mul {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommSemiring K] [CommSemiring L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] (Q : QuadraticForm L V) (s : L →ₗ[K] K) (a : L) : scharlauTransfer Q (s ∘ₗ (LinearMap.mul K L) a) = scharlauTransfer (a • Q) s

Multiplying the input to the functional scales the form before transfer.

@[simp]

theorem QuadraticMap.scharlauTransfer_scharlauTransfer {K : Type u_1} {L : Type u_2} {E : Type u_3} {V : Type u_4} [CommSemiring K] [CommSemiring L] [CommSemiring E] [Algebra K L] [Algebra L E] [Algebra K E] [IsScalarTower K L E] [AddCommMonoid V] [Module E V] [Module L V] [Module K V] [IsScalarTower L E V] [IsScalarTower K E V] [IsScalarTower K L V] (Q : QuadraticForm E V) (t : E →ₗ[L] L) (s : L →ₗ[K] K) : scharlauTransfer (scharlauTransfer Q t) s = scharlauTransfer Q (s ∘ₗ ↑K t)

Transfer is transitive in a tower of scalar rings.

noncomputable def QuadraticMap.traceTransfer (K : Type u_1) {L : Type u_2} {V : Type u_3} [CommRing K] [CommRing L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] (Q : QuadraticForm L V) : QuadraticForm K V

Transfer along the algebra trace. For a finite separable field extension the functional is nonzero, by Algebra.trace_ne_zero.

theorem QuadraticMap.traceTransfer_apply {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing K] [CommRing L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] (Q : QuadraticForm L V) (x : V) : (traceTransfer K Q) x = (Algebra.trace K L) (Q x)

@[simp]

theorem QuadraticMap.traceTransfer_eq_scharlauTransfer {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing K] [CommRing L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] (Q : QuadraticForm L V) : traceTransfer K Q = scharlauTransfer Q (Algebra.trace K L)

Trace transfer is Scharlau transfer along the algebra trace.

theorem QuadraticMap.traceTransfer_sq {K : Type u_1} {L : Type u_2} [CommRing K] [CommRing L] [Algebra K L] : traceTransfer K sq = LinearMap.BilinMap.toQuadraticMap (Algebra.traceForm K L)

The trace transfer of the one-dimensional unit form is the quadratic trace form.

@[simp]

theorem QuadraticMap.scharlauTransfer_neg {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing K] [CommRing L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] (Q : QuadraticForm L V) (s : L →ₗ[K] K) : scharlauTransfer (-Q) s = -scharlauTransfer Q s

Transfer preserves negation of forms.

@[simp]

theorem QuadraticMap.scharlauTransfer_sub {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing K] [CommRing L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] (Q R : QuadraticForm L V) (s : L →ₗ[K] K) : scharlauTransfer (Q - R) s = scharlauTransfer Q s - scharlauTransfer R s

Transfer preserves subtraction of forms.

@[simp]

theorem QuadraticMap.polar_scharlauTransfer {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing K] [CommRing L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] (Q : QuadraticForm L V) (s : L →ₗ[K] K) (x y : V) : polar (⇑(scharlauTransfer Q s)) x y = s (polar (⇑Q) x y)

The polar form of a transfer is obtained by applying the functional to the polar form.

@[simp]

theorem QuadraticMap.associated_scharlauTransfer {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing K] [CommRing L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [Invertible 2] (Q : QuadraticForm L V) (s : L →ₗ[K] K) (x y : V) : ((associated (scharlauTransfer Q s)) x) y = s (((associated Q) x) y)

The associated bilinear form of a Scharlau transfer is obtained by applying the functional to the associated bilinear form.

@[simp]

theorem QuadraticMap.radical_scharlauTransfer {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing K] [CommRing L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [Invertible 2] (Q : QuadraticForm L V) (s : L →ₗ[K] K) (hs : s.IsFrobeniusFunctional) : radical (scharlauTransfer Q s) = Submodule.restrictScalars K (radical Q)

A Frobenius functional preserves the radical when two is invertible.

@[simp]

theorem QuadraticMap.nondegenerate_scharlauTransfer_iff {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing K] [CommRing L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [Invertible 2] (Q : QuadraticForm L V) (s : L →ₗ[K] K) (hs : s.IsFrobeniusFunctional) : Nondegenerate ↔ Nondegenerate

Transfer along a Frobenius functional preserves and reflects regularity.

theorem QuadraticMap.radical_scharlauTransfer_of_ne_zero {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing K] [Field L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [Invertible 2] (Q : QuadraticForm L V) (s : L →ₗ[K] K) (hs : s ≠ 0) : radical (scharlauTransfer Q s) = Submodule.restrictScalars K (radical Q)

A nonzero functional on a field preserves the radical when two is invertible.

theorem QuadraticMap.nondegenerate_scharlauTransfer_iff_of_ne_zero {K : Type u_1} {L : Type u_2} {V : Type u_3} [CommRing K] [Field L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [Invertible 2] (Q : QuadraticForm L V) (s : L →ₗ[K] K) (hs : s ≠ 0) : Nondegenerate ↔ Nondegenerate

Transfer along a nonzero functional preserves and reflects regularity when the larger ring is a field.

theorem QuadraticMap.exists_unit_scharlauTransfer_eq {K : Type u_1} {L : Type u_2} {V : Type u_3} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [FiniteDimensional K L] (Q : QuadraticForm L V) (s t : L →ₗ[K] K) (hs : s ≠ 0) (ht : t ≠ 0) : ∃ (a : Lˣ), scharlauTransfer Q t = scharlauTransfer (↑a • Q) s

Over a finite field extension, changing between any two nonzero functionals amounts to scaling the form by a unit before transfer.

theorem QuadraticMap.nondegenerate_traceTransfer_iff {K : Type u_1} {L : Type u_2} {V : Type u_3} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module L V] [Module K V] [IsScalarTower K L V] [Invertible 2] [FiniteDimensional K L] [Algebra.IsSeparable K L] (Q : QuadraticForm L V) : Nondegenerate ↔ Nondegenerate

Trace transfer is regular exactly when the original form is, for a finite separable extension in characteristic different from two.

def QuadraticMap.IsometryEquiv.scharlauTransfer {K : Type u_1} {L : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring K] [CommSemiring L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] [AddCommMonoid W] [Module L W] [Module K W] [IsScalarTower K L W] {Q : QuadraticForm L V} {R : QuadraticForm L W} (e : IsometryEquiv Q R) (s : L →ₗ[K] K) : IsometryEquiv (QuadraticMap.scharlauTransfer Q s) (QuadraticMap.scharlauTransfer R s)

An isometry over the larger ring induces an isometry of transferred forms.

@[simp]

theorem QuadraticMap.IsometryEquiv.scharlauTransfer_apply {K : Type u_1} {L : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring K] [CommSemiring L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] [AddCommMonoid W] [Module L W] [Module K W] [IsScalarTower K L W] {Q : QuadraticForm L V} {R : QuadraticForm L W} (e : IsometryEquiv Q R) (s : L →ₗ[K] K) (x : V) : (e.scharlauTransfer s) x = e x

theorem QuadraticMap.Equivalent.scharlauTransfer {K : Type u_1} {L : Type u_2} {V : Type u_3} {W : Type u_4} [CommSemiring K] [CommSemiring L] [Algebra K L] [AddCommMonoid V] [Module L V] [Module K V] [IsScalarTower K L V] [AddCommMonoid W] [Module L W] [Module K W] [IsScalarTower K L W] {Q : QuadraticForm L V} {R : QuadraticForm L W} (h : Equivalent Q R) (s : L →ₗ[K] K) : Equivalent (QuadraticMap.scharlauTransfer Q s) (QuadraticMap.scharlauTransfer R s)

Transfer respects isometry classes.