Representation by quadratic forms

This file defines both representation of values by a quadratic map and representation of one quadratic map by another through an injective isometry. It gives the latter relation its basic reflexivity, transitivity, and equivalence-invariance API, from which anisotropy is read off as an isometry invariant.

For scalar values, it defines the represented-unit value set, proves its elementary square-class invariance, and gives the criterion that, for a form with trivial radical, representing a unit is equivalent to isotropy after adjoining the one-dimensional form with that unit as its negative coefficient. A nondegenerate form has trivial radical by Mathlib's radical_eq_bot theorem. A nondegenerate form over a field pairs every nonzero isotropic vector with an isotropic partner of polar pairing one, so a nondegenerate isotropic form contains such an isotropic pair. If the orthogonal sum of a form with trivial radical and an anisotropic form on a nonzero space is isotropic, the two summands therefore share a nonzero opposite value; for two nondegenerate summands, the first with some unit value and the second on a nonzero space, isotropy of the sum is equivalent to such a shared opposite unit value. These results provide the basic bridge from value questions to isotropy questions, following Lam, Introduction to Quadratic Forms over Fields, I.2.3 and I.3.5.

def QuadraticMap.Represents {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) (a : N) : Prop

A value a : N is represented by a quadratic map if it is the value of the map at a vector.

Equations

• Q.Represents a = ∃ (v : M), Q v = a

def QuadraticMap.IsRepresentedBy {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] (Q : QuadraticMap R M N) (Q' : QuadraticMap R M' N) : Prop

A quadratic map is represented by another if it admits an injective isometry into it.

Equations

• Q.IsRepresentedBy Q' = ∃ (f : Q →qᵢ Q'), Function.Injective ⇑f

