View on GitHub

Exact p-Adics

A Magma package for exact p-adic computation

Valuations

Contents

Introduction

In this package, we define new types to represent valuations of p-adic numbers and polynomials. These are also used to represent precisions.

The valuation of a p-adic number is represented by the type Val_FldPadElt, whose value is either an integer, or positive or negative infinity. Mathematically its values are in $Z := \ZZ \cup {\pm\infty}$. Addition of valuations corresponds to multiplications of p-adics, so we define this. On the other hand, multiplication of two valuations has no natural interpretation, so we do not define this. Taking the minimum of two valuations is defined, since this bounds the valuation of the sum of the corresponding p-adics. Hence $Z$ is more like the tropical ring of integers than the usual ring of integers $\ZZ$. Multiplying by an ordinary integer (scalar multiplication) is defined because this corresponds to exponentiation of p-adic numbers. They are also totally ordered. For convenience, we extend $Z$ to include the rationals $\QQ$ too.

The valuation of a polynomial is (by definition in the package) a function taking an exponent vector to the valuation of the corresponding coefficient. That is, for polynomials of rank $n$, it is a function $\NN^n \to Z^n$, i.e. an element of $Z^{\NN^n}$. They are represented by the type Val_RngUPolElt_FldPad for univariate polynomials and Val_RngMPolElt_FldPad for multivariate polynomials over p-adic fields. Since polynomials by definition have only finitely many non-zero coefficients, the function is constant except for finitely many inputs. We can define a partial ordering on these valuations: $v_1 < v_2$ iff for all $n \in \NN$ then $v_1(n) < v_2(n)$. This partial ordering gives us suprema and infema (defined pointwise), and we can also define addition and scalar multiplication pointwise.

Generic intrinsics

In this section we document intrinsics common to all valuations. Where there are multiple Val inputs, it suffices for only one to be a Val and for them all to be coercible to a common Val type.

'-' (v :: Val)

'+' (v :: Val, w :: Val)

'-' (v :: Val, w :: Val)

-> Val

Negation, addition and subtraction.

This is as normal for Val_FldPadElt, and defined pointwise otherwise. For convenience, we define $\infty-\infty=0$.

'*' (v :: Val, n)

'*' (n, v :: Val)

'/' (v :: Val, n)

-> Val

Scalar multiplication and division. n must be an integer or rational.

'eq' (v :: Val, w :: Val)

'ne' (v :: Val, w :: Val)

'le' (v :: Val, w :: Val)

'lt' (v :: Val, w :: Val)

'ge' (v :: Val, w :: Val)

'gt' (v :: Val, w :: Val)

-> Val

Ordering predicates.

This is as normal for Val_FldPadElt (i.e. a total ordering), and defined pointwise otherwise (i.e. a partial ordering).

'join' (v :: Val, w :: Val)

'meet' (v :: Val, w :: Val)

-> Val

Supremum and infemum.

This is just maximum and minimum for Val_FldPadElt, and defined pointwise otherwise.

'diff' (v :: Val, w :: Val)

-> Val

Diff. For Val_FldPadElt, v diff w is defined to be v if v gt w and otherwise is negative infinity. Otherwise, it is defined pointwise.

If you view the valuation of a compound structure like a multiset, except where the multiplicities on each element are tropical integers instead of normal integers, then diff is like set difference defined via a universal property.

Value (v :: Val)

-> Any

Retrieves the value of the valuation. For Val_FldPadElt this is an integer, rational or infinite. For compound structures it is the underlying function, e.g. for polynomials it is an AssocDflt representing a function which is constant almost everywhere.

IsValidAbsolutePrecision (x, v)

-> Val

True if v may be coerced to a valuation for x. If so, also returns the coerced valuation.

IsValidAbsolutePrecisionDiff (x, v)

-> Val

True if v may be coerced to a valuation for x. If so also returns the coerced valuation. Differs from IsValidAbsolutePrecision in that, for example, for polynomials, if the constant value is not implied by v, then it is taken to be -infinity instead of infinity.

Val_FldPadElt

Represents the valuation of a p-adic number.

Creation

Val_FldPadElt_IsCoercible (v)

Val_FldPadElt_IsCoercible (v :: Val_FldPadElt)

Val_FldPadElt_IsCoercible (v :: RngIntElt)

Val_FldPadElt_IsCoercible (v :: Infty)

Val_FldPadElt_IsCoercible (v :: ExtReElt)

Val_FldPadElt_IsCoercible (v :: FldRatElt)

-> BoolElt, Any

True if v is coercible to a Val_FldPadElt, and the coerced value.

