Finite places of number fields #
This file defines finite places of a number field K as absolute values coming from an embedding
into a completion of K associated to a non-zero prime ideal of š K.
Main Definitions and Results #
NumberField.adicAbv: av-adic absolute value onK.NumberField.FinitePlace: the type of finite places of a number fieldK.NumberField.FinitePlace.embedding: the canonical embedding of a number fieldKto thev-adic completionv.adicCompletion KofK, wherevis a non-zero prime ideal ofš KNumberField.FinitePlace.norm_def: the norm ofembedding v xis the same as thev-adic absolute value ofx. See alsoNumberField.FinitePlace.norm_def'andNumberField.FinitePlace.norm_def_intfor versions where thev-adic absolute value is unfolded.NumberField.FinitePlace.mulSupport_finite: thev-adic absolute value of a non-zero element ofKis different from 1 for at most finitely manyv.
Tags #
number field, places, finite places
The norm of a maximal ideal is > 1
Alias of NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm.
The norm of a maximal ideal is > 1
The norm of a maximal ideal as an element of āā„0 is > 1
Alias of NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal.
The norm of a maximal ideal as an element of āā„0 is > 1
The norm of a maximal ideal as an element of āā„0 is ā 0
Alias of NumberField.RingOfIntegers.HeightOneSpectrum.absNorm_ne_zero.
The norm of a maximal ideal as an element of āā„0 is ā 0
The v-adic absolute value on K defined as the norm of v raised to negative v-adic
valuation
Equations
- One or more equations did not get rendered due to their size.
Instances For
Alias of NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv.
The v-adic absolute value on K defined as the norm of v raised to negative v-adic
valuation
Equations
Instances For
Alias of NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def.
The embedding of a number field inside its completion with respect to v.
Instances For
Alias of NumberField.FinitePlace.embedding.
The embedding of a number field inside its completion with respect to v.
Instances For
Equations
- NumberField.instRankOneValuedAdicCompletion v = { hom := { toFun := ā(WithZeroMulInt.toNNReal āÆ), map_zero' := āÆ, map_one' := āÆ, map_mul' := āÆ }, strictMono' := āÆ, nontrivial' := āÆ }
The v-adic completion of K is a normed field.
A finite place of a number field K is a place associated to an embedding into a completion
with respect to a maximal ideal.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Return the finite place defined by a maximal ideal v.
Equations
- NumberField.FinitePlace.mk v = āØNumberField.place (NumberField.FinitePlace.embedding v), āÆā©
Instances For
Alias of NumberField.toNNReal_valued_eq_adicAbv.
The norm of the image after the embedding associated to v is equal to the v-adic absolute
value.
The norm of the image after the embedding associated to v is equal to the norm of v raised
to the power of the v-adic valuation.
The norm of the image after the embedding associated to v is equal to the norm of v raised
to the power of the v-adic valuation for integers.
The v-adic absolute value satisfies the ultrametric inequality.
Alias of NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_add_le_max.
The v-adic absolute value satisfies the ultrametric inequality.
The v-adic absolute value of a natural number is ā¤ 1.
Alias of NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_natCast_le_one.
The v-adic absolute value of a natural number is ā¤ 1.
The v-adic absolute value of an integer is ā¤ 1.
Alias of NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_intCast_le_one.
The v-adic absolute value of an integer is ā¤ 1.
The v-adic norm of an integer is at most 1.
Alias of NumberField.FinitePlace.norm_le_one.
The v-adic norm of an integer is at most 1.
The v-adic norm of an integer is 1 if and only if it is not in the ideal.
Alias of NumberField.FinitePlace.norm_eq_one_iff_not_mem.
The v-adic norm of an integer is 1 if and only if it is not in the ideal.
The v-adic norm of an integer is less than 1 if and only if it is in the ideal.
Alias of NumberField.FinitePlace.norm_lt_one_iff_mem.
The v-adic norm of an integer is less than 1 if and only if it is in the ideal.
Equations
- NumberField.FinitePlace.instFunLikeReal = { coe := fun (w : NumberField.FinitePlace K) (x : K) => āw x, coe_injective' := āÆ }
Alias of NumberField.FinitePlace.mk_apply.
For a finite place w, return a maximal ideal v such that w = finite_place v .
Equations
- w.maximalIdeal = āÆ.choose
Instances For
The equivalence between finite places and maximal ideals.
Equations
- NumberField.FinitePlace.equivHeightOneSpectrum = { toFun := NumberField.FinitePlace.maximalIdeal, invFun := NumberField.FinitePlace.mk, left_inv := āÆ, right_inv := āÆ }