Local forms attached to an admissible system of invariants #
Let I be a system of local invariants of rank n over a number field K: a global
discriminant d, a Hasse sign s_v at each finite place and a positive index p_w at each real
place. A family of regular quadratic forms U_v over the completions K_v and R_w over ℝ,
all on the coordinate space of dimension n, realizes I locally when U_v has discriminant
the image of d in K_v and local Hasse invariant s_v, and R_w has positive index p_w.
The main theorem is that an admissible system is realized locally. At a finite place this is the
local realization theorem TauCeti.RegularFormClass.exists_of_realization: the two exceptions
it carries, rank one with s_v = -1 and rank two with d_v = [-1] and s_v = -1, are exactly the
small-rank conditions of admissibility. At a real place the form is a sum of p_w squares minus
n - p_w squares, and its discriminant (-1)^(n - p_w) is the image of d by the real
discriminant condition of admissibility. As for the local predicates of
TauCeti.NumberTheory.QuadraticForm.Global.Predicates, no complex clause is included: a complex
place carries only the rank, and every regular form on Fin n → ℂ is isometric to the sum of n
squares (QuadraticForm.equivalent_weightedSumSquares_one_iff_finrank_eq), so a complex-place
form would carry no information beyond n.
The predicate IsLocalRealization only records the local invariants; the global constraints are
inherited from the system when that system is admissible. A family realizing an admissible system
has all its local discriminants images of the one global class d, its finite Hasse invariants
trivial at almost every place, and the product of its finite Hasse invariants with the real Hasse
signs (-1)^(q(q-1)/2), q the negative index, equal to one. These are exactly the hypotheses of
O'Meara's existence theorem 72:1 for a global form with prescribed localizations: applied to a
family realizing an admissible system, that theorem produces a global form isometric to U_v at
every finite place and to R_w at every real place, hence a global form with invariants I.
The construction is not canonical: the local realization theorem is an existence statement, and so is the theorem here.
Conversely, the hypotheses of 72:1 make a family of local forms a realization of an admissible
system. A family U_v, R_w of rank n ≥ 1 whose discriminants are the images of one global
class d, whose finite Hasse invariants are trivial at almost every place and whose Hasse product
is one realizes the system of rank n, discriminant d, the Hasse invariants of the U_v and the
positive indices of the R_w, and that system is admissible. The small-rank conditions of
admissibility hold automatically for any family of regular local forms.
Main definitions #
TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.IsLocalRealization: a family of local forms realizes the systemI.TauCeti.NumberField.QuadraticForm.GlobalFormInvariants.ofLocalForms: the system of invariants of a family of local forms, with a chosen global discriminant.
Main results #
GlobalFormInvariants.IsAdmissible.exists_regularFormClass_atFinitePlace,GlobalFormInvariants.IsAdmissible.exists_quadraticForm_atFinitePlace: at each finite place, an admissible system is realized by a regular form over the completion.GlobalFormInvariants.IsAdmissible.exists_quadraticForm_atRealPlace: at each real place, by a regular real form of the prescribed signature.GlobalFormInvariants.IsAdmissible.exists_isLocalRealization: an admissible system is realized locally.GlobalFormInvariants.IsLocalRealization.discr_real,GlobalFormInvariants.IsLocalRealization.hasFiniteMulSupport_localHasse,GlobalFormInvariants.IsLocalRealization.finprod_localHasse_mul_prod_eq_one: for a family realizing an admissible system, the real discriminants are images of the global discriminant, the finite Hasse invariants have finite support, and the Hasse product is one.GlobalFormInvariants.IsLocalRealization.isAdmissible_iff: conversely, a system realized by a family of local forms is admissible exactly when its rank is positive, the real discriminants are images of the global discriminant, and the finite Hasse invariants of the family have finite support and Hasse product one.GlobalFormInvariants.isLocalRealization_ofLocalForms,GlobalFormInvariants.isAdmissible_ofLocalForms: a family of regular local forms of positive rank with discriminants coming from one global class, almost everywhere trivial Hasse invariants and Hasse product one realizes an admissible system, its own systemofLocalForms.
References #
- O. T. O'Meara, Introduction to Quadratic Forms, Springer (1963), 63:23 for the local realization and 72:1 for existence with prescribed local invariants.
- J.-P. Serre, A Course in Arithmetic, Springer (1973), Chapter IV, §2.3, Proposition 6, and §3.3, Theorem 9.
A family of local forms realizing a system of invariants. Regular quadratic forms U v
over the completion K_v at every finite place v and R w over ℝ at every real place w,
all on the coordinate space of dimension I.rank, realize I when U v has discriminant the
image of the global discriminant of I and local Hasse invariant I.finiteHasse v, and R w
has positive index I.realPositiveIndex w.
- nondegenerate_finite (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : QuadraticMap.Nondegenerate
The form at a finite place is regular.
- discr_finite (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (formClass (U v) ⋯).discr = I.discrAtFinitePlace v
The discriminant at a finite place is the image of the global discriminant.
- localHasse_finite (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) : (formClass (U v) ⋯).localHasse = I.finiteHasse v
The local Hasse invariant at a finite place is the prescribed Hasse sign.
- nondegenerate_real (w : { w : NumberField.InfinitePlace K // w.IsReal }) : QuadraticMap.Nondegenerate
The form at a real place is regular.
- sigPos_real (w : { w : NumberField.InfinitePlace K // w.IsReal }) : sigPos (R w) = I.realPositiveIndex w
The positive index at a real place is the prescribed one.
Instances For
The negative index at a real place is the negative index n - p_w of the system.
The discriminant at a real place of a family realizing an admissible system is the image of the global discriminant under the real embedding.
The real Hasse sign (-1)^(q(q-1)/2) of the form at a real place, q its negative index, is
the real Hasse sign of the system.
For a diagonalization R w ≃ ⟨a₁, …, aₙ⟩ of the form at a real place, the product
∏_{i<j} (aᵢ, aⱼ)_ℝ of the real Hilbert symbols is the real Hasse sign of the system.
The finite Hasse invariants of a family realizing an admissible system are trivial at all but finitely many finite places.
The Hasse product of a locally realizing family is one. For a family realizing an
admissible system, the product over all finite places of the local Hasse invariants, times the
product over the real places of the real Hasse signs (-1)^(q(q-1)/2), is 1.
The Hasse product of a locally realizing family may be computed over any finite set of finite places outside which the finite Hasse invariants are trivial.
Admissibility of a locally realized system. A system of invariants realized by a family of
regular local forms is admissible exactly when its rank is positive, the discriminant of the form
at every real place is the image of the global discriminant, the local Hasse invariants of the
forms at the finite places are trivial at almost every place, and their product with the real
Hasse signs (-1)^(q(q-1)/2), q the negative index, is one.
The two small-rank conditions of admissibility need no hypothesis: in rank one, and in rank two
with discriminant [-1], every regular form over a nonarchimedean local field has trivial local
Hasse invariant.
The system of invariants of a family of local forms. For a global square class d and
regular forms U v over the completions K_v and R w over ℝ, all on the coordinate space of
dimension n, this is the system of rank n and global discriminant d whose Hasse sign at a
finite place v is the local Hasse invariant of U v and whose positive index at a real place
w is that of R w.
The body is exposed so that the rank of ofLocalForms d U hU R reduces to n: the forms U v
and R w live on Fin n, and IsLocalRealization asks for forms on the coordinate space of the
rank of the system.
Instances For
The rank of the system of a family of local forms is the dimension n.
The global discriminant of the system of a family of local forms is the chosen class d.
The Hasse sign at a finite place v of the system of a family of local forms is the local
Hasse invariant of U v.
The positive index at a real place w of the system of a family of local forms is the
positive index of R w.
A family of regular local forms whose discriminants at the finite places are the images of a
global square class d realizes the system of invariants it defines with d.
The local data of a global form with prescribed localizations is admissible. Let U v and
R w be regular forms of rank n ≥ 1 over the finite completions and over ℝ at the real places
of K, whose discriminants are the images of one global square class d, whose local Hasse
invariants are trivial at almost every finite place, and whose Hasse product, with the real Hasse
signs (-1)^(q(q-1)/2) for the negative indices q, is one. Then the system of invariants of the
family is admissible.
These are the hypotheses of O'Meara's existence theorem 72:1 for a global form with prescribed
localizations. Since the family realizes its own system (isLocalRealization_ofLocalForms), such a
family is a local realization of an admissible system.
Local realization at a finite place. An admissible system is realized at every finite
place v by an isometry class of regular forms over K_v of the prescribed rank, with
discriminant the image of the global discriminant and the prescribed local Hasse invariant.
Local realization at a finite place, by a form on the coordinate space. An admissible
system is realized at every finite place v by a regular quadratic form on K_v ^ n, n the
rank of the system, with discriminant the image of the global discriminant and the prescribed
local Hasse invariant.
Local realization at a real place. An admissible system is realized at every real place
w by a regular quadratic form on ℝ ^ n, n the rank of the system, with positive index
p_w, negative index n - p_w, and discriminant the image of the global discriminant under the
real embedding of w.
Local realization of an admissible system. An admissible system of invariants is realized by a family of regular quadratic forms over the finite and real completions, on the coordinate space of its rank.