IsPromotable (v :: Val_FldPadElt, w)

-> BoolElt, Any, Any

True if v and w are promotable to a common type.

Val_FldPadElt_Make (v)

-> Val_FldPadElt

A Val_FldPadElt with value v.

Special values

Val_FldPadElt_Infinity ()

-> Val_FldPadElt

The valuation Infinity.

Val_FldPadElt_NegInfinity ()

-> Val_FldPadElt

The valuation -Infinity.

Val_FldPadElt_Zero ()

-> Val_FldPadElt

The valuation 0.

Other operations

IsFinite (v :: Val_FldPadElt)

-> BoolElt

True if v is finite, i.e. an integer or rational.

IsIntegral (v :: Val_FldPadElt)

-> BoolElt, RngIntElt

True if v has an integer value, and the value if so.

IntegerValue (v :: Val_FldPadElt)

-> RngIntElt

The value of v coerced to an integer.

Ceiling (v :: Val_FldPadElt)

-> Val_FldPadElt

The integer valuation larger than v, or just v if infinite.

ExactpAdics_Val (x :: FldPadElt)

-> Val_FldPadElt

The valuation of x.

ExactpAdics_APr (x :: FldPadElt)

-> Val_FldPadElt

The absolute precision of x.

Val_RngUPolElt_FldPad

Represents the valuation of a univariate polynomial over a p-adic field.

Creation

Val_RngUPolElt_FldPad_IsCoercible (v)

Val_RngUPolElt_FldPad_IsCoercible (v :: Val_RngUPolElt_FldPad)

Val_RngUPolElt_FldPad_IsCoercible (v :: AssocDflt)

-> BoolElt, Any

True if v is coercible to a Val_RngUPolElt_FldPad.

IsPromotable (v :: Val_RngUPolElt_FldPad, w)

-> BoolElt, Any

True if v and w are promotable to a common type.

Val_RngUPolElt_FldPad_IsCoercible (dflt, v)

Val_RngUPolElt_FldPad_IsCoercible (dflt :: Val_FldPadElt, v)

-> BoolElt, Any

True if v is coercible to a Val_RngUPolElt_FldPad with given default.

Val_RngUPolElt_FldPad_Make (v)

-> Val_RngUPolElt_FldPad

A Val_RngUPolElt_FldPad with value v.

Val_RngUPolElt_FldPad_Make (x, y)

-> Val_RngUPolElt_FldPad

Same as Val_RngUPolElt_FldPad_Make(DefaultAssociativeArray(x,y)).

Val_RngUPolElt_FldPad_Make (x, y, z)

-> Val_RngUPolElt_FldPad

Same as Val_RngUPolElt_FldPad_Make(DefaultAssociativeArray(x,y,z)).

Special values

Val_RngUPolElt_FldPad_Infinity ()

-> Val_RngUPolElt_FldPad

The valuation Infinity.

Val_RngUPolElt_FldPad_NegInfinity ()

-> Val_RngUPolElt_FldPad

The valuation -Infinity.

Val_RngUPolElt_FldPad_Zero ()

-> Val_RngUPolElt_FldPad

The valuation 0.

Other operations

Value (v :: Val_RngUPolElt_FldPad)

-> AssocDflt

The underlying associative array of values.

Ceiling (v :: Val_RngUPolElt_FldPad)

-> Val_RngUPolElt_FldPad

The integer valuation larger than v, or just v if infinite.

'&join' (v :: Val_RngUPolElt_FldPad)

-> Val_FldPadElt

The join of the valuations at each coefficient. Equivalent to “&join Image(Value(v))”.

'&meet' (v :: Val_RngUPolElt_FldPad)

-> Val_FldPadElt

The meet of the valuations at each coefficient. Equivalent to “&meet Image(Value(v))”.

'@' (i :: RngIntElt, v :: Val_RngUPolElt_FldPad)

-> Val_FldPadElt

The valuation of coefficient i.

ShiftSlope (v :: Val_RngUPolElt_FldPad, s)

-> Val_RngUPolElt_FldPad

Adds i*s onto v(i).

ExactpAdics_Val (f :: RngUPolElt[FldPad])

-> Val_RngUPolElt_FldPad

The valuation of f.

ExactpAdics_APr (f :: RngUPolElt[FldPad])

-> Val_RngUPolElt_FldPad

The absolute precision of f.

Val_RngMPolElt_FldPad

Represents the valuation of a multivariate polynomial over a p-adic field.

Creation

Val_RngMPolElt_FldPad_IsCoercible (v)

Val_RngMPolElt_FldPad_IsCoercible (v :: Val_RngMPolElt_FldPad)

