Quadratic Form

Results named in Tau Ceti's TauCeti.LinearAlgebra.QuadraticForm modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremEuler's four-square identity for a quadratic map#

Multiplying (x, y, z, w) by the quaternion a + bi + cj + dk multiplies Q x + Q y + Q z + Q w by a² + b² + c² + d². For Q = x ↦ x² on a commutative ring this is euler_four_squares.

QuadraticMap.euler_four_squares.{u_1, u_2, u_3} {R : Type u_1} {M : Type u_2} {N : Type u_3}
  [CommRing R] [AddCommGroup M] [AddCommGroup N] [_root_.Module R M] [_root_.Module R N]
  (Q : QuadraticMap R M N) (a b c d : R) (x y z w : M) :
  Q (a • x - b • y - c • z - d • w) + Q (a • y + b • x + c • w - d • z) +
        Q (a • z - b • w + c • x + d • y) +
      Q (a • w + b • z - c • y + d • x) =
    (a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) • (Q x + Q y + Q z + Q w)

Lean

Formalized in Tau Ceti as QuadraticMap.euler_four_squares.

Sources

• Tau Ceti documentation: QuadraticMap.euler_four_squares
• Source of QuadraticMap.euler_four_squares in TauCeti/LinearAlgebra/QuadraticForm/FourSquares.lean

LeanQuadraticMap.euler_four_squares

Used by 2

Used byNikulin's comparison theorem · Milgram's theorem

TheoremFrobenius reciprocity on regular-form classes#

Transfer of a class over L multiplied by a scalar-extended class from K is the transfer multiplied by the original base class.

TauCeti.RegularFormClass.scharlauTransfer_mul_baseChange.{u, v} {K : Type u} {L : Type v} [Field K]
  [Field L] [Algebra K L] [FiniteDimensional K L] [Invertible 2] (s : L →ₗ[K] K) (hs : s ≠ 0)
  (x : TauCeti.RegularFormClass L) (y : TauCeti.RegularFormClass K) :
  (TauCeti.RegularFormClass.scharlauTransfer s hs) (x * TauCeti.RegularFormClass.baseChange L y) =
    (TauCeti.RegularFormClass.scharlauTransfer s hs) x * y

Lean

Formalized in Tau Ceti as TauCeti.RegularFormClass.scharlauTransfer_mul_baseChange.

Sources

• Tau Ceti documentation: TauCeti.RegularFormClass.scharlauTransfer_mul_baseChange
• Source of TauCeti.RegularFormClass.scharlauTransfer_mul_baseChange in TauCeti/LinearAlgebra/QuadraticForm/Transfer/Class/Frobenius.lean

LeanTauCeti.RegularFormClass.scharlauTransfer_mul_baseChange

TheoremSerre's connectivity theorem for orthogonal bases#

Orthogonal bases of a regular quadratic space in dimension at least three are joined by a finite chain whose every step consists of two orthogonal bases with a vector in common.

