Documentation

TauCeti.NumberTheory.QuadraticForm.Global.IdeleCharacter

The Hilbert character of the idele group #

For b āˆˆ KĖ£ in a number field K, the idele Hilbert character of b is the homomorphism

Ļ†_b : š•€_K ā†’* {Ā±1}, Ļ†_b(x) = āˆ_v (x_v, b)_v,

where v runs over all places of K, x_v is the coordinate of the idele x at v, and (Ā·, Ā·)_v is the norm-equation Hilbert symbol TauCeti.hilbertSymbol read over the completion K_v. The product is a finite one: at a finite place not above 2 at which both x_v and b are local units the symbol is 1, and almost every finite place is of this kind. It is multiplicative because the Hilbert symbol is multiplicative in its first argument over every nonarchimedean local field, and over ā„ and ā„‚.

By the norm-equation definition of the symbol, (x_v, b)_v = 1 says that x_v is a norm from K_v(āˆšb), so an idele lies in the kernel of Ļ†_b exactly when it is a local non-norm at an even number of places. This is the character used in the proof of Hilbert sign prescription (O'Meara 71:19a) to describe the subgroup KĖ£ Ā· N_{K(āˆšb)/K}(š•€_{K(āˆšb)}) of š•€_K as the kernel of Ļ†_b. That description also needs the product formula for the Hilbert symbol and the norm index theorem, neither of which is proved here.

This file constructs Ļ†_b, computes it on the ideles concentrated at one place, and proves that it is onto {Ā±1} exactly when b is a nonsquare at some finite or real place, in which case its kernel has index two. A complex place contributes nothing, since every element of ā„‚ is a square. It also proves that the idele norms from any number field L āŠ‡ K in which b is a square, for instance L = K(āˆšb), lie in the kernel of Ļ†_b: at a place v of K the coordinate of such a norm is a product of norms from completions L_w containing a square root of b, hence a norm from K_v(āˆšb).

Finally, it proves the two statements about ideles that turn the description of the kernel into sign prescription. For a finite set of finite places at which b is a nonsquare and a finite set of real places at which b is negative, some idele has local symbol -1 with b exactly at those places, and its image under Ļ†_b is -1 to the number of places. If an idele lies in KĖ£ Ā· N_{L/K}(š•€_L) for such an L, then some a āˆˆ KĖ£ has the same local symbols with b as the idele at every place. So once that idele, for an even number of places, is known to lie in KĖ£ Ā· N_{K(āˆšb)/K}(š•€_{K(āˆšb)}), an element a with the prescribed symbols follows.

Main definitions #

Main results #

References #

The local symbols #

source
theorem TauCeti.NumberField.QuadraticForm.hasFiniteMulSupport_hilbertSymbol_ideleFiniteCoord {K : Type u_1} [Field K] [NumberField K] (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) (b : KĖ£) :
Function.HasFiniteMulSupport fun (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) => hilbertSymbol (v.ideleFiniteCoord x) (v.unitAtFinitePlace b)

Finite support of the local symbols of an idele. For an idele x and b āˆˆ KĖ£, the Hilbert symbol (x_v, b)_v over the completion K_v is 1 at all but finitely many finite places v.

The character #

source
noncomputable def TauCeti.NumberField.QuadraticForm.ideleHilbertCharacter {K : Type u_1} [Field K] [NumberField K] (b : KĖ£) :
NumberField.IdeleGroup (NumberField.RingOfIntegers K) K ā†’* ā„¤Ė£

The idele Hilbert character Ļ†_b(x) = āˆ_v (x_v, b)_v of b āˆˆ KĖ£: the product over all places v of K of the Hilbert symbol, over the completion K_v, of the coordinate x_v of the idele x and the image of b. The product over the finite places is a finite one by hasFiniteMulSupport_hilbertSymbol_ideleFiniteCoord.

Instances For
    source
    theorem TauCeti.NumberField.QuadraticForm.ideleHilbertCharacter_apply {K : Type u_1} [Field K] [NumberField K] (b : KĖ£) (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K) :
    (ideleHilbertCharacter b) x = (āˆ w : NumberField.InfinitePlace K, hilbertSymbol (w.ideleInfiniteCoord x) ((Units.map ā†‘(algebraMap K w.Completion)) b)) * āˆį¶  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), hilbertSymbol (v.ideleFiniteCoord x) (v.unitAtFinitePlace b)

    The idele Hilbert character is the product of the local Hilbert symbols at the infinite and at the finite places.

    source
    @[simp]
    theorem TauCeti.NumberField.QuadraticForm.ideleHilbertCharacter_ofAdicCompletion {K : Type u_1} [Field K] [NumberField K] (b : KĖ£) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) (u : (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)Ė£) :
    (ideleHilbertCharacter b) ((NumberField.IdeleGroup.ofAdicCompletion (NumberField.RingOfIntegers K) K v) u) = hilbertSymbol u (v.unitAtFinitePlace b)

    On an idele concentrated at a finite place v, the idele Hilbert character of b is the Hilbert symbol over K_v of the coordinate at v and the image of b.

    source
    @[simp]
    theorem TauCeti.NumberField.QuadraticForm.ideleHilbertCharacter_ofCompletion {K : Type u_1} [Field K] [NumberField K] (b : KĖ£) (w : NumberField.InfinitePlace K) (u : w.CompletionĖ£) :
    (ideleHilbertCharacter b) ((NumberField.IdeleGroup.ofCompletion (NumberField.RingOfIntegers K) K w) u) = hilbertSymbol u ((Units.map ā†‘(algebraMap K w.Completion)) b)

    On an idele concentrated at an infinite place w, the idele Hilbert character of b is the Hilbert symbol over the completion K_w of the coordinate at w and the image of b.

    source
    theorem TauCeti.NumberField.QuadraticForm.ideleHilbertCharacter_ofCompletion_of_isReal {K : Type u_1} [Field K] [NumberField K] (b : KĖ£) (w : { w : NumberField.InfinitePlace K // w.IsReal }) (u : (ā†‘w).CompletionĖ£) :
    (ideleHilbertCharacter b) ((NumberField.IdeleGroup.ofCompletion (NumberField.RingOfIntegers K) K ā†‘w) u) = hilbertSymbol ((Units.map ā†‘(NumberField.InfinitePlace.Completion.ringEquivRealOfIsReal ā‹Æ)) u) ((unitAtRealPlace w) b)

    On an idele concentrated at a real place w, the idele Hilbert character of b is the real Hilbert symbol of the coordinate at w, read in ā„, and the image of b under the real embedding at w.

    source
    theorem TauCeti.NumberField.QuadraticForm.ideleHilbertCharacter_unitEmbedding {K : Type u_1} [Field K] [NumberField K] (a b : KĖ£) :
    (ideleHilbertCharacter b) ((NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K) a) = (āˆį¶  (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b)) * āˆ w : { w : NumberField.InfinitePlace K // w.IsReal }, hilbertSymbol ((unitAtRealPlace w) a) ((unitAtRealPlace w) b)

    The idele Hilbert character on a principal idele. For a, b āˆˆ KĖ£, the image under Ļ†_b of the principal idele of a is the product of the Hilbert symbols (a_v, b_v)_v over the finite places, read in the completions K_v, and over the real places, read in ā„.

    Triviality and surjectivity #

    source
    theorem TauCeti.NumberField.QuadraticForm.ideleHilbertCharacter_eq_one_iff {K : Type u_1} [Field K] [NumberField K] (b : KĖ£) :
    ideleHilbertCharacter b = 1 ā†” (āˆ€ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), IsSquare (v.unitAtFinitePlace b)) āˆ§ āˆ€ (w : { w : NumberField.InfinitePlace K // w.IsReal }), 0 < (NumberField.InfinitePlace.embedding_of_isReal ā‹Æ) ā†‘b

    Triviality of the idele Hilbert character. Ļ†_b is trivial exactly when b is a square in the completion at every finite place and positive at every real place.

    source
    theorem TauCeti.NumberField.QuadraticForm.ideleHilbertCharacter_surjective_iff {K : Type u_1} [Field K] [NumberField K] (b : KĖ£) :
    Function.Surjective ā‡‘(ideleHilbertCharacter b) ā†” (āˆƒ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), Ā¬IsSquare (v.unitAtFinitePlace b)) āˆØ āˆƒ (w : { w : NumberField.InfinitePlace K // w.IsReal }), (NumberField.InfinitePlace.embedding_of_isReal ā‹Æ) ā†‘b < 0

    Surjectivity of the idele Hilbert character. Ļ†_b is onto {Ā±1} exactly when b is a nonsquare in the completion at some finite place or negative at some real place.

    source
    theorem TauCeti.NumberField.QuadraticForm.index_ker_ideleHilbertCharacter {K : Type u_1} [Field K] [NumberField K] {b : KĖ£} (hb : (āˆƒ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), Ā¬IsSquare (v.unitAtFinitePlace b)) āˆØ āˆƒ (w : { w : NumberField.InfinitePlace K // w.IsReal }), (NumberField.InfinitePlace.embedding_of_isReal ā‹Æ) ā†‘b < 0) :
    (ideleHilbertCharacter b).ker.index = 2

    The kernel of the idele Hilbert character has index two when b is a nonsquare in the completion at some finite place or negative at some real place.

    Idele norms #

    source
    @[simp]
    theorem TauCeti.NumberField.QuadraticForm.hilbertSymbol_ideleFiniteCoord_ideleNormMap {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)) (x : NumberField.IdeleGroup (NumberField.RingOfIntegers L) L) (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)) :
    hilbertSymbol (v.ideleFiniteCoord ((GlobalNumberFields.ideleNormMap K L) x)) (v.unitAtFinitePlace b) = 1

    The finite coordinates of an idele norm are local norms. If b āˆˆ KĖ£ is a square in a number field L over K, then at every finite place v of K the coordinate of an idele norm from L has Hilbert symbol 1 with b. It is a product of norms from completions L_w in which b is a square, so it is a norm from K_v(āˆšb).

    source
    @[simp]
    theorem TauCeti.NumberField.QuadraticForm.hilbertSymbol_ideleInfiniteCoord_ideleNormMap {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)) (x : NumberField.IdeleGroup (NumberField.RingOfIntegers L) L) (v : NumberField.InfinitePlace K) :
    hilbertSymbol (v.ideleInfiniteCoord ((GlobalNumberFields.ideleNormMap K L) x)) ((Units.map ā†‘(algebraMap K v.Completion)) b) = 1

    The infinite coordinates of an idele norm are local norms. If b āˆˆ KĖ£ is a square in a number field L over K, then at every infinite place v of K the coordinate of an idele norm from L has Hilbert symbol 1 with b.

    source
    @[simp]
    theorem TauCeti.NumberField.QuadraticForm.ideleHilbertCharacter_ideleNormMap {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)) (x : NumberField.IdeleGroup (NumberField.RingOfIntegers L) L) :
    (ideleHilbertCharacter b) ((GlobalNumberFields.ideleNormMap K L) x) = 1

    Idele norms lie in the kernel of the idele Hilbert character. If b āˆˆ KĖ£ is a square in a number field L over K, then Ļ†_b is trivial on the idele norms N_{L/K}(š•€_L): every local symbol of an idele norm is 1.

    source
    theorem TauCeti.NumberField.QuadraticForm.range_ideleNormMap_le_ker_ideleHilbertCharacter {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)) :
    (GlobalNumberFields.ideleNormMap K L).range ā‰¤ (ideleHilbertCharacter b).ker

    The idele norm group lies in the kernel of the idele Hilbert character. If b āˆˆ KĖ£ is a square in a number field L over K, then N_{L/K}(š•€_L) ā‰¤ ker Ļ†_b.

    source
    theorem TauCeti.NumberField.QuadraticForm.exists_hilbertSymbol_eq_of_mem_sup_range_ideleNormMap {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)) {x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K} (hx : x āˆˆ (NumberField.IdeleGroup.unitEmbedding (NumberField.RingOfIntegers K) K).range āŠ” (GlobalNumberFields.ideleNormMap K L).range) :
    āˆƒ (a : KĖ£), (āˆ€ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), hilbertSymbol (v.unitAtFinitePlace a) (v.unitAtFinitePlace b) = hilbertSymbol (v.ideleFiniteCoord x) (v.unitAtFinitePlace b)) āˆ§ āˆ€ (w : NumberField.InfinitePlace K), hilbertSymbol ((Units.map ā†‘(algebraMap K w.Completion)) a) ((Units.map ā†‘(algebraMap K w.Completion)) b) = hilbertSymbol (w.ideleInfiniteCoord x) ((Units.map ā†‘(algebraMap K w.Completion)) b)

    Local symbols on KĖ£ Ā· N_{L/K}(š•€_L). Let b āˆˆ KĖ£ be a square in a number field L over K. If an idele x lies in the subgroup KĖ£ Ā· N_{L/K}(š•€_L) generated by the principal ideles and the idele norms, then some a āˆˆ KĖ£ has the same Hilbert symbol with b as x at every finite and every infinite place: writing x = a Ā· N(y), the coordinates of x and a differ by those of the idele norm N(y), which are local norms.

    Ideles with prescribed local symbols #

    source
    theorem TauCeti.NumberField.QuadraticForm.exists_idele_hilbertSymbol_eq_ite {K : Type u_1} [Field K] [NumberField K] (b : KĖ£) (S : Finset (IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K))) (T : Finset { w : NumberField.InfinitePlace K // w.IsReal }) (hS : āˆ€ v āˆˆ S, Ā¬IsSquare (v.unitAtFinitePlace b)) (hT : āˆ€ w āˆˆ T, (NumberField.InfinitePlace.embedding_of_isReal ā‹Æ) ā†‘b < 0) :
    āˆƒ (x : NumberField.IdeleGroup (NumberField.RingOfIntegers K) K), (āˆ€ (v : IsDedekindDomain.HeightOneSpectrum (NumberField.RingOfIntegers K)), hilbertSymbol (v.ideleFiniteCoord x) (v.unitAtFinitePlace b) = if v āˆˆ S then -1 else 1) āˆ§ (āˆ€ (w : { w : NumberField.InfinitePlace K // w.IsReal }), hilbertSymbol ((ā†‘w).ideleInfiniteCoord x) ((Units.map ā†‘(algebraMap K (ā†‘w).Completion)) b) = if w āˆˆ T then -1 else 1) āˆ§ (ideleHilbertCharacter b) x = (-1) ^ (S.card + T.card)

    An idele with prescribed local symbols. 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. There is an idele x whose Hilbert symbol with b is -1 at the places of S and of T, and 1 at every other finite and real place; its image under Ļ†_b is (-1)^(#S + #T).