Refactoring to use ValuativeRel instead of Valued

Stream: PR reviews

[Yakov Pechersky]

I'd like to use this thread to track PRs in the Valued -> ValuativeRel refactor. I am planning on doing it in three ways:

• PRs that build API up bottom up for ValuativeRel
• PRs that work backwards from leaf files, replacing usages of Valued with ValuativeRel
• PRs that improve existing Valued usage to make it easier for them to get refactored later

Here are some outstanding PRs in these directions

[Yakov Pechersky]

#26712 (+43/-1): additional API for ValuativeRel

[Yakov Pechersky]

#26713 (+151/-1) (relies on previous): helper instance to get a Valued from ValuativeTopology

[Yakov Pechersky]

#25450 (+272/-30): ideal and submodule versions of Valuation.ltAddSubgroup

[Yakov Pechersky]

#26524 (+35/-22): Valuation.Integers implies IsFractionRing

[Yakov Pechersky]

#26545 (+94/-33): generalizing lemmas about valuation of irreducibles in the subring, so that they can be applied to a Valued (or ValRel in the future)

[Yakov Pechersky]

#26549 (+205/-84) (relies on previous): refactor locally compact proofs to discuss Valued instead of NormedField -- will make it easier to switch to ValRel

[Yakov Pechersky]

I will also be adding soon PRs on interaction of ValuativeRel.IsRankLeOne and Valuation.RankOne (below), as well as NormedField implies ValuativeTopology.

[Yakov Pechersky]

cc @Adam Topaz @Johan Commelin @Filippo A. E. Nuccio @Aaron Liu

[Yakov Pechersky]

#26754 (+79/-7): Valuation.RankOne iff ValuativeRel.isRankLeOne

[Yakov Pechersky]

#26713 (+108/0): helper instance to get a Valued from ValuativeTopology -- now ready for review

[Yakov Pechersky]

#26826 (+19/-12): generalize Valuation.IsEquiv inequality lemmas to not require DivisionRing

[Yakov Pechersky]

#26827 (+296/-12) (includes two above): NormedDivisionRing induces scoped ValuativeRel (substitute for NormedField->Valued)

[Yakov Pechersky]

#26829 (+177/-0): ideal and submodule versions of Valuation.ltAddSubgroup, without lemmas about their clopen-ness for Valued. This is a subset of #25450 to avoid interaction with Valued, as requested by Filippo.

[Yakov Pechersky]

#26833 (+12/-0): MulArchimedean (ValueGroupWithZero R) when IsRankLeOne. I left a proof_wanted for the reverse implication.

[Yakov Pechersky]

#26834 (waiting on #26713, will be +13/-0): add notation of 𝒪[K]

[Filippo A. E. Nuccio]

Wow, thanks for the amazing work (let me also add @María Inés de Frutos Fernández to the thread): just to be sure, are you on the long run thinking about getting rid of Valued (so that it will disappear from mathlib) or refactor its definition by something related to ValuativeRel?

[Yakov Pechersky]

My understanding from the comment thread on the PR that made ValuativeRel is that we'd like to refactor Mathlib to prefer ValuativeRel instead of Valued. Following this my plan is to provide helper instances of how one implies the other, and convert Mathlib results that mention Valued to ones that mention ValuativeRel. Then, deprecate Valued without removing it outright.

This way, downstream users that still rely on Valued can use all the current results, thanks to the helper instances that give ValuativeRel, and can take a gradual approach to refactoring.

[Filippo A. E. Nuccio]

That sounds perfect, but are you sure that there is a way to "deprecate a class"?

[Yakov Pechersky]

We've done such deprecations for class declarations like with the rename of UniformAddGroup to IsUniformAddGroup

[Filippo A. E. Nuccio]

Yes, I agree that you can deprecate some name when it changes, but deprecating a declaration altogether?

[Yakov Pechersky]

One can deprecate a declaration without providing a direct alias reference to the same statement. Like in https://github.com/leanprover-community/mathlib4/blob/master/Mathlib%2FDeprecated%2FOrder.lean

[Filippo A. E. Nuccio]

Excellent, I was unaware of this. Then yes, I agree that your plan looks perfect, including the deprecation instead of direct erasure.

[Yakov Pechersky]

There is a bit of an obstacle in completely generalizing away from NontriviallyNormedField since results on LocallyCompact are phrased using ProperSpace, and ProperSpace requires PseudoMetricSpace. An example result that needs to be generalized to UniformSpace would be docs#NormedField.completeSpace_iff_isComplete_closedBall

[Aaron Liu]

What is a ball without PseudoMetricSpace?

[Yakov Pechersky]

What would be needed here is a complete entourage in the uniformity, such that any entourage can be scaled to be inside this complete entourage.

[Aaron Liu]

what is scaling in a uniform space?

[Aaron Liu]

does Set.univ count as such an entourage?

[Yakov Pechersky]

scaling in a uniform space

[SMul K K] [UniformContinuousConstSMul K K]

[Yakov Pechersky]

Yakov Pechersky said:

#26827 (+296/-12) (includes two above): NormedDivisionRing induces scoped ValuativeRel (substitute for NormedField->Valued)

#26827 is now (+242/-25): it includes some proof refactor to refer to uniform space balls. LMK if that is not useful.

[Yakov Pechersky]

Yakov Pechersky said:

#26834 (waiting on #26713, will be +13/-0): add notation of 𝒪[K]

#26834 (+13/-0): add notation of 𝒪[K]

[Yakov Pechersky]

#26874 (+13/-0): ValuativeRel + UniformSpace implies Valued (scoped)

[Yakov Pechersky]

#26885 (+95/-10): ValuativeTopology 𝒪[K] (depends on notation PR)

[Yakov Pechersky]

#26886 (+315/-25, depends on normed field PR): ValuativeRel ℚ_[p] and associated instances

