Restricting a valuation to a convex subgroup #
Wedhorn, Adic Spaces (arXiv:1910.05934v1), §7.1.2.
Given a valuation v and a convex subgroup H of the units of its value monoid, the
restriction of v to H keeps those values whose unit lies in H and sends every other
value to 0. It is the construction underlying the retraction r_I : Spv A → Spv (A, I).
That this is again a valuation is not formal: multiplicativity fails for an arbitrary subgroup,
because two units outside H can have a product inside it. Convexity of H together with the
hypothesis that H absorbs every attained value ≥ 1 is what rules that out: a unit outside
H must lie below 1, so a product of two such is below each factor.
Main definitions #
Valuation.restrictToConvex: the restricted valuation, with codomainWithZero H.toSubgroup.
Main results #
Valuation.restrictToConvex_apply_of_mem,Valuation.restrictToConvex_apply_of_notMemandValuation.restrictToConvex_apply_of_eq_zero: the three branches, which are the intended interface — the definition itself is aditechain and is not meant to be unfolded.Valuation.restrictToConvex_eq_zero_iff: where the restriction vanishes, totally.Valuation.restrictToConvex_le_iff: how restricted values compare, totally.Valuation.restrictToConvex_lt_coe_iffandValuation.coe_le_restrictToConvex_iff: a restricted value compared against an abstract member ofH.Valuation.one_le_restrictToConvex: a value at least1stays at least1. The converse bounds are the generalrestrictToConvex_le_iffandrestrictToConvex_lt_coe_iffat1.Valuation.restrictToConvex_mul_inv_le_oneandValuation.one_lt_restrictToConvex_mul_inv: the two directions of the quotient bound, and they are not the same comparison. Dividing by a kept value that dominates the numerator (v a ≤ v b) lands at or below1; the quotient is strictly above1in the opposite case, when the numerator strictly dominates the kept divisor (v b < v a). Wedhorn's Lemma 7.44 extension indexes its divisor by a power, and instantiates these atb = t ^ n—pow_memsupplies the membership,map_powandinv_powthe rewriting.Valuation.supp_le_restrictToConvex_supp: the support can only grow.Valuation.mk0_mem_of_inv_le_of_le:Hkeeps every value bracketed by an attained value≥ 1and its inverse — so the characteristic values ofvall survive the restriction. (A convex subgroup of a value group has to be carried onto the units of the value monoid before it can be restricted to; that transport ships with the retraction that needs it.)
References #
- T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, §7.1.2
Provenance #
Ported from AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit
37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, project projects/AdicSpaces/,
file Adic spaces/ValuationContinuity.lean, declarations convexRestrictFun and
restrictToConvexBounded, together with the bound and support lemmas ported here:
supp_le_restrictToConvex_supp (:724). The source's restrictToConvex_mul_inv_pow_le_one (:814)
and one_lt_restrictToConvex_mul_inv_pow (:839) are generalised rather than ported: their
content is here as restrictToConvex_mul_inv_le_one and
one_lt_restrictToConvex_mul_inv, stated for an arbitrary kept divisor, of which the
source's power forms are the case b = t ^ n. That file's restrictToConvex_le_one (:733) and
restrictToConvex_lt_one_of_val_lt_one (:786) are deliberately not ported: here they are
one-line specializations of restrictToConvex_le_iff and restrictToConvex_lt_coe_iff at 1,
so a caller applies those directly. That development carries
set_option backward.isDefEq.respectTransparency false on the definition and several proofs;
TauCeti's CI forbids set_option, and it turns out not to be needed — stating the dite chain
as restrictToConvexFun_unfold and rewriting through it, rather than unfolding the definition in
place, lets the instances be synthesised in the consumer's context.
The restriction of v to a convex subgroup H of its value units. Values whose unit
lies in H are kept; every other value is sent to 0.
The hypothesis says that H absorbs each attained value ≥ 1. It cannot be dropped: without it
the result is not multiplicative, since two units outside H may have a product inside it.
Equations
- v.restrictToConvex H hH = { toFun := Valuation.restrictToConvexFun✝ v H, map_zero' := ⋯, map_one' := ⋯, map_mul' := ⋯, map_add_le_max' := ⋯ }
Instances For
On a value whose unit lies in H, the restriction keeps that unit.
Off H, the restriction vanishes.
The restriction vanishes wherever v does.
On values whose units lie in H, the restriction both preserves and reflects the order.
This is what lets an order fact about v be moved to the restricted valuation without
unfolding either.
Not @[simp]: restrictToConvex_le_iff is the simp-normal form for a comparison of restricted
values, and it rewrites this lemma's left-hand side, which simpNF rejects.
Comparison after restriction, totally. A discarded value sits at the bottom, so it is
below everything; a kept value is below only kept values; and two kept values compare exactly
as they did under v. restrictToConvex_le_iff_of_mem is the both-kept branch, in the form
consumers holding membership hypotheses want.
The side conditions are stated as vanishing of the restriction rather than as membership in H,
so that restrictToConvex_eq_zero_iff discharges them without the caller naming H.
A value at least 1 stays at least 1 under the restriction. Such a value is always kept,
since H absorbs the attained values ≥ 1 by hypothesis.
A valuation bounded by 1 satisfies the absorption hypothesis vacuously. If v r ≤ 1
for every r, then an attained value that is also ≥ 1 equals 1, so its unit is 1 and lies
in every convex subgroup. This is what lets restrictToConvex be applied to a valuation of a
ring of definition without first choosing H.
H keeps every value sandwiched between an attained value ≥ 1 and its inverse. Since
H absorbs the attained values ≥ 1, and is convex, it absorbs everything they bracket —
which is exactly the characteristic values of v.
The restriction vanishes at a nonzero value exactly when its unit avoids H.
Not @[simp]: restrictToConvex_eq_zero_iff is the simp-normal form for a vanishing
restriction, and tagging this branch too would make normalisation depend on whether a
nonvanishing proof happens to be available.
Comparing a restricted value against an arbitrary element of H, back in Γ₀.
Unlike restrictToConvex_le_iff, which relates two restricted values, this compares a
restricted value with an abstract member of H — the form a cofinality argument needs, where
the bound comes from the value group rather than from a ring element.
The discarded branch is the interesting one: a unit outside H lies below 1, and convexity
then puts it strictly below every member of H, since otherwise H would have to contain
it.
The companion of restrictToConvex_lt_coe_iff with the member of H on the left.
Both discarded branches work the same way: a value the restriction throws away sits strictly
below every member of H, so no member of H is below it.
Where the restriction vanishes, totally: at the zeros of v, and where v is nonzero
but its unit avoids H. restrictToConvex_eq_zero_iff_of_ne is the nonzero branch, in the form
consumers holding a nonvanishing hypothesis want.
Dividing a restricted value by a kept value that dominates it lands at or below 1.
Only the order comparison and membership of the divisor are used; nothing here is special to a
power.
A restricted value strictly dominating a kept value stays strictly above 1 after
dividing by it. As with the ≤ form, only the comparison and the divisor's membership matter.
The support can only grow under the restriction: every zero of v is a zero of the
restricted valuation, alongside the discarded values. Stated over a commutative ring because
Valuation.supp is.