Layer 0 of the Hasse–Minkowski development

Mathlib 4.33 has the abstract theory of quadratic maps: QuadraticMap.Anisotropic, QuadraticMap.Nondegenerate, weightedSumSquares, the orthogonal sum QuadraticMap.prod and base change QuadraticForm.baseChange. The theory of quadratic forms over number fields needs the dual notions: isotropy, representation of a value, and the interaction of nondegeneracy with orthogonal sums and base change. This file supplies them.

Main definitions

• Isotropic Q: Q vanishes on a nonzero vector.
• IsotropicFn f: the same for a bare function f, used for translates of a form.
• represents Q a: Q takes the value a on a nonzero vector.
• Indefinite Q (over ℝ): Q takes both a negative and a positive value.

Main results

• isotropic_iff_not_anisotropic, not_isotropic_iff_anisotropic.
• represents_zero_iff_isotropic, represents_iff_sub_isotropic.
• isotropic_iff_zero_of_rank_one: in dimension one isotropy is being zero.
• nondegenerate_weightedSumSquares, nondegenerate_prod, nondegenerate_of_anisotropic.
• IsometryEquiv.baseChange, Equivalent.baseChange.
• Indefinite.isotropic: an indefinite real form is isotropic (intermediate value theorem).

Isotropic quadratic maps

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

A quadratic map is isotropic if it vanishes on some nonzero vector.

Equations

• HasseMinkowski.Isotropic Q = ∃ (x : M), x ≠ 0 ∧ Q x = 0

theorem HasseMinkowski.isotropic_iff_not_anisotropic {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (Q : QuadraticMap R M N) : Isotropic Q ↔ ¬Q.Anisotropic

theorem HasseMinkowski.not_isotropic_iff_anisotropic {R : Type u_1} {M : Type u_2} {N : Type u_3} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M] [Module R N] (Q : QuadraticMap R M N) : ¬Isotropic Q ↔ Q.Anisotropic

def HasseMinkowski.IsotropicFn {M : Type u_1} {N : Type u_2} [Zero M] [Zero N] (f : M → N) : Prop

Function-level isotropy: a function vanishing at a nonzero vector.

This is needed to speak about a translate x ↦ Q x - a of a quadratic form, which is not a quadratic map (it does not vanish at 0 when a ≠ 0).

Equations

• HasseMinkowski.IsotropicFn f = ∃ (x : M), x ≠ 0 ∧ f x = 0

Representing values

def HasseMinkowski.represents {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : R) : Prop

A quadratic form represents a if it takes the value a on a nonzero vector.

For a ≠ 0 the restriction to nonzero vectors is immaterial, since Q 0 = 0; for a = 0 it makes the notion agree with isotropy, as in the classical theory.

Equations

• HasseMinkowski.represents Q a = ∃ (x : M), x ≠ 0 ∧ Q x = a

theorem HasseMinkowski.represents_zero_iff_isotropic {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : represents Q 0 ↔ Isotropic Q

theorem HasseMinkowski.represents_iff_sub_isotropic {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : R) : represents Q a ↔ IsotropicFn fun (x : M) => Q x - a

Rank-one forms

theorem HasseMinkowski.isotropic_iff_zero_of_rank_one {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hr : Module.finrank K V = 1) : Isotropic Q ↔ Q = 0

Nondegeneracy

theorem HasseMinkowski.nondegenerate_weightedSumSquares {K : Type u_1} {ι : Type u_2} [Field K] [Invertible 2] [Fintype ι] (w : ι → Kˣ) : QuadraticMap.Nondegenerate

theorem HasseMinkowski.nondegenerate_prod {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [CommRing R] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Invertible 2] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h₁ : QuadraticMap.Nondegenerate) (h₂ : QuadraticMap.Nondegenerate) : QuadraticMap.Nondegenerate

theorem HasseMinkowski.nondegenerate_of_anisotropic {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [Invertible 2] {Q : QuadraticForm K V} (hQ : QuadraticMap.Anisotropic Q) : QuadraticMap.Nondegenerate

Rank-zero forms

theorem HasseMinkowski.anisotropic_of_rank_zero {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hr : Module.finrank K V = 0) : QuadraticMap.Anisotropic Q

theorem HasseMinkowski.not_isotropic_of_rank_zero {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hr : Module.finrank K V = 0) : ¬Isotropic Q

Indefinite real forms

def HasseMinkowski.Indefinite {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) : Prop

A real quadratic form is indefinite if it takes both a negative and a positive value.

Equations

• HasseMinkowski.Indefinite Q = ((∃ (x : M), Q x < 0) ∧ ∃ (x : M), 0 < Q x)

theorem HasseMinkowski.Indefinite.isotropic {M : Type u_1} [AddCommGroup M] [Module ℝ M] {Q : QuadraticForm ℝ M} (h : Indefinite Q) : Isotropic Q

Base change of isometries

These belong to the QuadraticMap namespace so that e.baseChange works by dot notation for an isometry equivalence e, in the same way as the rest of Mathlib's quadratic-form API.

noncomputable def QuadraticMap.IsometryEquiv.baseChange {R : Type u_1} {A : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Invertible 2] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (e : IsometryEquiv Q₁ Q₂) : IsometryEquiv (QuadraticForm.baseChange A Q₁) (QuadraticForm.baseChange A Q₂)

Base change sends an isometry equivalence of quadratic forms to one.

Equations

• e.baseChange = { toLinearEquiv := LinearEquiv.baseChange R A M₁ M₂ e.toLinearEquiv, map_app' := ⋯ }

theorem QuadraticMap.Equivalent.baseChange {R : Type u_1} {A : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} [CommRing R] [CommRing A] [Algebra R A] [AddCommGroup M₁] [AddCommGroup M₂] [Module R M₁] [Module R M₂] [Invertible 2] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} (h : Equivalent Q₁ Q₂) : Equivalent (QuadraticForm.baseChange A Q₁) (QuadraticForm.baseChange A Q₂)

Dot-notation aliases

The generic API above lives in HasseMinkowski; these aliases let Q.Isotropic and Q.represents a be used directly for a quadratic map Q, matching Mathlib's convention for Q.Anisotropic and QuadraticMap.prod.

@[reducible, inline]

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

Dot-notation alias for HasseMinkowski.Isotropic: the quadratic map vanishes on some nonzero vector.

Equations

• Q.Isotropic = HasseMinkowski.Isotropic Q

@[reducible, inline]

abbrev QuadraticMap.represents {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a : R) : Prop

Dot-notation alias for HasseMinkowski.represents: the quadratic form takes the value a on some nonzero vector.

Equations

• QuadraticMap.represents Q a = HasseMinkowski.represents Q a