Scalar representation over algebraically closed fields

Every nonzero quadratic form over an algebraically closed field represents every scalar. For a finite-dimensional nondegenerate form, a scalar is represented exactly when it is zero or its space has positive dimension. These results apply in every characteristic and justify omitting complex places from local-to-global scalar-representation predicates.

The classification and isotropy results in characteristic different from two hold more generally over separably closed fields and live in TauCeti.LinearAlgebra.QuadraticForm.SepClosed.

theorem QuadraticForm.represents_of_ne_zero_of_isAlgClosed {K : Type u_1} {W : Type u_2} [Field K] [IsAlgClosed K] [AddCommGroup W] [Module K W] {Q : QuadraticForm K W} (hQ : Q ≠ 0) (a : K) : QuadraticMap.Represents Q a

A nonzero quadratic form over an algebraically closed field represents every scalar.

theorem QuadraticForm.represents_of_finrank_pos_of_isAlgClosed {K : Type u_1} {W : Type u_2} [Field K] [IsAlgClosed K] [AddCommGroup W] [Module K W] (Q : QuadraticForm K W) (hQ : QuadraticMap.Nondegenerate) (hW : 0 < Module.finrank K W) (a : K) : QuadraticMap.Represents Q a

A regular quadratic form on a space of positive rank over an algebraically closed field represents every scalar. The positive-rank hypothesis supplies nontriviality directly, so no finite-dimensionality typeclass assumption is needed.

@[simp]

theorem QuadraticForm.represents_iff_eq_zero_or_finrank_pos_of_isAlgClosed {K : Type u_1} {W : Type u_2} [Field K] [IsAlgClosed K] [AddCommGroup W] [Module K W] [FiniteDimensional K W] (Q : QuadraticForm K W) (hQ : QuadraticMap.Nondegenerate) (a : K) : QuadraticMap.Represents Q a ↔ a = 0 ∨ 0 < Module.finrank K W

A regular quadratic form over an algebraically closed field represents a scalar exactly when the scalar is zero or the underlying space has positive dimension.