Coarsening a valuation by a convex subgroup

Collapsing a convex subgroup H of the value units of Γ₀ coarsens any Γ₀-valued valuation: values are pushed along Γ₀ ≃ WithZero Γ₀ˣ → WithZero (Γ₀ˣ ⧸ H), which is monotone precisely because H is convex. The support is unchanged, bounds by 1 survive, and a value that is at most 1 whose unit avoids H lands strictly below 1 — the three facts the height-one generization of Wedhorn's Lemma 7.45 consumes.

Main definitions

• TauCeti.coarsenMapOfValueGroup : the monoid-with-zero map Γ₀ → WithZero (Γ₀ˣ ⧸ H.toSubgroup).
• Valuation.coarsenByUnits : the coarsened valuation.

Main results

• Valuation.coarsenByUnits_supp : coarsening preserves the support.
• Valuation.coarsenByUnits_lt_one_of_notMem : the collapse detects non-membership — a value at most 1 whose unit avoids H drops strictly below 1. (Bounds by 1 come from coarsenMapOfValueGroup_monotone directly; no specialization is exported for them.)
• Valuation.cofinalValue_coarsenByUnits_restrict : coarsening by a proper convex subgroup preserves cofinality of a value. This needs no topology on A.

Provenance

The coarsening construction itself is adapted from AINTLIB (see References), projects/AdicSpaces/Adic spaces/ValuationCoarsening.lean: TauCeti.coarsenMapOfValueGroup, Valuation.coarsenByUnits and the collapse statements about them are that file's, with its local WithZero.mapMonoidWithZeroHom block replaced by Mathlib's WithZero.map' and the composite shaped as in Mathlib's own LinearOrderedCommGroupWithZero locally-finite instance.

Valuation.cofinalValue_coarsenByUnits_restrict is not from that development. It is the topology-free cofinality ingredient of Wedhorn's Remark 7.11(2), not the remark itself: the continuity statement the remark makes is Valuation.IsContinuous.coarsenByUnits_restrict in TauCeti.RingTheory.Huber.Continuous.Coarsen, which consumes this one. The order-level step it rests on is TauCeti.IsCofinalElement.quotientMk, which is Wedhorn Corollary 1.21 and already on hand; nothing about strictness is redone here.

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), around Lemma 7.45.
• C. Birkbeck, AINTLIB, branch dev/adic-spaces, commit 37bbdaeb, projects/AdicSpaces/Adic spaces/ValuationCoarsening.lean.

noncomputable def TauCeti.coarsenMapOfValueGroup {Γ₀ : Type u_1} [LinearOrderedCommGroupWithZero Γ₀] (H : ConvexSubgroup Γ₀ˣ) : Γ₀ →*₀ WithZero (Γ₀ˣ ⧸ H.toSubgroup)

The coarsening map Γ₀ → WithZero (Γ₀ˣ ⧸ H.toSubgroup): identify Γ₀ with WithZero Γ₀ˣ and collapse H.

Equations

• TauCeti.coarsenMapOfValueGroup H = (WithZero.map' (QuotientGroup.mk' H.toSubgroup)).comp OrderMonoidIso.withZeroUnits.symm.toMonoidWithZeroHom

theorem TauCeti.coarsenMapOfValueGroup_monotone {Γ₀ : Type u_1} [LinearOrderedCommGroupWithZero Γ₀] (H : ConvexSubgroup Γ₀ˣ) : Monotone ⇑(coarsenMapOfValueGroup H)

The coarsening map is monotone; convexity of H is what orders the quotient.

@[simp]

theorem TauCeti.coarsenMapOfValueGroup_apply_coe {Γ₀ : Type u_1} [LinearOrderedCommGroupWithZero Γ₀] (H : ConvexSubgroup Γ₀ˣ) (g : Γ₀ˣ) : (coarsenMapOfValueGroup H) ↑g = ↑((QuotientGroup.mk' H.toSubgroup) g)

The coarsening map sends the value of a unit to its class.

noncomputable def Valuation.coarsenByUnits {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (H : TauCeti.ConvexSubgroup Γ₀ˣ) : Valuation R (WithZero (Γ₀ˣ ⧸ H.toSubgroup))

Coarsening a valuation by a convex subgroup of the units of its value monoid.

Equations

• v.coarsenByUnits H = Valuation.map (TauCeti.coarsenMapOfValueGroup H) ⋯ v

@[simp]

theorem Valuation.coarsenByUnits_apply {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (H : TauCeti.ConvexSubgroup Γ₀ˣ) (r : R) : (v.coarsenByUnits H) r = (TauCeti.coarsenMapOfValueGroup H) (v r)

Coarsening applies the coarsening map to each value.

theorem Valuation.coarsenByUnits_lt_one_of_notMem {R : Type u_1} [Ring R] {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation R Γ₀) (H : TauCeti.ConvexSubgroup Γ₀ˣ) {a : R} (ha_ne : v a ≠ 0) (ha_le : v a ≤ 1) (hm : Units.mk0 (v a) ha_ne ∉ H) : (v.coarsenByUnits H) a < 1

A value at most 1 whose unit avoids H lands strictly below 1 after coarsening.

@[simp]

theorem Valuation.coarsenByUnits_supp {S : Type u_3} [CommRing S] {Γ₀ : Type u_4} [LinearOrderedCommGroupWithZero Γ₀] (v : Valuation S Γ₀) (H : TauCeti.ConvexSubgroup Γ₀ˣ) : (v.coarsenByUnits H).supp = v.supp

Coarsening preserves the support.

theorem Valuation.cofinalValue_coarsenByUnits_restrict {Γ₀ : Type u_2} [LinearOrderedCommGroupWithZero Γ₀] {A : Type u_3} [Ring A] {v : Valuation A Γ₀} {H : TauCeti.ConvexSubgroup (MonoidWithZeroHom.ofClass v).ValueGroup₀ˣ} (hH : H ≠ ⊤) {a : A} (hcof : v.CofinalValue a) : (v.restrict.coarsenByUnits H).CofinalValue a

Coarsening by a proper convex subgroup preserves cofinality of a value. This is the half of Wedhorn Remark 7.11(2) that properness is needed for: the coarsening map is monotone but not strictly so, and properness is exactly what supplies the room to recover a strict inequality.

The recovery itself is not redone here. Cofinality of v a says that the powers of the unit v a fall below every element of the value group, which is TauCeti.IsCofinalElement for that group; TauCeti.IsCofinalElement.quotientMk — Wedhorn Corollary 1.21 — carries that to the quotient by H, and properness is the hypothesis it asks for. What is left is bookkeeping: the coarsened value monoid embeds in WithZero (Γˣ ⧸ H), so a cofinal element of the whole quotient group is in particular below every value the coarsened valuation attains.