Val_RngMPolElt_FldPad_IsCoercible (v :: AssocDflt)

-> BoolElt, Any

True if v is coercible to a Val_RngMPolElt_FldPad.

IsPromotable (v :: Val_RngMPolElt_FldPad, w)

-> BoolElt, Any

True if v and w are promotable to a common type.

Val_RngMPolElt_FldPad_IsCoercible (dflt, v)

Val_RngMPolElt_FldPad_IsCoercible (dflt :: Val_FldPadElt, v)

-> BoolElt, Any

True if v is coercible to a Val_RngMPolElt_FldPad with given default.

IsValidAbsolutePrecision (x :: RngMPolElt_FldPadExact, v)

-> BoolElt, Any

True if v is coercible to an absolute precision for x. Also returns the coerced value.

IsValidAbsolutePrecisionDiff (x :: RngMPolElt_FldPadExact, v)

-> BoolElt, Any

True if v is coercible to an absolute precision diff for x. Also returns the coerced value.

IsValidRelativePrecision (x :: RngMPolElt_FldPadExact, v)

-> BoolElt, Any

True if v is coercible to a relative precision for x. Also returns the coerced value.

Val_RngMPolElt_FldPad_Make (v)

-> Val_RngMPolElt_FldPad

A Val_RngMPolElt_FldPad with value v.

Val_RngMPolElt_FldPad_Make (x, y)

-> Val_RngMPolElt_FldPad

Same as Val_RngMPolElt_FldPad_Make(DefaultAssociativeArray(x,y)).

Val_RngMPolElt_FldPad_Make (x, y, z)

-> Val_RngMPolElt_FldPad

Same as Val_RngMPolElt_FldPad_Make(DefaultAssociativeArray(x,y,z)).

Special values

Val_RngMPolElt_FldPad_Infinity ()

-> Val_RngMPolElt_FldPad

The valuation Infinity.

Val_RngMPolElt_FldPad_NegInfinity ()

-> Val_RngMPolElt_FldPad

The valuation -Infinity.

Val_RngMPolElt_FldPad_Zero ()

-> Val_RngMPolElt_FldPad

The valuation 0.

Other operations

Ceiling (v :: Val_RngMPolElt_FldPad)

-> Val_RngMPolElt_FldPad

The integer valuation larger than v, or just v if infinite.

'&join' (v :: Val_RngMPolElt_FldPad)

-> Val_FldPadElt

The join of the valuations at each coefficient. Equivalent to “&join Image(Value(v))”.

'&meet' (v :: Val_RngMPolElt_FldPad)

-> Val_FldPadElt

The meet of the valuations at each coefficient. Equivalent to “&meet Image(Value(v))”.

'@' (i :: [RngIntElt], v :: Val_RngMPolElt_FldPad)

-> Val_FldPadElt

The valuation of coefficient i.

'@' (m :: RngMPolElt, v :: Val_RngMPolElt_FldPad)

-> Val_FldPadElt

The valuation of coefficient Exponents(m).

ShiftSlope (v :: Val_RngMPolElt_FldPad, s :: [])

-> Val_RngMPolElt_FldPad

Adds i.s onto v(i).

ExactpAdics_Val (f :: RngMPolElt)

-> Val_RngMPolElt_FldPad

The valuation of f.

ExactpAdics_APr (f :: RngMPolElt)

-> Val_RngMPolElt_FldPad

The absolute precision of f.

Val_Tup_PadExact

Represents the valuation of a tuple of p-adic objects.

Creation

Val_Tup_PadExact_IsCoercible (v)

Val_Tup_PadExact_IsCoercible (v :: Val_Tup_PadExact)

Val_Tup_PadExact_IsCoercible (v :: Tup)

-> BoolElt, Val_Tup_PadExact

True if v is coercible to a Val_Tup_PadExact, and the coerced value.

IsPromotable (v :: Val_Tup_PadExact, w)

-> BoolElt, Any, Any

True if v and w are coercible to a common type.

Val_Tup_PadExact_Make (v)

-> Val_Tup_PadExact

Coerces v to a Val_Tup_PadExact.

Other operations

'@' (i :: RngIntElt, v :: Val_Tup_PadExact)

-> Val_PadExactElt

The valuation in the ith component of v.

'#' (v :: Val_Tup_PadExact)

-> RngIntElt

The number of components in v.

ExactpAdics_Val (t :: Tup)

-> Val_Tup_PadExact

The valuation of t.

ExactpAdics_APr (t :: Tup)

-> Val_Tup_PadExact

The absolute precision of t.