The characteristic subgroup of a valuation, cofinal values, and fullness #
The characteristic subgroup cΓ_v of Wedhorn, Adic Spaces (arXiv:1910.05934v1), 4.13 —
the convex subgroup of the value group generated by the attained values ≥ 1 — together
with the two value conditions of the Spv (A, I) theory of §4.3 and §7.1 that are stated
against it. They share a file because the fullness condition Γ_v = cΓ_v is precisely a
statement about this subgroup, and the Spv (A, I) membership criterion of Lemma 7.4
combines it with cofinality. Both are formulated
on the value group of v — Mathlib's ValueGroup₀ (.ofClass v), via the restricted
valuation v.restrict — not on the ambient codomain, so they are invariant under valuation
equivalence (IsEquiv.cofinalValue_iff, IsEquiv.hasFullCharacteristicGroup_iff) and can
be consumed on points of the valuation spectrum:
- a value
v ais cofinal if its powers fall below every positive element of the value group — the condition on ideals of definition in Wedhorn Lemma 7.1; vhas full characteristic group if every positive element of the value group is bounded between(v a)⁻¹andv afor somea— the elementwise reading of "Γ_v = cΓ_v", for the characteristic subgroupcΓ_vof Wedhorn 4.13.
These are the two disjuncts of the membership criterion for Spv (A, I): Wedhorn
Lemma 7.4 proves cΓ_v(I) = Γ_v equivalent to "v a is cofinal for every a ∈ I, or
Γ_v = cΓ_v". The microbial condition of Wedhorn Definition 5.46 (existence of a
dependent height-one valuation) is a genuinely different notion and is deliberately not
formalised here.
Main definitions #
Valuation.CofinalValue v a: Powers ofv afall below every positive element of the value group ofv.Valuation.characteristicGenerators vandValuation.characteristicSubgroup v: The attained values≥ 1and the convex subgroupcΓ_vthey generate.Valuation.HasFullCharacteristicGroup v: Every positive element of the value group ofvis bounded by attained values.
Main results #
Valuation.exists_pow_lt_of_forall_cofinalValue: one exponent serves finitely many cofinal values.Valuation.mem_characteristicSubgroup_iff: Membership incΓ_vis bounding by a single attained value≥ 1.Valuation.hasFullCharacteristicGroup_iff_characteristicSubgroup_eq_top: The elementwise fullness condition is exactlycΓ_v = Γ_v.Valuation.characteristicSubgroup_eq_comap_of_isEquivandValuation.valueGroupOrderIso_mem_characteristicSubgroup_iff:cΓ_vis invariant under valuation equivalence, so it descends to points of the valuation spectrum.
References #
- T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, 4.13, Lemma 7.1, Lemma 7.4
The statements are adapted from the AINTLIB development (Apache 2.0), files
projects/AdicSpaces/Adic spaces/SpvAI.lean (the cofinal-value cluster) and
projects/AdicSpaces/Adic spaces/CharacteristicSubgroup.lean (the characteristic-group
cluster), reformulated on the value group.
Cofinal values #
A value v a is cofinal if for every positive γ in the value group of v some
power (v a) ^ n lies strictly below γ (Wedhorn Lemma 7.1: the condition satisfied by
the elements of an ideal of definition).
Equations
- v.CofinalValue a = ∀ (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀), 0 < γ → ∃ (n : ℕ), v.restrict a ^ n < γ
Instances For
The defining property of a cofinal value, on the value group of v.
A uniform exponent for finitely many cofinal values. If every member of a finite set has cofinal value, then a single exponent works for all of them at once.
No bound on the values need be assumed: cofinality already forces v.restrict a ≤ 1, by taking
γ = 1. That is what makes the exponent uniform, since raising a value ≤ 1 to a higher power
only decreases it, so the largest of the individual exponents serves.
Cofinality transports along an equivalence of valuations, through the ordered isomorphism of their value groups.
Cofinality is invariant under valuation equivalence.
The full-characteristic-group condition #
A valuation has full characteristic group if every positive element of its value
group is bounded between (v a)⁻¹ and v a for some a — the elementwise form of
"Γ_v = cΓ_v", for the characteristic subgroup cΓ_v of Wedhorn 4.13. Such a witness
automatically satisfies 1 ≤ v.restrict a, since the two bounds force x⁻¹ ≤ x. This is
the second disjunct of Wedhorn Lemma 7.4(ii); it is weaker than the microbial condition
of Wedhorn Definition 5.46 (on a field it holds for every valuation).
Equations
- v.HasFullCharacteristicGroup = ∀ (γ : (MonoidWithZeroHom.ofClass v).ValueGroup₀), 0 < γ → ∃ (a : A), (v.restrict a)⁻¹ ≤ γ ∧ γ ≤ v.restrict a
Instances For
The defining property of the full-characteristic-group condition.
Strengthened elimination: a bounding witness for a positive γ can be taken with
1 ≤ v.restrict a alongside the two bounds.
The full-characteristic-group condition transports along an equivalence of valuations, through the ordered isomorphism of their value groups.
The full-characteristic-group condition is invariant under valuation equivalence.
Under the full-characteristic-group condition, every positive element of the value
group dominates the inverse of some nonzero value: the existence statement used in the
Γ_v = cΓ_v case of Wedhorn Lemma 7.10.
The characteristic subgroup #
The generators of the characteristic subgroup cΓ_v of Wedhorn 4.13: the values ≥ 1
attained by v, as elements of the value group (Mathlib's valueGroup.mk f r s
represents (f r)⁻¹ * f s, so valueGroup.mk (.ofClass v) 1 a is the value v a).
Equations
- v.characteristicGenerators = {γ : ↥(MonoidWithZeroHom.ofClass v).valueGroup | 1 ≤ γ ∧ ∃ (a : A), v.restrict a = ↑γ}
Instances For
Membership in the generating set: the attained values ≥ 1, in the v.restrict form
consumers hold.
The characteristic subgroup cΓ_v of Wedhorn 4.13: the smallest convex subgroup of
the value group containing the values ≥ 1 attained by v.
Instances For
Universal property: cΓ_v lies inside a convex subgroup exactly when the attained
values ≥ 1 do.
The generators lie in the characteristic subgroup they generate.
Introduction rule. An attained value ≥ 1 lies in the characteristic subgroup,
stated for the ordinary restricted value.
The valueGroup.mk restatement of the introduction rule, for consumers already holding
a representation of the value.
An attained value at least 1 puts its class in cΓ_v. This is the form consumers hold,
since they meet 1 ≤ v a rather than a bound in the value group. The nonvanishing hypothesis
is part of the statement, since the class valueGroup.mk … h is indexed by it.
Equivalent valuations have corresponding characteristic generators.
Invariance under valuation equivalence. The characteristic subgroup is carried into
the characteristic subgroup by the induced value-group isomorphism. Applying this to h.symm
gives the converse inclusion, so cΓ_v is a genuine invariant of the equivalence class and
may be used on points of the valuation spectrum.
Membership form of the invariance.
Fullness as a statement about the characteristic subgroup #
Elimination rule. Membership in cΓ_v is bounding by a single attained value ≥ 1.
The non-obvious direction is that one generator suffices: the attained values ≥ 1 are closed
under multiplication, so the elements they bound already form a convex subgroup.
Fullness is exactly Γ_v = cΓ_v. The elementwise condition of
HasFullCharacteristicGroup says every positive value is bounded by a single attained
value; that is equivalent to the characteristic subgroup exhausting the value group, because
the attained values ≥ 1 are multiplicatively closed and so a single bound already suffices
for the whole convex subgroup they generate.
The generators correspond exactly under the induced value-group isomorphism: both
sides are indexed by the same ring, and orderMonoidIso_spec matches v.restrict a with
w.restrict a.
Not a simp lemma, though its subgroup counterpart is: mem_characteristicGenerators is
already the simp normal form for the left-hand side, so tagging this one fails simpNF
(the left-hand side rewrites to 1 ≤ … ∧ ∃ a, w.restrict a = … before it can fire).
cΓ_v is an invariant of the equivalence class, in membership form.
Equality form of the invariance: cΓ_v is the pullback of cΓ_w.