Documentation

TauCeti.NumberTheory.QuadraticForm.Global.ArchimedeanSymbol

The archimedean Hilbert symbol #

The archimedean symbol is the norm-equation Hilbert symbol read over the completion at an infinite place. This module records that symbol for global units at the places of a number field, the square criterion for a global unit at a real place, and the real-place half of the sign prescription.

At a real place the symbol of two elements is -1 exactly when both are negative there, and 1 exactly when one of them is positive there. A product of such symbols over a prescribed set of real places is therefore a product of signs, and the bimultiplicativity it needs is that of TauCeti.hilbertSymbol_real_mul_left and TauCeti.hilbertSymbol_real_mul_right, in TauCeti.NumberTheory.HilbertSymbol.Archimedean; both are [simp], so simp expands a product of global units inside the localized symbol. At a complex place the symbol is 1 for the same reason the archimedean classification of a form is by rank alone: every element of ℂˣ is a square, so TauCeti.hilbertSymbol_eq_one_of_isAlgClosed, in TauCeti.NumberTheory.HilbertSymbol.IsAlgClosed, already settles the complex places of a number field and the real places alone decide such a product. For the symbol of two arbitrary elements of the completion K_w itself, such as the coordinates of an idele, the same two facts are read through the isomorphisms of K_w with ℝ and with ℂ.

The real-place half of the sign prescription of O'Meara 71:19 is recorded as well. Given a prescribed element b that is a nonsquare at a real place, exists_hilbertSymbol_eq_neg_one_atRealPlace turns it into a local non-norm, which is what a sign-prescription argument needs at each place of its set; a field unit negative at every real place is such a b.

Main results #

A value-group convention #

The value group of HeightOneSpectrum.valuation is WithZero (Multiplicative ℤ), whose multiplicative identity 1 is the value zero, that is, order of vanishing zero. So v.valuation K x = 1 says that x is a local unit at v, while an element of order of vanishing 1 is written WithZero.exp (-1), the value of a generator of v.asIdeal; the additive order of vanishing of an element is the negative logarithm of its value, as IsDedekindDomain.HeightOneSpectrum.neg_log_valuation_eq_one_iff records. A criterion phrased with the hypothesis v.valuation K (a : K) = 1 would therefore be false, and a = 1 is the counterexample: its image in the completion is the unit 1, which is a square.

The finite-place nonsquare criterion that does hold is IsDedekindDomain.HeightOneSpectrum.not_isSquare_adicCompletion_of_valuation_eq_exp_of_not_even: an element of odd order of vanishing is a nonsquare in the completion, and the prime of a prescribed modulus supplies an element of that kind. Here Kˣ is the group of all nonzero elements of K, not the unit group of the ring of integers, so a field unit of odd order of vanishing at a finite place is a nonsquare in its completion by that criterion, exactly as any other element of odd order of vanishing is. The criterion is one way to obtain a nonsquare and not a description of all of them; in particular it says nothing about the local units, which are the case v.valuation K x = 1.

References #