[Yaël Dillies]

Aaron Liu said:

does Set.univ count as such an entourage?

If Set.univ is complete, then sure

[Yakov Pechersky]

#26942 (+236/-14): isomorphism of value groups when compatible

[Yakov Pechersky]

Relies on small API PRs #26939, #26940, #26941. Should help with RankOne refactoring.

[Anatole Dedecker]

Is there no point in keeping Valued purely as a convenient way to have a canonical valuation?

[Anatole Dedecker]

Or is the idea that we should just use Compatible hypotheses?

[Kevin Buzzard]

I don't know. It's not just a canonical valuation, it's also a canonical target monoid, which is what was causing problems.

[Antoine Chambert-Loir]

Imagine you start from a ring, and define a valuation on it. What is the way to get the corresponding topology? For the moment, one has to use Valued, no? Although, of course, the path through ValuationRel will be more natural.

[Aaron Liu]

Something like TopologicalSpace.induced (ValuativeRel.valuation R) (nhdsAdjoint atBot)

[Anatole Dedecker]

I don't think that works.

[Anatole Dedecker]

But indeed one should be able to create the topology from just the relation (and eventually the canonical valuation associated to it).

[Anatole Dedecker]

Related: I commented on #26827 to argue that it would be good to have API allowing to study any/the docs#ValuatedTopology associated to a docs#ValuativeRel through any docs#Valuation.Compatible valuation. Since I don't know how these things are used in practice I may be completely wrong, but I wonder what people here think about this.

[Kevin Buzzard]

The delicate issue here, as Antoine has been keen to stress, is that the naive topology associated to a valuation (pull back sets of the form B_eps := {x : 0 <= x < eps} in the target and these are a basis of nhds of 0 in the domain) is not the correct topology; the issue is that the target type might be gigantic and include e.g. infinitely small elements which are not in the imge of the valuation map, meaning that the corresponding B_eps pulls back to {0} giving you the discrete topology). Indeed this ValuativeRel business is exactly trying to get around that problem.

[Aaron Liu]

Can you give an example?

[Kevin Buzzard]

To put it another way, you can have two valuations which are compatible with the rel, but which introduce different "naive" topologies on the ring

[Filippo A. E. Nuccio]

