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 ValFldPadExactElt, 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 ValFldPadExactElt, 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 ValFldPadExactElt (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 ValFldPadExactElt, and defined pointwise otherwise.
'diff' (v :: Val, w :: Val)
-> Val
Diff. For ValFldPadExactElt, 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 ValFldPadExactElt 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.
ValFldPadExactElt
Represents the valuation of a p-adic number.
Creation
ValFldPadExactElt_IsCoercible (v)
ValFldPadExactElt_IsCoercible (v :: ValFldPadExactElt)
ValFldPadExactElt_IsCoercible (v :: RngIntElt)
ValFldPadExactElt_IsCoercible (v :: Infty)
ValFldPadExactElt_IsCoercible (v :: ExtReElt)
ValFldPadExactElt_IsCoercible (v :: FldRatElt)
-> BoolElt, Any
True if v is coercible to a ValFldPadExactElt, and the coerced value.
IsPromotable (v :: ValFldPadExactElt, w)
-> BoolElt, Any, Any
True if v and w are promotable to a common type.
ValFldPadExactElt_Make (v)
-> ValFldPadExactElt
A ValFldPadExactElt with value v.
Special values
ValFldPadExactElt_Infinity ()
-> ValFldPadExactElt
The valuation Infinity.
ValFldPadExactElt_NegInfinity ()
-> ValFldPadExactElt
The valuation -Infinity.
ValFldPadExactElt_Zero ()
-> ValFldPadExactElt
The valuation 0.
Other operations
IsFinite (v :: ValFldPadExactElt)
-> BoolElt
True if v is finite, i.e. an integer or rational.
IsIntegral (v :: ValFldPadExactElt)
-> BoolElt, RngIntElt
True if v has an integer value, and the value if so.
IntegerValue (v :: ValFldPadExactElt)
-> RngIntElt
The value of v coerced to an integer.
Ceiling (v :: ValFldPadExactElt)
-> ValFldPadExactElt
The integer valuation larger than v, or just v if infinite.
ExactpAdics_Val (x :: FldPadElt)
-> ValFldPadExactElt
The valuation of x.
ExactpAdics_APr (x :: FldPadElt)
-> ValFldPadExactElt
The absolute precision of x.
ValRngUPolElt_FldPadExact
Represents the valuation of a univariate polynomial over a p-adic field.
Creation
ValRngUPolElt_FldPadExact_IsCoercible (v)
ValRngUPolElt_FldPadExact_IsCoercible (v :: ValRngUPolElt_FldPadExact)
ValRngUPolElt_FldPadExact_IsCoercible (v :: AssocDflt)
-> BoolElt, Any
True if v is coercible to a ValRngUPolElt_FldPadExact.
IsPromotable (v :: ValRngUPolElt_FldPadExact, w)
-> BoolElt, Any
True if v and w are promotable to a common type.
ValRngUPolElt_FldPadExact_IsCoercible (dflt, v)
ValRngUPolElt_FldPadExact_IsCoercible (dflt :: ValFldPadExactElt, v)
-> BoolElt, Any
True if v is coercible to a ValRngUPolElt_FldPadExact with given default.
ValRngUPolElt_FldPadExact_Make (v)
-> ValRngUPolElt_FldPadExact
A ValRngUPolElt_FldPadExact with value v.
ValRngUPolElt_FldPadExact_Make (x, y)
-> ValRngUPolElt_FldPadExact
Same as ValRngUPolElt_FldPadExact_Make(DefaultAssociativeArray(x,y)).
ValRngUPolElt_FldPadExact_Make (x, y, z)
-> ValRngUPolElt_FldPadExact
Same as ValRngUPolElt_FldPadExact_Make(DefaultAssociativeArray(x,y,z)).
Special values
ValRngUPolElt_FldPadExact_Infinity ()
-> ValRngUPolElt_FldPadExact
The valuation Infinity.
ValRngUPolElt_FldPadExact_NegInfinity ()
-> ValRngUPolElt_FldPadExact
The valuation -Infinity.
ValRngUPolElt_FldPadExact_Zero ()
-> ValRngUPolElt_FldPadExact
The valuation 0.
Other operations
Value (v :: ValRngUPolElt_FldPadExact)
-> AssocDflt
The underlying associative array of values.
Ceiling (v :: ValRngUPolElt_FldPadExact)
-> ValRngUPolElt_FldPadExact
The integer valuation larger than v, or just v if infinite.
'&join' (v :: ValRngUPolElt_FldPadExact)
-> ValFldPadExactElt
The join of the valuations at each coefficient. Equivalent to “&join Image(Value(v))”.
'&meet' (v :: ValRngUPolElt_FldPadExact)
-> ValFldPadExactElt
The meet of the valuations at each coefficient. Equivalent to “&meet Image(Value(v))”.
'@' (i :: RngIntElt, v :: ValRngUPolElt_FldPadExact)
-> ValFldPadExactElt
The valuation of coefficient i.
ShiftSlope (v :: ValRngUPolElt_FldPadExact, s)
-> ValRngUPolElt_FldPadExact
Adds i*s onto v(i).
ExactpAdics_Val (f :: RngUPolElt[FldPad])
-> ValRngUPolElt_FldPadExact
The valuation of f.
ExactpAdics_APr (f :: RngUPolElt[FldPad])
-> ValRngUPolElt_FldPadExact
The absolute precision of f.