source
@[simp]
theorem TauCeti.hilbertSymbol_unitAtRealPlace_eq_neg_one_iff {K : Type u_1} [Field K] (w : { w : NumberField.InfinitePlace K // w.IsReal }) (a b : Kˣ) :
hilbertSymbol ((unitAtRealPlace w) a) ((unitAtRealPlace w) b) = -1 ↔ (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑a < 0 ∧ (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑b < 0

The archimedean symbol at a real place is -1 exactly when both global units are negative there. This is the real formula TauCeti.hilbertSymbol_real, read at a place of a number field through TauCeti.unitAtRealPlace; it is the sign criterion by which a sign prescription multiplies the symbols of a prescribed set over its real places.

source
theorem TauCeti.hilbertSymbol_unitAtRealPlace_eq_one_iff {K : Type u_1} [Field K] (w : { w : NumberField.InfinitePlace K // w.IsReal }) (a b : Kˣ) :
hilbertSymbol ((unitAtRealPlace w) a) ((unitAtRealPlace w) b) = 1 ↔ 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑a ∨ 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑b

The archimedean symbol at a real place is 1 exactly when one of the two global units is positive there.

source
theorem TauCeti.isSquare_unitAtRealPlace_iff {K : Type u_1} [Field K] (w : { w : NumberField.InfinitePlace K // w.IsReal }) (a : Kˣ) :
IsSquare ((unitAtRealPlace w) a) ↔ 0 < (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑a

A global unit is a square at a real place exactly when it is positive there.

source
theorem TauCeti.not_isSquare_unitAtRealPlace_iff {K : Type u_1} [Field K] (w : { w : NumberField.InfinitePlace K // w.IsReal }) (a : Kˣ) :
¬IsSquare ((unitAtRealPlace w) a) ↔ (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑a < 0

A global unit is a nonsquare at a real place exactly when it is negative there.

source
theorem TauCeti.exists_hilbertSymbol_eq_neg_one_atRealPlace {K : Type u_1} [Field K] (w : { w : NumberField.InfinitePlace K // w.IsReal }) (b : Kˣ) (hb : (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑b < 0) :
∃ (a : Kˣ), (NumberField.InfinitePlace.embedding_of_isReal ⋯) ↑a < 0 ∧ hilbertSymbol ((unitAtRealPlace w) a) ((unitAtRealPlace w) b) = -1

A prescribed negative global unit at a real place has a partner with symbol -1.

Given the element b whose local nonsquareness a sign-prescription argument presupposes, there is a global unit a whose symbol with b at w is -1, and a is negative there. Both operands are read at the same real place, so that the symbol can be multiplied with the symbols at the other places of the prescribed set. This is the step that turns a prescribed nonsquare into a local non-norm.

source
theorem TauCeti.units_map_ringEquivRealOfIsReal_algebraMap {K : Type u_1} [Field K] (w : { w : NumberField.InfinitePlace K // w.IsReal }) (b : Kˣ) :
(Units.map ↑(NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal ⋯)) ((Units.map ↑(algebraMap K (↑w).Completion)) b) = (unitAtRealPlace w) b

The image of a global unit in the completion K_w at a real place w, read in ℝ through the isomorphism K_w ≃ ℝ, is its image under the real embedding at w.

source
theorem TauCeti.hilbertSymbol_completion_eq_unitAtRealPlace {K : Type u_1} [Field K] (w : { w : NumberField.InfinitePlace K // w.IsReal }) (a b : Kˣ) :
hilbertSymbol ((Units.map ↑(algebraMap K (↑w).Completion)) a) ((Units.map ↑(algebraMap K (↑w).Completion)) b) = hilbertSymbol ((unitAtRealPlace w) a) ((unitAtRealPlace w) b)

At a real place w, the Hilbert symbol of the images of two global units in the completion K_w is the real Hilbert symbol of their images under the real embedding at w.

source
theorem TauCeti.hilbertSymbol_completion_eq_one_of_isComplex {K : Type u_1} [Field K] {w : NumberField.InfinitePlace K} (hw : w.IsComplex) (a c : w.Completionˣ) :
hilbertSymbol a c = 1

Over the completion at a complex place, every Hilbert symbol is 1: the completion is isomorphic to ℂ, where every element is a square.

source
theorem TauCeti.hilbertSymbol_completion_mul_left {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (a a' c : w.Completionˣ) :
hilbertSymbol (a * a') c = hilbertSymbol a c * hilbertSymbol a' c

Over the completion at an infinite place, the Hilbert symbol is multiplicative in its first argument: at a real place this is TauCeti.hilbertSymbol_real_mul_left read through the isomorphism with ℝ, and at a complex place every symbol is 1.

source
@[simp]
theorem TauCeti.hilbertSymbol_completion_one_left {K : Type u_1} [Field K] (w : NumberField.InfinitePlace K) (c : w.Completionˣ) :
hilbertSymbol 1 c = 1

Over the completion at an infinite place, the symbol with first argument 1 is 1.