Another approach (that has been not been deemed very efficient, so I'm developing it mainly for other reasons) is to only look at the range of the valuation, as in #26588 .

[Kevin Buzzard]

Aaron yes: take your favourite ring, which is the p-adic numbers, which has an interesting topology. Put the usual valuation on it, taking values in, say, the non-negative reals. Now change the target groupwithzero by adding in a formal new infinitely small element e, with 0<e but e<epsilon for all real epsilon>0, and then beef up the system to make it a totally ordered group with zero again (so basically add in re^n for n an integer and r a positive real). Now use the same valuation, but now you have a different topology because there are open nhds of 0 in the target which now miss v(x) for all nonzero x (namely open ball centre 0 radius e) and their preimage under v is now just {0} which has mysteriously become open.

[Aaron Liu]

Kevin Buzzard said:

0<e but e<epsilon for all real epsilon>0

I thought the domain was the padics?

[Kevin Buzzard]

The valuation is on the p-adics, I'm altering the target groupwithzero, sorry, I made a typo, now fixed. Thanks.

[Yaël Dillies]

Yes, but the point is that the codomain can a priori be anything

[Kevin Buzzard]

(yeah I made a typo)

[Filippo A. E. Nuccio]

Look at this example
#maths > Question about `Valued.is_topological_valuation` @ 💬
by @Yakov Pechersky , building upon a previous idea of @Jiang Jiedong .

[Aaron Liu]

I thought the target groupwithzero was ValuativeRel.ValueGroupWithZero and you weren't supposed to alter it

[Kevin Buzzard]

My understanding of what Anatole was suggesting is that we talk about the topology associated to an arbitrary valuation which is compatible with the rel, and the technical issue with this is precisely that if you allow arbitrary valuations then you can't control the target groupwithzero.

[Adam Topaz]

There is a middle ground to be had here, which may be what Anatole has in mind (I haven't followed all the discussion the last few hours). Namely, the definition of ValuativeTopology uses ValuativeRel.ValueGroupWithZero in its definition, but all the api lemmas about ValuativeTopology are stated in terms of an arbitrary valuation v satisfying [v.Compatible]. Since ValuativeRel.valuation is compatible, that means that this approach is strictly more general.

[Yakov Pechersky]

The example linked above is showing that the current mathlib Valution.IsEquiv isn't strong enough, which means that I'm afraid that v.Compatible isn't strong enough.

[Adam Topaz]

I'm not sure what you mean @Yakov Pechersky .

[Kevin Buzzard]

Whatever issues we might have with Valuation.IsEquiv, this is the notion which is in the literature so we're stuck with it.

[Aaron Liu]

you could restrict to the range before pulling back a neighborhood of zero

[Adam Topaz]

The lemmas need to hold true for arbitrary valuations v which are compatible

[Kevin Buzzard]

Aaron Liu said:

you could restrict to the range before pulling back a neighborhood of zero

Yes, that's exactly what is done in the literature, although it is more complicated than you might think because the domain is typically a ring, so the image of the valuation is a monoid with zero, and for technical reasons one wants to look at the associated group with zero, so things can get a bit messy.

[Yakov Pechersky]

I'll try to formalize what I mean.

[Kevin Buzzard]

See definition 1.22 (value group, after (c)), and def 1.27 of equiv (one definition using value groups, one using rel) and definition 5.39 (topology associated to a valuation, which has to use the value group rather than the target groupwithzero) of https://arxiv.org/abs/1910.05934

[Anatole Dedecker]

I know about the codomain vs range issue, I’ve talked about this with Antoine a few times. What I had in mind is indeed that all the lemmas for an arbitrary valuation would only refer to balls with radii a quotient of valuations of elements of the ring. And maybe have a predicate like Valuation.DenseAtZero with conditions allowing to take any element in the codomain as a radius.

[Anatole Dedecker]

And again, I agree that doing the definitions in terms of the relation is cleaner. But in practice people may want to use their favorite valuation, no ?

[Adam Topaz]

What is "their favorite valuation"?

[Adam Topaz]

In practice people would prove theorems about valued fields.

[Adam Topaz]

you could argue that $\mathbb{Q}_p$ has a preferred valuation, but I think in practice we would prove theorems about local fields of characteristic zero, instead of just that one example

[Filippo A. E. Nuccio]

FWIW, a lot of the work concerning "playing with the range rather than a random huge group" was being done in #26872, but we're thinking about giving up if you all agree that Valued will disappear. The main problem is that currently toNormedField depends both on RankOne and on Valued: if we refactor RankOne to mean that the range embeds in $\mathbb{R}_{\geq 0}$, we also need to refactor Valued (so that the topology is defined in terms of the valueGroup) for toNormedValued to compile. This might not be too long (or yes? :thinking: ) but if Valued is going to die at any rate, it is probably a waste of time.

[Adam Topaz]

I think the better approach is to define a ValuativeRel.CompatibleNorm class stating that a NormedRing structure is compatible with a ValuativeRel, and provide a constructor toNormedValued that takes a compatible real-valued valuation as a parameter.

[Adam Topaz]

This way NormedRing and ValuativeRel can coexist.

[Yakov Pechersky]

Here's what I mean. I construct a new valuation that is into Zm0 x Zm0 that is compatible with the regular valuation on Q_p, but would induce a different TopologicalSpace if one used its Valuation.subgroups_basis:

instance vothercomp : (other v).Compatible (R := ℚ_[p]) := by
  -- should be a .of_isEquiv constructor
  constructor
  intro x y
  rw [← otherIsEquiv v]
  exact vcomp.rel_iff_le _ _

-- now imagine we had not already had a topology on `Q_[p]`
-- but instead used the valuation's topology like how Valued.mk' does

instance otherv_disc [hp : Fact p.Prime] :
    @DiscreteTopology ℚ_[p] (other v).subgroups_basis.topology := by
  have : Fact p.Prime := hp
  apply @discreteTopology_of_isOpen_singleton_zero _ ((other (v (p := p))).subgroups_basis.topology)
  simp_rw [isOpen_iff_mem_nhds, Set.mem_singleton_iff]
  rintro _ rfl
  rw [(other (v (p := p))).subgroups_basis.hasBasis_nhds_zero.mem_iff]
  obtain ⟨r, hr⟩ := problem (v (p := p))
  refine ⟨r, trivial, fun x ↦ ?_⟩
  simpa [Valuation.ltAddSubgroup] using hr _

-- here, the ValuativeRel is still from the "true" valuation on `ℚ_[p]`
example [hp : Fact p.Prime] :
    ¬ @ValuativeTopology ℚ_[p] _ _ (other v).subgroups_basis.topology := by
  have : Fact p.Prime := hp
  letI := (other (v (p := p))).subgroups_basis.topology
  intro H
  have := otherv_disc (p := p)
  have : ({0} : Set ℚ_[p]) ∈ nhds (0 : ℚ_[p]) := mem_nhds_discrete.mpr rfl
  rw [H.mem_nhds_iff] at this
  simp only [Set.subset_singleton_iff, Set.mem_setOf_eq] at this
  obtain ⟨γ, hγ⟩ := this
  obtain ⟨r, s, hr⟩ := valuation_surjective γ.val
  simp_rw [← hr, ← vIsEquiv.lt_div_iff_lt_div] at hγ
   -- multiply by some power of `p`
  obtain ⟨x, hx0, hx⟩ : ∃ x : ℚ_[p], x ≠ 0 ∧ v x * v s.val < v r := sorry
  refine hx0 (hγ x ?_)
  rwa [lt_div_iff₀]
  simp [zero_lt_iff]

[Yakov Pechersky]

The full example is

import Mathlib

open WithZero LinearOrderedCommGroupWithZero

namespace Valuation.IsEquiv

variable {R Γ₀ Γ'₀ : Type*} [Ring R]
  [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀]
  {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀}

theorem eq_zero (h : v₁.IsEquiv v₂) {r : R} : v₁ r = 0 ↔ v₂ r = 0 := by
  have : v₁ r = v₁ 0 ↔ v₂ r = v₂ 0 := h.val_eq
  rwa [v₁.map_zero, v₂.map_zero] at this

lemma div_le_iff_div_le (h : v₁.IsEquiv v₂) {x y z : R} :
    v₁ x / v₁ y ≤ v₁ z ↔ v₂ x / v₂ y ≤ v₂ z := by
  by_cases hy : v₁ y = 0
  · simp [hy, h.eq_zero.mp hy]
  · rw [div_le_iff₀ (zero_lt_iff.mpr hy), div_le_iff₀ (zero_lt_iff.mpr (h.ne_zero.mp hy)),
      ← map_mul, h, map_mul]

lemma le_div_iff_le_div (h : v₁.IsEquiv v₂) {x y z : R} :
    v₁ x ≤ v₁ y / v₁ z ↔ v₂ x ≤ v₂ y / v₂ z := by
  by_cases hz : v₁ z = 0
  · simp [hz, h.eq_zero.mp hz, h.eq_zero]
  · rw [le_div_iff₀ (zero_lt_iff.mpr hz), le_div_iff₀ (zero_lt_iff.mpr (h.ne_zero.mp hz)),
      ← map_mul, h, map_mul]

lemma div_lt_iff_div_lt (h : v₁.IsEquiv v₂) {x y z : R} :
    v₁ x / v₁ y < v₁ z ↔ v₂ x / v₂ y < v₂ z := by
  rw [← le_iff_le_iff_lt_iff_lt, h.le_div_iff_le_div]

lemma lt_div_iff_lt_div (h : v₁.IsEquiv v₂) {x y z : R} :
    v₁ x < v₁ y / v₁ z ↔ v₂ x < v₂ y / v₂ z := by
  rw [← le_iff_le_iff_lt_iff_lt, h.div_le_iff_div_le]

end Valuation.IsEquiv

section

variable {R : Type*} [CommRing R] (v : Valuation R ℤᵐ⁰)

def other : Valuation R (WithZero (ℤᵐ⁰ˣ ×ₗ ℤᵐ⁰ˣ)) where
  toMonoidWithZeroHom := (inr _ _).toMonoidWithZeroHom.comp v.toMonoidWithZeroHom
  map_add_le_max' := by
    intro x y
    simpa using ((inr ℤᵐ⁰ _).monotone' (v.map_add_le_max' x y))

lemma other_apply {x : R} (hx : v x ≠ 0) :
    other v x = WithZero.coe (toLex (1, Units.mk0 (v x) hx)) := by
  -- simp lemmas get in the way
  change (inr _ _) (v x) = _
  simp [inr_eq_coe_inrₗ hx]

lemma otherIsEquiv : v.IsEquiv (other v) := by
  intro r s
  by_cases hr : v r = 0
  · simp [hr, other]
  by_cases hs : v s = 0
  · simp [hs, other]
  simp [other_apply v hr, other_apply v hs, Prod.Lex.toLex_le_toLex, ← Units.val_le_val]

lemma problem :
    ∃ (r : (WithZero (ℤᵐ⁰ˣ ×ₗ ℤᵐ⁰ˣ))ˣ), ∀ x : R, other v x < r → v x = 0 := by
  let r := OrderMonoidHom.inlₗ ℤᵐ⁰ˣ ℤᵐ⁰ˣ
    (OrderMonoidIso.unitsWithZero.symm (Multiplicative.ofAdd (-1)))
  use OrderMonoidIso.unitsWithZero.symm r
  intro x
  contrapose!
  intro hx
  rw [other_apply v hx]
  simp [r, Prod.Lex.toLex_le_toLex, ← Units.val_lt_val, ← Multiplicative.toAdd_lt]

end

variable {p : ℕ} [Fact p.Prime]
open ValuativeRel

@[simp] -- #26942, among others
lemma val_posSubmonoid_ne_zero {R : Type*} [CommRing R] [ValuativeRel R] (x : posSubmonoid R) :
    (x : R) ≠ 0 := by
  have := x.prop
  rw [posSubmonoid_def] at this
  contrapose! this
  simp [this]

noncomputable section
open Classical

def v : Valuation ℚ_[p] ℤᵐ⁰ where
  toFun x := if x = 0 then 0 else WithZero.exp x.valuation
  map_zero' := by simp
  map_one' := by simp
  map_mul' := sorry
  map_add_le_max' := sorry

lemma norm_eq {x : ℚ_[p]} (hx : x ≠ 0) : ‖x‖ = p ^ (WithZero.log (v x)) := by
  sorry

instance vrel : ValuativeRel ℚ_[p] := .ofValuation v
instance vcomp : Valuation.Compatible (R := ℚ_[p]) v := .ofValuation v
lemma vIsEquiv : v.IsEquiv (valuation ℚ_[p]) := isEquiv _ _
instance vtop : ValuativeTopology ℚ_[p] := by
  -- this should use a `.ofHasBasis` constructor that I have in one of my PRs
  constructor
  intro s
  simp only [Metric.mem_nhds_iff, gt_iff_lt]
  constructor
  · rintro ⟨ε, εpos, h⟩
    obtain ⟨x, hx0, hx⟩ : ∃ x : ℚ_[p], x ≠ 0 ∧ ‖x‖ < ε := by sorry
    refine ⟨Units.mk0 (valuation _ x) ?_, h.trans' ?_⟩
    · simp [hx0]
    · intro y
      rcases eq_or_ne y 0 with rfl | hy
      · simp [εpos]
      simp only [Units.val_mk0, ← vIsEquiv.lt_iff_lt, Set.mem_setOf_eq, Metric.mem_ball,
        dist_zero_right]
      intro hyx
      refine hx.trans' ?_
      rw [norm_eq hx0, norm_eq hy]
      refine zpow_lt_zpow_right₀ (by exact_mod_cast Nat.Prime.one_lt Fact.out) ?_
      rwa [WithZero.log_lt_iff_lt_exp, WithZero.exp_log] <;>
      simp [hx0, hy]
  · rintro ⟨γ, h⟩
    obtain ⟨r, s, hr⟩ := valuation_surjective γ.val
    rcases eq_or_ne r 0 with rfl | hr0
    · simp [eq_comm] at hr
    refine ⟨‖r / s‖, ?_, h.trans' ?_⟩
    · rw [norm_eq]
      · refine zpow_pos ?_ _
        exact_mod_cast Nat.Prime.pos Fact.out
      · simp [hr0]
    · intro y
      rcases eq_or_ne y 0 with rfl | hy
      · simp
      simp only [norm_div, norm_eq hr0, norm_eq (val_posSubmonoid_ne_zero s), Metric.mem_ball,
        dist_zero_right, norm_eq hy, ← hr, Set.mem_setOf_eq, ← vIsEquiv.lt_div_iff_lt_div]
      rw [lt_div_iff₀, lt_div_iff₀]
      · rw [← zpow_add₀, zpow_lt_zpow_iff_right₀, ← log_mul, log_lt_iff_lt_exp, exp_log]
        · exact id
        all_goals simp_all [Nat.Prime.one_lt Fact.out, Nat.Prime.ne_zero Fact.out]
      · simp [zero_lt_iff, vIsEquiv.ne_zero]
      · refine zpow_pos ?_ _
        exact_mod_cast Nat.Prime.pos Fact.out

instance vothercomp : (other v).Compatible (R := ℚ_[p]) := by
  -- should be a .of_isEquiv constructor
  constructor
  intro x y
  rw [← otherIsEquiv v]
  exact vcomp.rel_iff_le _ _

-- now imagine we had not already had a topology on `Q_[p]`
-- but instead used the valuation's topology like how Valued.mk' does

instance otherv_disc [hp : Fact p.Prime] :
    @DiscreteTopology ℚ_[p] (other v).subgroups_basis.topology := by
  have : Fact p.Prime := hp
  apply @discreteTopology_of_isOpen_singleton_zero _ ((other (v (p := p))).subgroups_basis.topology)
  simp_rw [isOpen_iff_mem_nhds, Set.mem_singleton_iff]
  rintro _ rfl
  rw [(other (v (p := p))).subgroups_basis.hasBasis_nhds_zero.mem_iff]
  obtain ⟨r, hr⟩ := problem (v (p := p))
  refine ⟨r, trivial, fun x ↦ ?_⟩
  simpa [Valuation.ltAddSubgroup] using hr _

-- here, the ValuativeRel is still from the "true" valuation on `ℚ_[p]`
example [hp : Fact p.Prime] :
    ¬ @ValuativeTopology ℚ_[p] _ _ (other v).subgroups_basis.topology := by
  have : Fact p.Prime := hp
  letI := (other (v (p := p))).subgroups_basis.topology
  intro H
  have := otherv_disc (p := p)
  have : ({0} : Set ℚ_[p]) ∈ nhds (0 : ℚ_[p]) := mem_nhds_discrete.mpr rfl
  rw [H.mem_nhds_iff] at this
  simp only [Set.subset_singleton_iff, Set.mem_setOf_eq] at this
  obtain ⟨γ, hγ⟩ := this
  obtain ⟨r, s, hr⟩ := valuation_surjective γ.val
  simp_rw [← hr, ← vIsEquiv.lt_div_iff_lt_div] at hγ
   -- multiply by some power of `p`
  obtain ⟨x, hx0, hx⟩ : ∃ x : ℚ_[p], x ≠ 0 ∧ v x * v s.val < v r := sorry
  refine hx0 (hγ x ?_)
  rwa [lt_div_iff₀]
  simp [zero_lt_iff]

[Adam Topaz]

But you constructed a topology that does not satisfy ValuativeTopology as it is currently defined. As long as ValuativeTopology doesn’t change, is there still an issue?

[Yakov Pechersky]

Correct. And so what I am saying is that v.IsEquiv v' or v'.Compatible does not promise that if v.subgroups_basis.topology is a ValuativeTopology then v'.sugroups_basis.topology is also a ValuativeTopology.

[Yakov Pechersky]

you constructed a topology that does not satisfy ValuativeTopology as it is currently defined

Rather, I showed that the topology on Q_p as currently defined _is_ a ValuativeTopology, and that a topology coming from other v would not be.

[Adam Topaz]

‘As currently defined’ there refers to the definition of the class ValuativeTopology

[Antoine Chambert-Loir]

Just a note that Valued may disappear, but that will not suppress the task of having a ring R, with some valuation v, and willing to define the corresponding topology on R. This is what is done in the API for Valued.

[Notification Bot]

Norbert Voelker has marked this topic as resolved.

[Notification Bot]

Filippo A. E. Nuccio has marked this topic as unresolved.

[Adam Topaz]

Yakov Pechersky said:

Correct. And so what I am saying is that v.IsEquiv v' or v'.Compatible does not promise that if v.subgroups_basis.topology is a ValuativeTopology then v'.sugroups_basis.topology is also a ValuativeTopology.

I think the point is then that v.subgroup_basis.topology is not the right construction!

[Adam Topaz]

One should rather define the subgroup basis on a ring $R$ as indexed by $R \times \{ r | v r \ne 0\}$, sending $(r,s)$ to the set of all $t$ such that $v(t) \cdot v(s) < v(r)$.

[Adam Topaz]

... or index it by the nonzero elements of the subgroup-with-zero generated by the image of $v$, as others have suggested (the two approaches should yield the same result)

[Adam Topaz]

... or you could go via the route Valuation -> ValuativeRel -> SubgroupBasis

[Yakov Pechersky]

I think the subgroup basis would need to be indexed by a pair of posSubmonoid -- the first element can't be 0. At least that what my experiment below showed. Did I miss something?

import Mathlib

variable {R : Type*} [CommRing R] [ValuativeRel R]

open Topology ValuativeRel

@[simp] -- #26942, among others
lemma val_posSubmonoid_ne_zero (x : posSubmonoid R) :
    (x : R) ≠ 0 := by
  have := x.prop
  rw [posSubmonoid_def] at this
  contrapose! this
  simp [this]

lemma valuation_eq_zero_iff {x : R} :
    valuation R x = 0 ↔ x ≤ᵥ 0 :=
  ValueGroupWithZero.mk_eq_zero _ _

@[simp]
lemma valuation_posSubmonoid_ne_zero (x : posSubmonoid R) :
    valuation R (x : R) ≠ 0 := by
  rw [ne_eq, valuation_eq_zero_iff]
  exact x.prop

abbrev ValuativeRel.rel_lt (x y : R) : Prop := x ≤ᵥ y ∧ ¬ y ≤ᵥ x
notation:50 (name := valuativeRelLt) a:50 " <ᵥ " b:51 => binrel% ValuativeRel.rel_lt a b

lemma rel_lt_iff (x y : R) : x <ᵥ y ↔ x ≤ᵥ y ∧ ¬ y ≤ᵥ x := Iff.rfl

lemma ValuativeTopology.of_hasBasis [TopologicalSpace R] (h : (𝓝 (0 : R)).HasBasis (fun _ ↦ True)
    fun γ : (ValueGroupWithZero R)ˣ ↦ { x | (valuation R) x < γ }) :
    ValuativeTopology R :=
  ⟨by simp [h.mem_iff]⟩

lemma of_hasBasis_pair [TopologicalSpace R]
    (h : (𝓝 (0 : R)).HasBasis (fun rs : R × R ↦ rs.1 ∈ posSubmonoid R ∧ rs.2 ∈ posSubmonoid R)
      fun rs  ↦ { x | x * rs.2 <ᵥ rs.1 }) :
    ValuativeTopology R := by
  refine ValuativeTopology.of_hasBasis (h.to_hasBasis ?_ ?_)
  · rintro ⟨r, s⟩ ⟨hr, hs⟩
    -- by_cases hr : valuation R r = 0
    -- · refine ⟨1, trivial, ?_⟩ -- the choice of unit won't matter here
    --   intro x
    --   simp only [valuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
    --     Units.val_one, Set.mem_setOf_eq]
    --   -- goal is `(x * s) ≤ᵥ r`, which means that since we have `r ≤ᵥ 0`,
    --   -- then we need `x ≤ᵥ 0`, but x was arbitrary
    --   sorry
    refine ⟨Units.mk0 (.mk r ⟨s, hs⟩) ?_, trivial, ?_⟩
    · simpa using hr
    · simp [valuation]
  · rintro γ -
    obtain ⟨r, s, h⟩ := valuation_surjective γ.val
    by_cases hr : valuation R r = 0
    · simp [hr, eq_comm] at h
    · refine ⟨⟨r, s⟩, ⟨by simpa [valuation] using hr, s.prop⟩, ?_⟩
      simp only [← h, Set.setOf_subset_setOf, and_imp]
      intro x hx hx'
      rw [lt_div_iff₀ (by simp [zero_lt_iff])]
      simp [valuation, hx, hx']

[Adam Topaz]

Oh, yes, you're right. So both r and s should satisfy v x \neq 0.

[Kevin Buzzard]

Anatole Dedecker said:

And again, I agree that doing the definitions in terms of the relation is cleaner. But in practice people may want to use their favorite valuation, no ?

What is your favourite $\R_{\geq0}$-valued valuation on $\mathbb{Q}_3(\sqrt{-1})$? There are two canonical ones. There is the one which sends an element to the amount that multiplication by it scales additive Haar measure (cf #25829) which is completely canonical, and then there is the one which is the unique nonarchimedean valuation which extends the standard 3-adic valuation on $\mathbb{Q}_3$; this is also completely canonical, and different; one is the square of the other, just like how the function sending a complex number to the amount it scales additive Haar measure is not the complex norm but its square. So Valued is a bit dangerous because maybe I want two different instances of Valued Q3i NNReal

[Filippo A. E. Nuccio]

Although I agree with the content of @Kevin Buzzard 's comment, the current $\mathfrak{p}$-adic valuation on $\mathbb{Q}_3(\sqrt{-1})$ actually takes values in $\mathbb{Z}^{m0}$ (which is the new notation for $\mathbb{Z}_{m0}$).

[Yakov Pechersky]

#27111: (+3/-0): valuationSubring_integers, a shortcut lemma

[Yakov Pechersky]

#27112 (+127/-0): Int.set_denselyOrdered_iff_subsingleton, but importantly, that subsets of Zm0 are not densely ordered, which is a critical ingredient for DVR of valuation subrings. This PR has some basic DenselyOrdered API as well

[Yakov Pechersky]

#27114 (+10/-0): MonoidWithZeroHom.(m)range_nontrivial, the other ingredient to show that a valuation subring of a Zm0 valuation is a PIR, which implied DVR

[Yakov Pechersky]

#27116 (+24/-6): R-algebras that go to K_v via K maintain FaithfulSMul, which gives helper simp lemmas and golfs proofs

[Yakov Pechersky]

#27117 (+212/-6): combines the 4 PRs above + that the valuation subring of K_v for v : HeightOneSpectrum A is a DVR

[Antoine Chambert-Loir]

Adam Topaz said:

One should rather define the subgroup basis on a ring $R$ as indexed by $R \times \{ r | v r \ne 0\}$, sending $(r,s)$ to the set of all $t$ such that $v(t) \cdot v(s) < v(r)$.

There is a suggestion by @Anatole Dedecker that subgroup basis be indexed by a set and a predicate, similarly to docs#Filter.HasBasis. This would eliminate some (moderately, but still painful) coercion stuff all over the proofs, but requires that someone takes care of this first.

[Yakov Pechersky]

Antoine, does the phrasing of

(h : (𝓝 (0 : R)).HasBasis (fun rs : R × R ↦ rs.1 ∈ posSubmonoid R ∧ rs.2 ∈ posSubmonoid R)
      fun rs  ↦ { x | x * rs.2 <ᵥ rs.1 })

work for you?

Should we also state things using docs#TopologicalSpace.IsTopologicalBasis ?

[Anatole Dedecker]

Sorry, I disappeared for the weekend. First, let me insist that I do not want to block anything: building the theory on top of ValuativeRel is clearly the best thing to do, and the API can be cleaned up a bit later.

Let me answer things a bit out of order.

Adam Topaz said:

I think the point is then that v.subgroup_basis.topology is not the right construction!

Indeed, this is what I had in mind: one should only take radii to be quotients of valuations of elements of the ring.

Adam Topaz said:

... or you could go via the route Valuation -> ValuativeRel -> SubgroupBasis

I think ultimately this is the way to go for the "defining the topology" part: we should have a way to endow the type with the unique topology compatible with a given valuative rel. But this is a different question of the API provided to study a docs#ValuativeTopology through a single appropriate valuation.

[Anatole Dedecker]

Kevin Buzzard said:

Anatole Dedecker said:

And again, I agree that doing the definitions in terms of the relation is cleaner. But in practice people may want to use their favorite valuation, no ?

What is your favourite $\R_{\geq0}$-valued valuation on $\mathbb{Q}_3(\sqrt{-1})$? There are two canonical ones. There is the one which sends an element to the amount that multiplication by it scales additive Haar measure (cf #25829) which is completely canonical, and then there is the one which is the unique nonarchimedean valuation which extends the standard 3-adic valuation on $\mathbb{Q}_3$; this is also completely canonical, and different; one is the square of the other, just like how the function sending a complex number to the amount it scales additive Haar measure is not the complex norm but its square. So Valued is a bit dangerous because maybe I want two different instances of Valued Q3i NNReal

This is actually a great example of my point. First, I am not advocating for docs#Valued, precisely because valuations are not canonical enough compared to docs#ValuativeRel. When I said "favorite valuation", I really meant "favorite in some context", and that is the point: say that $\mathbb{Q}_3(\sqrt{-1})$ is endowed with a valuative topology, and you want to know that balls for the Haar valuation are a basis of neighborhoods at zero. Ideally, you should just need a lemma saying that this valuation is compatible with the relation, and another saying that its image is dense around zero in $\mathbb{R}_{\geq 0}$, and then you'd be able to work with the topology using this valuation instead of the abstract docs#ValuativeRel.valuation. And likewise for your second choice of valuation. Does that make sense?

[Anatole Dedecker]

Yakov Pechersky said:

Antoine, does the phrasing of

(h : (𝓝 (0 : R)).HasBasis (fun rs : R × R ↦ rs.1 ∈ posSubmonoid R ∧ rs.2 ∈ posSubmonoid R)
      fun rs  ↦ { x | x * rs.2 <ᵥ rs.1 })

work for you?

Should we also state things using docs#TopologicalSpace.IsTopologicalBasis ?

I think Antoine was specifically referring to the "defining the topology through a docs#RingSubgroupsBasis" step. But indeed the HasBasis statement would be the most useful once the topology exists.

[Anatole Dedecker]

Adam Topaz said:

you could argue that $\mathbb{Q}_p$ has a preferred valuation, but I think in practice we would prove theorems about local fields of characteristic zero, instead of just that one example

This is the part where my whole argument may break down: I don't know precisely how any of this will be used. It just felt wrong to design the API around the abstractly defined docs#ValuativeRel.valuation only, because it would mean unnecessary boilerplate any time some other valuation would fit more naturally (e.g the one coming from the Haar measure if you're studying local fields, or a more specific one in the case of $\mathbb{Q}_p$ and Laurent Series). But if you tell me that this never happens then you can indeed ignore everything I've said.

[Adam Topaz]

I still don't really see what the issue is when you have some ring with a natural valuation. You can always define ValuativeRel using the canonical valuation, and include a Valuation.Compatible instance. As long as the API is developed generally enough using Valuation.Compatible, I don't see what issues would pop up?

[Anatole Dedecker]

Having the API developped generally enough using Valuation.Compatible is precisely my point, so I think we agree!

[Adam Topaz]

I see :) I thought that was implicitly understood!

[Anatole Dedecker]

Ah, maybe my initial message on this thread about Valued was giving the impression that I was advocating for Valued to stay, but this was really not my (main) point, and I'm okay with it disappearing.

What I've been saying is that, eventually, #26827's of_hasBasis (for example) should allow any compatible valuation instead of specifically ValuativeRel.valuation.

[Adam Topaz]

Ah I see. Yes, I do agree with that. Sorry I didn't look closely enough before.

[Adam Topaz]

Indeed making this of_hasBasis use an arbitrary compatible valuation would be strictly more general than the current version.

[Antoine Chambert-Loir]

Yakov Pechersky said:

Antoine, does the phrasing of

(h : (𝓝 (0 : R)).HasBasis (fun rs : R × R ↦ rs.1 ∈ posSubmonoid R ∧ rs.2 ∈ posSubmonoid R)
      fun rs  ↦ { x | x * rs.2 <ᵥ rs.1 })

work for you?

I'm not sure I can tell, in any direction. I had rewritten everything using the “SubgroupWithZero” defined by the valuation, the difficulty was not the math, but the avalanche of coercions required in the middle of the argument. I can't predict whether this will be cleaner, or not.

[Yakov Pechersky]

I think I've summarized the discussion above in the following theorems:

lemma of_hasBasis_compatible {Γ₀ : Type*} [LinearOrderedCommMonoidWithZero Γ₀] [TopologicalSpace R]
    {v : Valuation R Γ₀} [v.Compatible]
    (h : (𝓝 (0 : R)).HasBasis (fun rs : R × R ↦ v rs.1 ≠ 0 ∧ v rs.2 ≠ 0)
    fun rs : R × R ↦ { x | v x * v rs.2 < v rs.1 }) :
    ValuativeTopology R := sorry

lemma hasBasis_nhds_zero_compatible {Γ₀ : Type*} [LinearOrderedCommMonoidWithZero Γ₀]
    (v : Valuation R Γ₀) [v.Compatible] :
    (𝓝 (0 : R)).HasBasis (fun rs : R × R ↦ v rs.1 ≠ 0 ∧ v rs.2 ≠ 0)
      fun rs : R × R ↦ { x | v x * v rs.2 < v rs.1 } := sorry

[Yakov Pechersky]

Which is in #27163 (+105/-5): of and to basis of compatible valuations

[Yakov Pechersky]

The x * rs.2 <ᵥ rs.1 are in there as well

[Adam Topaz]

An easy one: #27167 (adds an unexpander for the relation notation)

[Yakov Pechersky]

#27177 (+57/-0): ValuativeRel ℚ_[p]. This is via Zm0, not via general normed field work in other PRs. Should be more direct and easier to review.

[Yakov Pechersky]

#27183 (+91/-1): IsRankLeOne when there is a compatible Zm0 or NNReal valuation

[Ruben Van de Velde]

Le or LE?

[Yakov Pechersky]

#27207 (+23/-0): ValuativeRel (WithVal v). Just the basics, no ValuativeTopology etc yet, waiting on other PRs for those.

[Anatole Dedecker]

Let me mention #27181 here: I had some fun playing with the definition of docs#ValuativeRel.ValueGroupWithZero to make it more conceptual and less ad-hoc:

• First, I define the equivalence relation associated to a valuative rel (I think this comes up often enough in the basic API to be justified) and the corresponding ValueQuotient. I show (by using some generic API) that this is always a docs#LinearOrderedCommMonoidWithZero, and that the quotient map is a valuation. I also show that it is a docs#LinearOrderedCommGroupWithZero when R is local with maximal ideal the support of the relation (and in particular a field).
• Then, I define the ValuativeRel on the localization of R with respect to any submonoid S of posSubmonoid R, and show that its support is the Ideal.map of the support of the original valuation.
• In particular, for S = posSubmonoid R, this localization is a local ring with maximal ideal the support of its valuation, so its ValueQuotient is a LinearOrderedCommGroupWithZero, and I take this as a definition of ValueGroupWithZero R.
• This means that we get all the structure on it by general arguments, but then I make sure that all the existing API matches (e.g all the induction stuff), but I'm not sure how much is really needed since we no longer need it to define e.g the order relation.

I should probably have discussed it here before, but I just had a sudden burst of motivation to start this and then wanted to finish it. I don't think we gain anything (we don't really care about the definition after all), but I think the intermediate steps are nice byproducts, which should be interesting in any case.

[Yakov Pechersky]

#27625 (+33/-0): discrete topology on a valued field when trivial valuation. Part of the preparation for ValuativeTopology refactor.

[Yakov Pechersky]

#27264 (+60/-0): range of valuation on competion is the same as base field. Also helper lemmas of Valued topology that use a v r * v x < v s style, which is what we'll need for ValuativeTopology.

[Yakov Pechersky]

#27172 (+169/-2): linearly ordered locally finite dense orders are trivial, now ready for review

[Aaron Liu]

I have a proof that in a dense locally finite order, no element is strictly less than another, and this proof is about 10 lines long and only imports Mathlib.Order.Interval.Finset.Basic. Would you be interested in taking a look?

[Aaron Liu]

@Yakov Pechersky Here it is

The whole thing

import Mathlib.Order.Interval.Finset.Basic

example {α : Type*} [Preorder α] [LocallyFiniteOrder α] [DenselyOrdered α] (a b : α) : ¬a < b := by
  intro hab
  induction hn : (Finset.Icc a b).card using Nat.strongRecOn generalizing b with
  | ind n ih =>
    subst hn
    obtain ⟨c, hac, hcb⟩ := exists_between hab
    refine ih (Finset.Icc a c).card ?_ c hac rfl
    apply Finset.card_lt_card
    apply (Finset.Icc_subset_Icc_right hcb.le).ssubset_of_ne
    apply ne_of_apply_ne (b ∈ ·)
    simp [hab.le, hcb.not_ge]

I never PR'd it because I didn't think it'd find a use.

[Aaron Liu]

you can combine what I have with docs#nontrivial_iff_lt to get that linear dense locally finite order are trivial pretty easily

[Yakov Pechersky]

Great! That proof could help golf LocallyFiniteOrder.denselyOrdered_iff_subsingleton. The rest of the PR is installing instances of DenselyOrdered on various other types.

[Yakov Pechersky]

The current proof basically does strong induction on the finset, I just fail every single time to remember how to invoke strong induction properly.

[Aaron Liu]

Congrats! You shaved a line:

import Mathlib.Order.Interval.Finset.Basic

def c {α : Type*} [Preorder α] [LocallyFiniteOrder α] [DenselyOrdered α] (a b : α) : ¬a < b := by
  intro hab
  induction hs : Finset.Icc a b using Finset.strongInduction generalizing b with
  -- chore: rename `H` to `ind`
  | H s ih =>
    subst hs
    obtain ⟨c, hac, hcb⟩ := exists_between hab
    refine ih (Finset.Icc a c) ?_ c hac rfl
    apply (Finset.Icc_subset_Icc_right hcb.le).ssubset_of_ne
    apply ne_of_apply_ne (b ∈ ·)
    simp [hab.le, hcb.not_ge]

[Yakov Pechersky]

The proof in the PR has been golfed using that.

[Yakov Pechersky]

#27312 (+54/-0): the trivial valuation, as One (Valuation R Γ₀)

[Yakov Pechersky]

#27313 (+182/-5): the trivial valuative relation, depends on the PR above. This is in a new ValuativeRel/Trivial.lean file -- I moved Valuation/ValuativeRel.lean to Valuation/ValuativeRel/Basic.lean.

[Yakov Pechersky]

this is in preparation for showing that the trivial relation, when ValuativeTopology, then DiscreteTopology, and the reverse. Which also then leads to a ValuativeRel on finite fields.

[Yakov Pechersky]

#27314: (+459/-111): the big kahuna. Refactoring Valued to use the {rs | v x * v rs.1 < v rs.2} topology. Prove that this is coarser than the previous topology. Migrate all uses of topology of Valued to rely on this. Do not yet assume ValuativeTopology, but still provide a ValuativeTopology => Valued helper instance (scoped). This is basically the largest (intermediate) step in the refactor. This relies on 3 upstream PRs.

[Yakov Pechersky]

Re-upping #27116 (+16/-6), which is [FaithfulSMul R K] => FaithfulSMul R (hat K)

[Yakov Pechersky]

Which leads to #27117 (+64/-6): IsDVR (K_v)