The ideal of cofinal values #
Wedhorn, Adic Spaces (arXiv:1910.05934v1), Lemma 7.1. For a valuation v on a
commutative ring and a convex subgroup H of its value group strictly containing the
characteristic subgroup cΓ_v, the elements whose value is cofinal for H form a radical
ideal. Almost all of this needs only a ring: Ideal A is Submodule A A, a left ideal,
and left absorption is exactly what the multiplicative step supplies, so the predicate, the
ideal, its membership lemma and its properness are all stated at [Ring A]. Commutativity
enters at one point, radicality, where Mathlib's Ideal.IsRadical requires it — and that is
the statement carrying Wedhorn's name, since Lemma 7.1 is about a commutative ring. This is
the object Wedhorn's §7.1
uses to reduce the construction of cΓ_v(I)
(Definition 7.3) to a finite generating set, and it is used twice in the proof of Lemma 7.2:
once to pass from generators to the whole ideal, and once to replace I by its radical.
Cofinality here is stated for a value that may vanish, since 0 is cofinal for every
subgroup — that is why the vanishing case is a case split in the proofs below rather than
something derivable from cofinality.
Main definitions #
Valuation.CofinalValueFor v H a: The powers ofv afall below every member of the subgroupHof the value group.Valuation.cofinalIdeal v hH: Those elements, as an ideal.
Main results #
Valuation.cofinalValueFor_closure_singleton_of_le: A value bounded byh < 1is cofinal for the convex subgrouphgenerates — below1, a larger value generates a smaller subgroup.Valuation.cofinalValueFor_iff_isCofinalElement: For a non-vanishing value, the valuation-side predicate agrees with the group-sideIsCofinalElementon the value group. This is what lets Wedhorn Proposition 1.20 apply.Valuation.isRadical_cofinalIdeal: The ideal is radical — therad(c) = chalf of Lemma 7.1 — withcofinalValueFor_pow_iffthe elementwise form behind it.Valuation.cofinalIdeal_ne_top: It is proper, a corollary of the ring-levelValuation.not_cofinalValueFor_one.Valuation.cofinalValueFor_top_iff: At the whole value group the predicate is the ambientCofinalValue.Valuation.cofinalValueFor_neg_iff: cofinality is invariant under negation, withCofinalValueFor.subthe resulting difference closure.
Implementation notes #
Ported from the AINTLIB adic-spaces development (aintlib-adic-spaces, revision 37bbdaeb9,
projects/AdicSpaces/Adic spaces/SpvAI.lean, Apache-2.0), whose Valuation.CofinalValue and
its lemmas supplied the statement shapes and the proof skeleton for the cofinality predicate
and its closure properties. The cofinality bridge is rebuilt here against Mathlib's
MonoidWithZeroHom.valueGroup API rather than the parallel value-group construction used
there.
References #
- T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Lemma 7.1
v a is cofinal for the subgroup H of the value group: its powers fall
below every member of H (Wedhorn Definition 1.16, at a value that may vanish).
Instances For
The defining property of cofinality relative to a subgroup.
Deliberately not @[simp]: the right-hand side is the unfolded bounded quantifier, so tagging
it would rewrite a ∈ cofinalIdeal v hH past the named predicate and into raw ∀ … ∃ … form.
mem_cofinalIdeal is the intended normal form.
Cofinality for H is downward closed in the value.
Cofinality for a larger convex subgroup implies cofinality for a smaller one: the monotonicity that makes the family in Wedhorn Lemma 7.2 downward closed.
A vanishing value is cofinal for every subgroup (Wedhorn's remark after
Definition 1.16: the adjoined base 0 is cofinal for every subgroup).
Zero has cofinal value.
A sum of cofinal-value elements has cofinal value: v (a + b) ≤ max (v a) (v b).
Cofinality is invariant under negation, since v (-a) = v a.
A difference of cofinal-value elements has cofinal value.
Multiplying by an element of value at most 1 preserves cofinality.
For a nonzero value, cofinality for H is cofinality of the corresponding element of
the value group: the bridge between the valuation-side and group-side predicates.
Wedhorn Lemma 7.1, the multiplicative step. Below the strict-containment threshold
cΓ_v < H, cofinality for H is preserved by multiplication by an arbitrary ring element.
A value bounded above by h < 1 is cofinal for the convex subgroup h generates. This is
the inversion at the heart of Wedhorn's choice of h := max { v t : t ∈ T }: below 1 a
larger value generates a smaller convex subgroup, so the maximum yields the subgroup that
every generator is cofinal for.
A cofinal value lies strictly below 1.
A power has cofinal value exactly when the element does (for a positive exponent):
the ingredient of rad c = c in Wedhorn Lemma 7.1.
Cofinality for the whole value group is the ambient CofinalValue: the positive elements
of ValueGroup₀ are exactly the coercions of the group elements. This is the bridge between
the subgroup-relative predicate here and the one already on main.
1 never has cofinal value: v 1 = 1, which is not below itself. Stated for the predicate
so that it needs only a ring — properness of the ideal below is a corollary.
The ideal of cofinal values #
Ideal A is Submodule A A, i.e. a left ideal, and CofinalValueFor.mul_left gives exactly left
absorption — which is exactly what Ideal A = Submodule A A asks for. So the ideal and its
membership and properness statements need only a ring; commutativity enters one step later,
at radicality, where Mathlib's Ideal.IsRadical requires it. Wedhorn states Lemma 7.1 over a
commutative ring, and it is isRadical_cofinalIdeal below that carries the lemma's name.
The elements whose value is cofinal for H, as an ideal — a left ideal in general,
since Ideal A is Submodule A A and CofinalValueFor.mul_left supplies left absorption.
Over a commutative ring this is the ideal of Wedhorn, Lemma 7.1, whose radicality is
isRadical_cofinalIdeal.
Equations
- v.cofinalIdeal hH = { carrier := {a : A | v.CofinalValueFor H.toSubgroup a}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
Instances For
Membership in the ideal is the cofinality predicate. This is the intended simp-normal form
for cofinalIdeal; cofinalValueFor_def deliberately does not unfold it further.
The ideal of cofinal values is proper: 1 has value 1, which is not cofinal.
Radicality #
Wedhorn Lemma 7.1. Over a commutative ring the ideal of cofinal values is radical.
Commutativity is needed only here, for Mathlib's Ideal.IsRadical.