The sublevel sets of a valuation, as additive subgroups

For γ ≠ 0 the set {a | v a < γ} is an additive subgroup: closure under addition is the strict triangle inequality v (x + y) ≤ max (v x) (v y), closure under negation is v (-x) = v x, and γ ≠ 0 is exactly what puts 0 in it.

Mathlib's Valuation.ltAddSubgroup is the same construction indexed by Γ₀ˣ, which forces a LinearOrderedCommGroupWithZero codomain. Much of this repository's valuation theory — continuity in particular — is stated over a LinearOrderedCommMonoidWithZero, where that version is unavailable, and the construction was being repeated by hand at each site. This file states it once at the weaker codomain; no inverses are used, only the strict triangle inequality.

Nothing here mentions a topology. It is deliberately separated from Valuation/Continuous/Basic.lean, whose consumers happened to be the first to need it.

Main definitions

• Valuation.ltAddSubgroupOfNeZero : the sublevel set {a | v a < γ} as an additive subgroup.

References

• Mathlib's Valuation.ltAddSubgroup, the same construction over a value group.

def Valuation.ltAddSubgroupOfNeZero {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation A Γ₀) {γ : Γ₀} (hγ : γ ≠ 0) : AddSubgroup A

A sublevel set of a valuation, as an additive subgroup. For γ ≠ 0 the set {a | v a < γ} is an additive subgroup, by the strict triangle inequality and v (-x) = v x; γ ≠ 0 is what puts 0 in it.

The characteristic lemmas Valuation.mem_ltAddSubgroupOfNeZero and Valuation.coe_ltAddSubgroupOfNeZero are the intended interface: the definition itself is sealed, so downstream code does not depend on how the subgroup is packaged.

Equations

• v.ltAddSubgroupOfNeZero hγ = { carrier := {a : A | v a < γ}, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[simp]

theorem Valuation.mem_ltAddSubgroupOfNeZero {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation A Γ₀} {γ : Γ₀} (hγ : γ ≠ 0) {a : A} : a ∈ v.ltAddSubgroupOfNeZero hγ ↔ v a < γ

@[simp]

theorem Valuation.coe_ltAddSubgroupOfNeZero {A : Type u_1} [Ring A] {Γ₀ : Type u_2} [LinearOrderedCommMonoidWithZero Γ₀] {v : Valuation A Γ₀} {γ : Γ₀} (hγ : γ ≠ 0) : ↑(v.ltAddSubgroupOfNeZero hγ) = {a : A | v a < γ}