Restricting a valuation to cΓ_v(I) #
Wedhorn, Adic Spaces (arXiv:1910.05934v1), §7.1.2.
Valuation.restrictToConvex restricts a valuation to an arbitrary convex subgroup of the units
of its value monoid. This file specialises it to the convex subgroup that matters for
Spv (A, I): the characteristic subgroup cΓ_v(I) of an ideal, from Wedhorn's Definition 7.3.
Two things have to be arranged. cΓ_v(I) lives in the value group, so it is transported onto
the units of the value monoid by ConvexSubgroup.comapUnitsWithZero; and the restriction needs
cΓ_v(I) to absorb every attained value ≥ 1, which holds because it contains cΓ_v.
The point-level map on Spv A that Wedhorn's retraction r_I is built from lives in
TauCeti.AlgebraicGeometry.AdicSpace.RestrictToIdeal.
Main definitions #
Valuation.RestrictedValues: the value monoid the restriction lands in.Valuation.restrictToIdeal: the restricted valuationv|cΓ_v(I).
Main results #
Valuation.restrictToIdeal_apply_of_notMem,Valuation.restrictToIdeal_apply_of_eq_zero: the two vanishing branches.Valuation.restrictToIdeal_eq_zero_iff: where the restriction vanishes, totally.Valuation.restrictToIdeal_le_iff: how restricted values compare, totally.Valuation.restrictToIdeal_ne_zero_of_le: the restriction keeps every value above a kept value.Valuation.exists_mem_restrictToIdeal_ne_zero: Wedhorn Lemma 7.5(3), that the restriction does not vanish identically onIunlessvdoes.Valuation.restrictToIdeal_ne_zero_of_isAdmissible: it does not kill a denominator dominating an admissible numerator set.
The characterisation lemmas — the vanishing branches, restrictToIdeal_eq_zero_iff and
restrictToIdeal_le_iff — are phrased through cΓ_v(I) itself or through vanishing of the
restriction, so a consumer of them never names the transport. one_le_restrictToIdeal mentions
neither, being an order fact about v.restrict.
The transport is named by four declarations, each unavoidably. RestrictedValues is the
transported subgroup with a zero adjoined, and the private restrictToIdeal_def is the
definitional unfolding and so carries the boundedness hypothesis over it. The two comparison
lemmas against an abstract bound, coe_le_restrictToIdeal_iff and restrictToIdeal_lt_coe_iff,
quantify over a member of that subgroup: their whole point is to compare a restricted value
against a bound arriving from the value group rather than from a ring element, and such a bound
is an element of the transported subgroup. A cofinality argument needs them in that form.
References #
- T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, §7.1.2
Provenance #
The construction is the one called restrictIdeal in AINTLIB
(github.com/CBirkbeck/AINTLIB, Apache-2.0), branch dev/adic-spaces at commit
37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, project projects/AdicSpaces/, file
Adic spaces/CharacteristicSubgroup.lean, built there on restrictToConvexBounded. The
port was checked against that source rather than copied: AINTLIB's cGammaIdeal is already
phrased on Γ₀ˣ and so needs no transport, whereas cΓ_v(I) here lives in the value group and
is carried across by ConvexSubgroup.comapUnitsWithZero.
The value monoid of the restricted valuation: cΓ_v(I), transported onto the units of the
value monoid, with a zero adjoined.
Equations
- v.RestrictedValues I hfg = WithZero ↥(v.characteristicSubgroupOfIdeal I hfg).comapUnitsWithZero.toSubgroup
Instances For
RestrictedValues is a linearly ordered commutative group with zero.
Equations
Wedhorn §7.1.2: the restriction v ↦ v|cΓ_v(I). Values whose unit lies in cΓ_v(I) are
kept; every other value is sent to 0.
Equations
- v.restrictToIdeal I hfg = v.restrict.restrictToConvex (v.characteristicSubgroupOfIdeal I hfg).comapUnitsWithZero ⋯
Instances For
The restriction, characterised through cΓ_v(I) #
restrictToIdeal keeps or discards a value according to membership in the transported
cΓ_v(I), which is not the form a consumer holds: the introduction rules for cΓ_v(I) speak
about the value group. The bridge below converts between the two, and the lemmas after it are
stated so that no consumer has to unfold the definition or mention the transport.
Off cΓ_v(I), the restriction vanishes. The hypothesis is non-membership in cΓ_v(I)
itself; the transport is applied internally.
Not @[simp]: restrictToIdeal_eq_zero_iff is the simp-normal form for a vanishing
restriction, and it rewrites this lemma's left-hand side, which simpNF rejects.
Where the restriction vanishes at a nonzero value, stated through cΓ_v(I) itself.
restrictToIdeal_eq_zero_iff is the total form, and is the @[simp] one: tagging this
branch too makes its left-hand side reducible by that lemma, which simpNF rejects.
Where the restriction vanishes, totally: at the zeros of v, and where v is nonzero
but its value escapes cΓ_v(I). restrictToIdeal_eq_zero_iff_of_ne is the nonzero branch, in
the form consumers holding a nonvanishing hypothesis want.
On values kept by the restriction, the order is both preserved and reflected — stated
through membership in cΓ_v(I) itself.
Not @[simp]: restrictToIdeal_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 value discarded by the restriction is below
everything, a kept value is below only kept values, and two kept values compare exactly as they
did under v. restrictToIdeal_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, which
restrictToIdeal_eq_zero_iff turns into membership in cΓ_v(I); so a caller never has to name
the transported subgroup.
The companion of restrictToIdeal_lt_coe_iff with the member on the left.
Comparing a restricted value against an abstract member of the transported cΓ_v(I),
back in the value monoid of v. This is the form a cofinality argument needs, where the
bound comes from the value group rather than from a ring element.
A value at least 1 stays at least 1: cΓ_v(I) keeps every attained value ≥ 1.
Wedhorn §7.1.2: the restricted valuation has full characteristic subgroup for I. This
is the valuation-level content of the landing law — the restriction v|cΓ_v(I) satisfies the very
condition that cuts out Spv (A, I). The point-level statement is
TauCeti.ValuationSpectrum.restrictToIdeal_mem_spvOfIdeal.
The proof is Wedhorn's case split on whether I meets cΓ_v, each branch above.
A value whose class lies in cΓ_v(I) is kept by the restriction. The contrapositive of
the nonzero branch of restrictToIdeal_eq_zero_iff, in the form a consumer holding a membership
proof wants.
The restriction keeps every value above a kept value. A value discarded by v|cΓ_v(I)
cannot dominate a kept one: the kept value's class lies in cΓ_v(I), and a larger class is
either below 1, so convexity puts it in, or above 1, so it is an attained characteristic
value and cΓ_v ≤ cΓ_v(I) puts it in.
This is the monotonicity that makes r_I a horizontal specialisation; Wedhorn uses it
without comment in the proof of Lemma 7.5(iii).
Wedhorn Lemma 7.5(3). If v does not vanish identically on I, neither does its
restriction: v(I) ≠ 0 implies r_I(v)(I) ≠ 0, so I is not contained in the support of the
restricted valuation. This is the form Wedhorn's Theorem 7.10 consumes.
The restriction does not kill an admissible denominator. If u dominates a set
T with I ⊆ √((T ∪ {u}) · A) and v u ≠ 0, then v|cΓ_v(I) keeps u.
This is one of the auxiliary claims in Wedhorn's proof of Lemma 7.5(1) — step (iii) there — and
it is what lets restrictToIdealCodRestrict_preimage compute the preimage of a rational
subset.