theorem QuadraticMap.isRepresentedBy_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {M' : Type u_4} [AddCommMonoid M'] [Module R M'] (Q : QuadraticMap R M N) (Q' : QuadraticMap R M' N) : Q.IsRepresentedBy Q' ↔ ∃ (f : M →ₗ[R] M'), Function.Injective ⇑f ∧ ∀ (x : M), Q' (f x) = Q x

Representation by a quadratic map is witnessed by an injective linear map preserving the quadratic map.

theorem QuadraticMap.restrict_isRepresentedBy {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) (U : Submodule R M) : (Q.restrict U).IsRepresentedBy Q

The restriction of a quadratic map to a submodule is represented by the ambient map.

theorem QuadraticMap.isRepresentedBy_prod_right {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q₁ : QuadraticMap R M N) {M₂ : Type u_4} [AddCommMonoid M₂] [Module R M₂] (Q₂ : QuadraticMap R M₂ N) : Q₂.IsRepresentedBy (Q₁.prod Q₂)

The right factor of an orthogonal product is represented by the product.

theorem QuadraticMap.IsRepresentedBy.refl {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : Q.IsRepresentedBy Q

Every quadratic map is represented by itself.

theorem QuadraticMap.IsRepresentedBy.trans {R : Type u_1} {N : Type u_3} [CommSemiring R] [AddCommMonoid N] [Module R N] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N} (h₁₂ : Q₁.IsRepresentedBy Q₂) (h₂₃ : Q₂.IsRepresentedBy Q₃) : Q₁.IsRepresentedBy Q₃

Representation of quadratic maps is transitive.

theorem QuadraticMap.Equivalent.isRepresentedBy {R : Type u_1} {N : Type u_3} [CommSemiring R] [AddCommMonoid N] [Module R N] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (h : Q₁.Equivalent Q₂) : Q₁.IsRepresentedBy Q₂

An equivalent quadratic map is represented by the other map.

theorem QuadraticMap.IsRepresentedBy.represents {R : Type u_1} {N : Type u_3} [CommSemiring R] [AddCommMonoid N] [Module R N] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {a : N} (h : Q₁.IsRepresentedBy Q₂) (ha : Q₁.Represents a) : Q₂.Represents a

A scalar represented by a represented quadratic map is represented by the ambient map.

theorem QuadraticMap.IsRepresentedBy.not_anisotropic {R : Type u_1} {N : Type u_3} [CommSemiring R] [AddCommMonoid N] [Module R N] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (h : Q₁.IsRepresentedBy Q₂) (hQ₁ : ¬Q₁.Anisotropic) : ¬Q₂.Anisotropic

An ambient quadratic map is isotropic when it represents an isotropic quadratic map.

theorem QuadraticMap.Equivalent.anisotropic_iff {R : Type u_1} {N : Type u_3} [CommSemiring R] [AddCommMonoid N] [Module R N] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (h : Q₁.Equivalent Q₂) : Q₁.Anisotropic ↔ Q₂.Anisotropic

Anisotropy is an invariant of isometry.

theorem QuadraticMap.Equivalent.isRepresentedBy_congr {R : Type u_1} {N : Type u_3} [CommSemiring R] [AddCommMonoid N] [Module R N] {M₁ : Type u_4} {M₂ : Type u_5} {M₃ : Type u_6} {M₄ : Type u_7} [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] [AddCommMonoid M₃] [Module R M₃] [AddCommMonoid M₄] [Module R M₄] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} {Q₃ : QuadraticMap R M₃ N} {Q₄ : QuadraticMap R M₄ N} (h₁₂ : Q₁.Equivalent Q₂) (h₃₄ : Q₃.Equivalent Q₄) : Q₁.IsRepresentedBy Q₃ ↔ Q₂.IsRepresentedBy Q₄

Replacing either quadratic map by an equivalent one preserves representation.

@[simp]

theorem QuadraticMap.represents_zero {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) : Q.Represents 0

Every quadratic map represents zero.

theorem QuadraticMap.represents_iff {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] (Q : QuadraticMap R M N) (a : N) : Q.Represents a ↔ a ∈ Set.range ⇑Q

Representation is the same as membership in the range of the quadratic map.

def QuadraticMap.unitValueSet {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticMap R M R) : Set Rˣ

The set of represented units of a scalar-valued quadratic map.

This is the classical value set D(Q) over a field; over a general commutative semiring it is the set of units represented by Q, rather than the full value set.

Equations

• Q.unitValueSet = {a : Rˣ | Q.Represents ↑a}

@[simp]

theorem QuadraticMap.mem_unitValueSet {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {Q : QuadraticMap R M R} {a : Rˣ} : a ∈ Q.unitValueSet ↔ Q.Represents ↑a

Membership in unitValueSet is representation of the underlying scalar.

theorem QuadraticMap.IsometryEquiv.represents_iff {R : Type u_1} [CommSemiring R] {M₁ : Type u_4} {M₂ : Type u_5} {N : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid N] [Module R M₁] [Module R M₂] [Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (e : Q₁.IsometryEquiv Q₂) (a : N) : Q₁.Represents a ↔ Q₂.Represents a

Representation is preserved by an isometric equivalence of quadratic maps.

theorem QuadraticMap.Equivalent.unitValueSet_eq {R : Type u_1} [CommSemiring R] {M₁ : Type u_4} {M₂ : Type u_5} [AddCommMonoid M₁] [AddCommMonoid M₂] [Module R M₁] [Module R M₂] {Q₁ : QuadraticMap R M₁ R} {Q₂ : QuadraticMap R M₂ R} (h : Q₁.Equivalent Q₂) : Q₁.unitValueSet = Q₂.unitValueSet

Equivalent quadratic forms have the same represented-unit value set.

theorem QuadraticMap.Represents.prod {R : Type u_1} [CommSemiring R] {M₁ : Type u_4} {M₂ : Type u_5} {P : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid P] [Module R M₁] [Module R M₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {a b : P} (h₁ : Q₁.Represents a) (h₂ : Q₂.Represents b) : (Q₁.prod Q₂).Represents (a + b)

A value represented by each factor is represented by their product.

theorem QuadraticMap.not_anisotropic_prod_of_represents_neg {R : Type u_1} [CommSemiring R] {M₁ : Type u_4} {M₂ : Type u_5} {P : Type u_6} [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommGroup P] [Module R M₁] [Module R M₂] [Module R P] {Q₁ : QuadraticMap R M₁ P} {Q₂ : QuadraticMap R M₂ P} {a : P} (h₁ : Q₁.Represents a) (h₂ : Q₂.Represents (-a)) (ha : a ≠ 0) : ¬(Q₁.prod Q₂).Anisotropic

If one factor represents a nonzero value a and the other represents -a, then their orthogonal product is isotropic.

theorem QuadraticMap.Represents.smul_mul_self {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] {Q : QuadraticMap R M N} {a : N} (h : Q.Represents a) (b : R) : Q.Represents ((b * b) • a)

Representing a value is preserved after multiplying it by the square of any scalar.

@[simp]

theorem QuadraticMap.represents_smul_mul_self_iff {R : Type u_1} [CommSemiring R] {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (Q : QuadraticMap R M N) (a : N) (b : Rˣ) : Q.Represents ((↑b * ↑b) • a) ↔ Q.Represents a

Representation is invariant under multiplication by the square of a unit.

theorem QuadraticMap.represents_of_radical_eq_bot_of_not_anisotropic {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hQ : radical Q = ⊥) (hiso : ¬Anisotropic Q) (a : K) : Represents Q a

A quadratic form with trivial radical and a nonzero isotropic vector represents every scalar.

theorem QuadraticMap.represents_of_nondegenerate_of_not_anisotropic {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hQ : Nondegenerate) (hiso : ¬Anisotropic Q) (a : K) : Represents Q a

A nondegenerate quadratic form with a nonzero isotropic vector represents every scalar.

theorem QuadraticMap.Represents.of_isSquare_div {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} {a b : K} (h : Represents Q a) (ha : a ≠ 0) (hab : IsSquare (b / a)) : Represents Q b

Over a field, a quadratic form representing a nonzero scalar a represents every b for which b / a is a square.

theorem QuadraticMap.Anisotropic.exists_ne_zero_eq_neg_of_not_anisotropic_prod {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] {V' : Type u_6} [AddCommGroup V'] [Module K V'] [Nontrivial V'] {U : QuadraticForm K V} {W : QuadraticForm K V'} (hW : Anisotropic W) (hU : radical U = ⊥) (h : ¬(prod U W).Anisotropic) : ∃ (x : V) (y : V'), U x ≠ 0 ∧ U x = -W y

If the orthogonal sum of a form with trivial radical and an anisotropic form on a nonzero space is isotropic, then some nonzero value of the first form is the negative of a value of the second (O'Meara, Introduction to Quadratic Forms, 66:1).

theorem QuadraticMap.Nondegenerate.exists_isotropic_polar_eq_one {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (hQ : Nondegenerate) {x : V} (hx : x ≠ 0) (hxQ : Q x = 0) : ∃ (y : V), Q y = 0 ∧ polar (⇑Q) x y = 1

For a nondegenerate quadratic form, every nonzero isotropic vector x has an isotropic partner y with polar Q x y = 1, so that x, y is a hyperbolic pair.

theorem QuadraticMap.Nondegenerate.exists_isotropic_pair {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] {Q : QuadraticForm K V} (hQ : Nondegenerate) (hiso : ¬Anisotropic Q) : ∃ (x : V) (y : V), x ≠ 0 ∧ Q x = 0 ∧ Q y = 0 ∧ polar (⇑Q) x y = 1

A nondegenerate isotropic quadratic form contains two isotropic vectors whose polar pairing is one.

@[simp]

theorem QuadraticMap.represents_mul_sq_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticMap R M R) (a : R) (b : Rˣ) : Q.Represents (a * ↑b ^ 2) ↔ Q.Represents a

Multiplying a represented scalar by the square of a unit preserves representation.

theorem QuadraticMap.mem_unitValueSet_mul_sq_iff {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (Q : QuadraticMap R M R) (a b : Rˣ) : a * b ^ 2 ∈ Q.unitValueSet ↔ a ∈ Q.unitValueSet

Membership in unitValueSet is invariant under multiplication by a unit square.

theorem QuadraticMap.mem_unitValueSet_iff_not_anisotropic_prod_of_radical_eq_bot {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hQ : radical Q = ⊥) (a : Kˣ) : a ∈ unitValueSet Q ↔ ¬(prod Q (-↑a • sq)).Anisotropic

A unit is represented exactly when adjoining its negative line makes the form isotropic, under triviality of the quadratic radical.

The added line is the one-dimensional form x ↦ -a * x², written as a scalar multiple of QuadraticMap.sq.

theorem QuadraticMap.mem_unitValueSet_iff_not_anisotropic_prod {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hQ : Nondegenerate) (a : Kˣ) : a ∈ unitValueSet Q ↔ ¬(prod Q (-↑a • sq)).Anisotropic

For a nondegenerate form, a unit is represented exactly when adjoining its negative line makes the form isotropic.

theorem QuadraticMap.not_anisotropic_prod_iff_exists_mem_unitValueSet_neg_mem {K : Type u_4} {V : Type u_5} [Field K] [AddCommGroup V] [Module K V] {V' : Type u_6} [AddCommGroup V'] [Module K V'] [Nontrivial V'] {Q₁ : QuadraticForm K V} {Q₂ : QuadraticForm K V'} (hQ₁ : radical Q₁ = ⊥) (hQ₂ : radical Q₂ = ⊥) (h : (unitValueSet Q₁).Nonempty) : ¬(prod Q₁ Q₂).Anisotropic ↔ ∃ x ∈ unitValueSet Q₁, -x ∈ unitValueSet Q₂

The orthogonal sum of a form Q₁ with trivial radical and some unit value and a form Q₂ with trivial radical on a nonzero space is isotropic exactly when some unit value x of Q₁ has -x a value of Q₂.