Global quadratic forms over number fields

The declarations the status of Tau Ceti's roadmap names as Tau Ceti has them at commit ace60277.

TheoremHilbert sign prescription (O'Meara 71:19a)#

Let S be a finite set of finite places at which b ∈ Kˣ is a nonsquare and T a finite set of real places at which b is negative, with #S + #T even. Then some a ∈ Kˣ has Hilbert symbol (a, b)_v = -1 at the places of S and of T, and 1 at every other finite and real place.

TauCeti.NumberField.QuadraticForm.exists_hilbertSymbol_eq_ite.{u_1} {K : Type u_1} [Field K]
  [NumberField K] (b : Kˣ)
  (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)))
  (T : Finset { w // w.IsReal }) (hS : ∀ v ∈ S, ¬IsSquare (v.unitAtFinitePlace b))
  (hT : ∀ w ∈ T, (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑b < 0)
  (hST : Even (S.card + T.card)) :
  ∃ a,
    (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)),
        TauCeti.hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b) =
          if v ∈ S then -1 else 1) ∧
      ∀ (w : { w // w.IsReal }),
        TauCeti.hilbertSymbol ((TauCeti.unitAtRealPlace w) a) ((TauCeti.unitAtRealPlace w) b) =
          if w ∈ T then -1 else 1
Lean

Formalized in Tau Ceti as TauCeti.NumberField.QuadraticForm.exists_hilbertSymbol_eq_ite.

Sources
LeanTauCeti.NumberField.QuadraticForm.exists_hilbertSymbol_eq_ite
Uses 13 · Used by 1
Proof usesCorestriction through Shapiro's lemma · The Galois action on the semi-local decomposition · Hensel's lemma for the norm · The kernel of the idele Hilbert character · The Kummer case of the second fundamental inequality · Restriction through Shapiro's lemma · The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w · Shapiro's lemma in degree one · The splitting criterion for quaternion algebras · Tate's cohomological triviality criterion (Milne II 3.10) · Tate's lattice lemma · TauCeti.algebraicExtensionNormedField · TauCeti.relDiscr
Used byO'Meara 72:1 up to one global representation

TheoremThe Hasse product formula#

For every regular form Q over a number field K, the product of the finite Hasse signs and of the real Hasse signs of Q is 1.

QuadraticForm.globalInvariants_hasseProduct_eq_one.{u_1, u_2} {K : Type u_1} [Field K]
  [NumberField K] {V : Type u_2} [AddCommGroup V] [_root_.Module K V] [FiniteDimensional K V]
  (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) :
  (Q.globalInvariants hQ).hasseProduct = 1
Lean

Formalized in Tau Ceti as QuadraticForm.globalInvariants_hasseProduct_eq_one.

Sources
LeanQuadraticForm.globalInvariants_hasseProduct_eq_one
Uses 6 · Used by 1
Statement usesA system of local invariants of a quadratic form over a number field K · The system of local invariants of a regular quadratic form Q over a number field
Proof usesHilbert's product formula · The splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField · Witt's chain theorem in its nontrivial range
Used byO'Meara 72:1 up to one global representation

TheoremThe quaternary case of the Hasse–Minkowski theorem#

Let Q be a regular quaternary form over a number field K which is isotropic at every finite and real place. If, over every number field, every regular diagonal ternary form that is isotropic at every finite and real place is isotropic, then Q is isotropic over K.

The ternary hypothesis is quantified over number fields because it is needed not only over K but also over the quadratic field K(√d), for d a nonsquare representative of the discriminant of Q.

QuadraticForm.not_anisotropic_of_isLocallyIsotropic_quaternary.{u, v} {K : Type u} [Field K]
  [NumberField K] {V : Type v} [AddCommGroup V] [_root_.Module K V] [FiniteDimensional K V]
  {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate) (hrank : Module.finrank K V = 4)
  (hloc : Q.IsLocallyIsotropic)
  (hternary :
    ∀ (L : Type u) [inst : Field L] [inst_1 : NumberField L]
      (p : TauCeti.RegularFormPresentation L),
      p.fst = 3 →
        (TauCeti.presentedForm p).IsLocallyIsotropic →
          ¬QuadraticMap.Anisotropic (TauCeti.presentedForm p)) :
  ¬QuadraticMap.Anisotropic Q
Lean

Formalized in Tau Ceti as QuadraticForm.not_anisotropic_of_isLocallyIsotropic_quaternary.

Other forms

The quaternary case of the Hasse–Minkowski theorem, square discriminant. Formalized in Tau Ceti as QuadraticForm.not_anisotropic_of_isLocallyIsotropic_quaternary_of_discr_eq_zero.

QuadraticForm.not_anisotropic_of_isLocallyIsotropic_quaternary_of_discr_eq_zero.{u, v} {K : Type u}
  [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [_root_.Module K V]
  [FiniteDimensional K V] {Q : QuadraticForm K V} (hQ : QuadraticMap.Nondegenerate)
  (hrank : Module.finrank K V = 4) (hdiscr : (TauCeti.formClass Q hQ).discr = 0)
  (hloc : Q.IsLocallyIsotropic)
  (hternary :
    ∀ (p : TauCeti.RegularFormPresentation K),
      p.fst = 3 →
        (TauCeti.presentedForm p).IsLocallyIsotropic →
          ¬QuadraticMap.Anisotropic (TauCeti.presentedForm p)) :
  ¬QuadraticMap.Anisotropic Q
Sources
LeanQuadraticForm.not_anisotropic_of_isLocallyIsotropic_quaternary · QuadraticForm.not_anisotropic_of_isLocallyIsotropic_quaternary_of_discr_eq_zero

TheoremThe Hasse–Minkowski induction step in rank at least five#

Let Q be a regular quadratic form of rank n ≥ 5 over a number field that is isotropic at every finite and real place. If every diagonal regular form of rank n - 1 that is isotropic at every finite and real place is isotropic over K, then Q is isotropic over K.

QuadraticForm.not_anisotropic_of_isLocallyIsotropic_of_five_le_finrank.{u_1, u_2} {K : Type u_1}
  [Field K] [NumberField K] {X : Type u_2} [AddCommGroup X] [_root_.Module K X]
  [FiniteDimensional K X] {Q : QuadraticForm K X} (hQ : QuadraticMap.Nondegenerate)
  (hX : 5 ≤ Module.finrank K X) (hloc : Q.IsLocallyIsotropic)
  (ih :
    ∀ (p : TauCeti.RegularFormPresentation K),
      p.fst + 1 = Module.finrank K X →
        (TauCeti.presentedForm p).IsLocallyIsotropic →
          ¬QuadraticMap.Anisotropic (TauCeti.presentedForm p)) :
  ¬QuadraticMap.Anisotropic Q
Lean

Formalized in Tau Ceti as QuadraticForm.not_anisotropic_of_isLocallyIsotropic_of_five_le_finrank.

Sources
LeanQuadraticForm.not_anisotropic_of_isLocallyIsotropic_of_five_le_finrank

TheoremLocal equivalence by invariants#

Two regular forms over a number field are isometric at every finite and every real place exactly when they have the same rank, the images of their global discriminants agree at every finite place, and they have the same Hasse sign at every finite place and the same positive index at every real place.

QuadraticForm.locallyEquivalent_iff_finrank_eq_and_discr_eq_and_finiteHasse_eq_and_realPositiveIndex_eq.{u,
    v, w}
  {K : Type u} [Field K] [NumberField K] {V : Type v} [AddCommGroup V] [_root_.Module K V]
  [FiniteDimensional K V] {W : Type w} [AddCommGroup W] [_root_.Module K W] [FiniteDimensional K W]
  {Q : QuadraticForm K V} {R : QuadraticForm K W} (hQ : QuadraticMap.Nondegenerate)
  (hR : QuadraticMap.Nondegenerate) :
  Q.LocallyEquivalent R ↔
    Module.finrank K V = Module.finrank K W ∧
      (∀ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)),
          (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap
              (TauCeti.formClass Q hQ).discr =
            (algebraMap K (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)).squareClassMap
              (TauCeti.formClass R hR).discr) ∧
        Q.finiteHasse hQ = R.finiteHasse hR ∧ Q.realPositiveIndex = R.realPositiveIndex
Lean

Formalized in Tau Ceti as QuadraticForm.locallyEquivalent_iff_finrank_eq_and_discr_eq_and_finiteHasse_eq_and_realPositiveIndex_eq.

Sources
LeanQuadraticForm.locallyEquivalent_iff_finrank_eq_and_discr_eq_and_finiteHasse_eq_and_realPositiveIndex_eq
Uses 5
Proof usesHensel's lemma for the norm · The splitting criterion for quaternion algebras · Sylvester's law of inertia at a real place · TauCeti.algebraicExtensionNormedField · Witt's chain theorem in its nontrivial range

DefinitionThe system of local invariants of a regular quadratic form Q over a number field#

its rank, its plain discriminant d(Q) ∈ Kˣ/(Kˣ)², its Hasse sign at every finite place and its positive index at every real place.

QuadraticForm.globalInvariants.{u, v} {K : Type u} [Field K] [NumberField K] {V : Type v}
  [AddCommGroup V] [_root_.Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V)
  (hQ : QuadraticMap.Nondegenerate) : TauCeti.NumberField.QuadraticForm.GlobalFormInvariants K
Lean

Formalized in Tau Ceti as QuadraticForm.globalInvariants.

Sources
LeanQuadraticForm.globalInvariants
Uses 4 · Used by 2
Statement usesA system of local invariants of a quadratic form over a number field K
Proof usesThe splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField · Witt's chain theorem in its nontrivial range
Used byO'Meara 72:1 up to one global representation · The Hasse product formula

StructureA system of local invariants of a quadratic form over a number field K#

a rank n, a global plain discriminant d ∈ Kˣ/(Kˣ)², a Hasse sign s_v ∈ {±1} at every finite place v, and a positive index p_w at every real place w. No condition relates the data; the systems arising from regular forms of positive rank are those satisfying IsAdmissible.

TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.{u_1} (K : Type u_1) [Field K]
  [NumberField K] : Type u_1
Lean

Formalized in Tau Ceti as TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.

Sources
LeanTauCeti.NumberField.QuadraticForm.GlobalFormInvariants
Used by 3
Used byO'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

TheoremThe kernel of the idele Hilbert character#

Let b ∈ Kˣ be a nonsquare at some finite place or negative at some real place, and let L be a number field over K in which b is a square. Suppose that the idele-class norm group N_{L/K}(C_L) has index dividing two in C_K, as the norm index theorem gives for L = K(√b). Then the kernel of φ_b is Kˣ · N_{L/K}(𝕀_L), the subgroup of 𝕀_K generated by the principal ideles and the idele norms.

TauCeti.NumberField.QuadraticForm.sup_range_ideleNormMap_eq_ker_ideleHilbertCharacter.{u_1, u_2}
  {K : Type u_1} [Field K] [NumberField K] {L : Type u_2} [Field L] [NumberField L] [Algebra K L]
  {b : Kˣ} (hb : IsSquare ((algebraMap K L) ↑b))
  (hidx : (TauCeti.GlobalNumberFields.ideleClassNormMap K L).range.index ∣ 2)
  (hns :
    (∃ v, ¬IsSquare (v.unitAtFinitePlace b)) ∨
      ∃ w, (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑b < 0) :
  NumberField.IdeleGroup.principalSubgroup (NumberField.RingOfIntegers K) K ⊔
      (TauCeti.GlobalNumberFields.ideleNormMap K L).range =
    (TauCeti.NumberField.QuadraticForm.ideleHilbertCharacter b).ker
Lean

Formalized in Tau Ceti as TauCeti.NumberField.QuadraticForm.sup_range_ideleNormMap_eq_ker_ideleHilbertCharacter.

Sources
LeanTauCeti.NumberField.QuadraticForm.sup_range_ideleNormMap_eq_ker_ideleHilbertCharacter
Uses 5 · Used by 1
Proof usesHilbert's product formula · The semi-local decomposition K_v ⊗[K] L ≃ₐ[K_v] ∏_{w ∣ v} L_w · The splitting criterion for quaternion algebras · TauCeti.algebraicExtensionNormedField · The third isomorphism theorem for coset spaces
Used byHilbert sign prescription (O'Meara 71:19a)

TheoremO'Meara 72:1 up to one global representation#

Let U_v and R_w be local forms realizing an admissible system I. Then there are a regular global form W of rank I.rank and α, β ∈ Kˣ such that ⟨α, -αβ⟩ is represented by ⟨1, -β⟩ ⊥ W at every finite and real place, and such that, if ⟨α, -αβ⟩ is represented by ⟨1, -β⟩ ⊥ W over K, some regular global form on K ^ I.rank has I as its system of local invariants.

TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsLocalRealization.exists_locallyRepresents_prod.{u_1}
  {K : Type u_1} [Field K] [NumberField K]
  {I : TauCeti.NumberField.QuadraticForm.GlobalFormInvariants K}
  {U :
    (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) →
      QuadraticForm (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)
        (Fin I.rank → IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)}
  {R : { w // w.IsReal } → QuadraticForm ℝ (Fin I.rank → ℝ)} (hI : I.IsAdmissible)
  (hL : I.IsLocalRealization U R) :
  ∃ W,
    ∃ (_ : QuadraticMap.Nondegenerate),
      ∃ a b,
        QuadraticForm.LocallyRepresents (QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)])
            ((QuadraticMap.weightedSumSquares K ![1, -↑b]).prod W) ∧
          ((QuadraticMap.weightedSumSquares K ![↑a, -(↑a * ↑b)]).IsRepresentedBy
              ((QuadraticMap.weightedSumSquares K ![1, -↑b]).prod W) →
            ∃ Q, ∃ (hQ : QuadraticMap.Nondegenerate), Q.globalInvariants hQ = I)
Lean

Formalized in Tau Ceti as TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsLocalRealization.exists_locallyRepresents_prod.

Sources
LeanTauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsLocalRealization.exists_locallyRepresents_prod
Uses 9
Statement usesA system of local invariants of a quadratic form over a number field K · The system of local invariants of a regular quadratic form Q over a number field
Proof usesThe Hasse product formula · Hensel's lemma for the norm · Hilbert sign prescription (O'Meara 71:19a) · The splitting criterion for quaternion algebras · Sylvester's law of inertia for regular forms · TauCeti.algebraicExtensionNormedField · Witt's chain theorem in its nontrivial range

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.