Module.Basis.reflTransGen_isOrtho_isContiguous.{u_1, u_2} {K : Type u_1} {V : Type u_2} [Field K]
  [Invertible 2] [AddCommGroup V] [_root_.Module K V] {Q : QuadraticForm K V} {n : ℕ}
  (b b' : Module.Basis (Fin (n + 3)) K V) (hQ : QuadraticMap.Nondegenerate)
  (hb : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b)
  (hb' : LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑b') :
  Relation.ReflTransGen
    (fun c c' =>
      LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑c ∧
        LinearMap.IsOrthoᵢ (QuadraticMap.associated Q) ⇑c' ∧ c.IsContiguous c')
    b b'

Lean

Formalized in Tau Ceti as Module.Basis.reflTransGen_isOrtho_isContiguous.

Sources

• Tau Ceti documentation: Module.Basis.reflTransGen_isOrtho_isContiguous
• Source of Module.Basis.reflTransGen_isOrtho_isContiguous in TauCeti/LinearAlgebra/QuadraticForm/Diagonal/Contiguous/Connected.lean

LeanModule.Basis.reflTransGen_isOrtho_isContiguous

TheoremSylvester's law of inertia for regular forms#

two nondegenerate real quadratic forms are isometric exactly when their signatures agree.

QuadraticForm.equivalent_iff_sigPos_eq_and_sigNeg_eq.{u_1, u_2} {M : Type u_1} {M' : Type u_2}
  [AddCommGroup M] [_root_.Module ℝ M] [AddCommGroup M'] [_root_.Module ℝ M']
  [FiniteDimensional ℝ M] [FiniteDimensional ℝ M'] {Q : QuadraticForm ℝ M} {Q' : QuadraticForm ℝ M'}
  (hQ : QuadraticMap.Nondegenerate) (hQ' : QuadraticMap.Nondegenerate) :
  QuadraticMap.Equivalent Q Q' ↔ sigPos Q = sigPos Q' ∧ sigNeg Q = sigNeg Q'

Lean

Formalized in Tau Ceti as QuadraticForm.equivalent_iff_sigPos_eq_and_sigNeg_eq.

Other forms

Sylvester's law of inertia, classification form. Formalized in Tau Ceti as QuadraticForm.equivalent_iff_finrank_eq_and_sigPos_eq_and_sigNeg_eq.

QuadraticForm.equivalent_iff_finrank_eq_and_sigPos_eq_and_sigNeg_eq.{u_1, u_2} {M : Type u_1}
  {M' : Type u_2} [AddCommGroup M] [_root_.Module ℝ M] [AddCommGroup M'] [_root_.Module ℝ M']
  [FiniteDimensional ℝ M] [FiniteDimensional ℝ M'] (Q : QuadraticForm ℝ M)
  (Q' : QuadraticForm ℝ M') :
  QuadraticMap.Equivalent Q Q' ↔
    Module.finrank ℝ M = Module.finrank ℝ M' ∧ sigPos Q = sigPos Q' ∧ sigNeg Q = sigNeg Q'

Sylvester's law of inertia for isometry classes. Formalized in Tau Ceti as TauCeti.RegularFormClass.eq_iff_rank_eq_and_signature_eq.

TauCeti.RegularFormClass.eq_iff_rank_eq_and_signature_eq.{u_1} {K : Type u_1} [Field K]
  [LinearOrder K] [IsStrictOrderedRing K] [Invertible 2] [IsRealClosed K]
  {x y : TauCeti.RegularFormClass K} : x = y ↔ x.rank = y.rank ∧ x.signature = y.signature

Sources

• Tau Ceti documentation: QuadraticForm.equivalent_iff_sigPos_eq_and_sigNeg_eq
• Source of QuadraticForm.equivalent_iff_sigPos_eq_and_sigNeg_eq in TauCeti/LinearAlgebra/QuadraticForm/Real.lean

LeanQuadraticForm.equivalent_iff_sigPos_eq_and_sigNeg_eq · QuadraticForm.equivalent_iff_finrank_eq_and_sigPos_eq_and_sigNeg_eq · TauCeti.RegularFormClass.eq_iff_rank_eq_and_signature_eq

Used by 2

Used byO'Meara 72:1 up to one global representation · Sylvester's law of inertia at a real place

TheoremWitt decomposition#

a class is its Witt index worth of hyperbolic planes plus its anisotropic part.

TauCeti.RegularFormClass.wittDecomposition.{u} {K : Type u} [Field K] [Invertible 2]
  (c : TauCeti.RegularFormClass K) : c = c.wittIndex • TauCeti.hyperbolicClass K + c.anisotropicPart

Lean

Formalized in Tau Ceti as TauCeti.RegularFormClass.wittDecomposition.

Other forms

Witt decomposition for a regular form. Formalized in Tau Ceti as QuadraticForm.exists_equivalent_hyperbolicPresentation_prod.

QuadraticForm.exists_equivalent_hyperbolicPresentation_prod.{u, v} {K : Type u} [Field K]
  [Invertible 2] {V : Type v} [AddCommGroup V] [_root_.Module K V] [FiniteDimensional K V]
  (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) :
  ∃ p,
    QuadraticMap.Anisotropic (TauCeti.presentedForm p) ∧
      Module.finrank K V = 2 * (TauCeti.formClass Q hQ).wittIndex + p.fst ∧
        QuadraticMap.Equivalent Q
          (QuadraticMap.prod
            (TauCeti.presentedForm
              (TauCeti.hyperbolicPresentation K (TauCeti.formClass Q hQ).wittIndex))
            (TauCeti.presentedForm p))

Witt decomposition (Lam I.4.1), uniqueness. Formalized in Tau Ceti as TauCeti.eq_of_nsmul_hyperbolicClass_add_eq.

TauCeti.eq_of_nsmul_hyperbolicClass_add_eq.{u} {K : Type u} [Field K] [Invertible 2] {m m' : ℕ}
  {a a' : TauCeti.RegularFormClass K} (ha : a.Anisotropic) (ha' : a'.Anisotropic)
  (h : m • TauCeti.hyperbolicClass K + a = m' • TauCeti.hyperbolicClass K + a') : m = m' ∧ a = a'

Witt decomposition (Lam I.4.1), existence. Formalized in Tau Ceti as TauCeti.exists_nsmul_hyperbolicClass_add.

TauCeti.exists_nsmul_hyperbolicClass_add.{u} {K : Type u} [Field K] [Invertible 2]
  (c : TauCeti.RegularFormClass K) : ∃ m a, a.Anisotropic ∧ c = m • TauCeti.hyperbolicClass K + a

Sources

• Tau Ceti documentation: TauCeti.RegularFormClass.wittDecomposition
• Source of TauCeti.RegularFormClass.wittDecomposition in TauCeti/LinearAlgebra/QuadraticForm/Witt/Decomposition.lean

LeanTauCeti.RegularFormClass.wittDecomposition · QuadraticForm.exists_equivalent_hyperbolicPresentation_prod · TauCeti.eq_of_nsmul_hyperbolicClass_add_eq · TauCeti.exists_nsmul_hyperbolicClass_add

Used by 2

Used byA Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup · The relative Stiefel–Whitney formula over a local field

TheoremWitt's chain theorem in its nontrivial range#

two diagonal forms of rank at least two are isometric if and only if their coefficient families are connected by a diagonal chain.

TauCeti.diagonalChain_iff_equivalent.{u} {K : Type u} [Field K] [Invertible 2] {n : ℕ}
  {w w' : Fin (n + 2) → Kˣ} :
  TauCeti.DiagonalChain w w' ↔
    (QuadraticMap.weightedSumSquares K fun i => ↑(w i)).Equivalent
      (QuadraticMap.weightedSumSquares K fun i => ↑(w' i))

Lean

Formalized in Tau Ceti as TauCeti.diagonalChain_iff_equivalent.

Sources

• Tau Ceti documentation: TauCeti.diagonalChain_iff_equivalent
• Source of TauCeti.diagonalChain_iff_equivalent in TauCeti/LinearAlgebra/QuadraticForm/Diagonal/WittChain.lean

LeanTauCeti.diagonalChain_iff_equivalent

Used by 10

Used byLocal equivalence by invariants · O'Meara 72:1 up to one global representation · The Hasse product formula · The system of local invariants of a regular quadratic form Q over a number field · A Kummer cup over a local field is its Hilbert symbol times a fixed nonzero cup · Lam's comparison of the Clifford and Hasse invariants (Lam V.3.20) · Local classification (O'Meara 63:20, Serre IV Thm 7) · The classification of regular forms over a local field, as an equivalence · The relative Stiefel–Whitney formula in degree two, on the trace forms themselves (Kahn, Théorème 2 in degree two) · The relative Stiefel–Whitney formula over a local field

TheoremWitt's extension theorem (Lam I.4.9)#

An isometry between regular subspaces of a finite-dimensional quadratic space extends to an isometry of the whole space. No regularity hypothesis on the ambient form is needed.

QuadraticMap.IsometryEquiv.exists_extension.{u, v} {K : Type u} [Field K] [Invertible 2]
  {V : Type v} [AddCommGroup V] [_root_.Module K V] [FiniteDimensional K V] {Q : QuadraticForm K V}
  {W W' : Submodule K V}
  (f : (QuadraticMap.restrict Q W).IsometryEquiv (QuadraticMap.restrict Q W'))
  (hW : QuadraticMap.Nondegenerate) : ∃ e, ∀ (x : ↥W), e ↑x = ↑(f x)

Lean

Formalized in Tau Ceti as QuadraticMap.IsometryEquiv.exists_extension.

Sources

• Tau Ceti documentation: QuadraticMap.IsometryEquiv.exists_extension
• Source of QuadraticMap.IsometryEquiv.exists_extension in TauCeti/LinearAlgebra/QuadraticForm/Witt/Extension.lean

LeanQuadraticMap.IsometryEquiv.exists_extension

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.