ValRingHom and ValAlgebra for valuations

Stream: maths

[Jiang Jiedong]

Hi everyone,

I am writing some definitions and theorems about lower-indexed ramification group. I find that I need to talk about the condition of "two valuations/valued instances are compatible with respect to a given ring map" again and again. More precisely, suppose we have

import Mathlib.RingTheory.DiscreteValuationRing.Basic
import Mathlib.Topology.Algebra.Valuation
import Mathlib.Algebra.Order.WithZero
import Mathlib.Algebra.Order.Group.TypeTags
import Mathlib.FieldTheory.Galois

open DiscreteValuation

variable {K L} [Field K] [Field L] [Algebra K L] [vK : Valued K ℤₘ₀] [vL : Valued L ℤₘ₀]
-- and some more instances

The condition of compatibility can be formalized as

variable (h : vK.v.IsEquiv (vL.v.comap (algebraMap K L)))

When I tried to introduce another intermediate field $E$ with valuations on E, soon the conditions get messy. Do you think introducing new structures/classes like ValRingHom, ValAlgebra, ValAlgHom a good idea?

For example,

structure ValRingHom (R S : Type*) {ΓR ΓS : outParam Type*} [Ring R] [Ring S]
  [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS]
  [vR : Valued R ΓR] [vS : Valued S ΓS] extends RingHom R S where
  val_isEquiv : vR.v.IsEquiv (vS.v.comap toRingHom)

infixr:25 " →+*v " => ValRingHom

This will make the statements of theorems concerning multiple ring maps compatible with valuations much shorter.

[Eric Wieser]

What would ValAlgebra look like?

[Kevin Buzzard]

IsValAlgebra is the prop saying that the valuations are compatible with the algebra map. Or perhaps compatible up to some equivalence...

[Kevin Buzzard]

There is more than one equivalence in play here though, e.g. the diagram commutes on the nose, or the diagram commutes up to multiplication by a positive integer (i.e. the valuation rings are the same)

[Adam Topaz]

Also what if you just so happen to consider the $p$-adic valuation on $$\Q$$ as a valuation taking values in $\R$ as opposed to $\Z$, then take a finite extension of $$\Q$$ and an extension of the $p$-adic valuation which just so happens to take values in $\Z$?

[Adam Topaz]

For fields this can all be handled if you just work with valuation subrings.

[Jiang Jiedong]

Eric Wieser said:

What would ValAlgebra look like?

Currently it looks like:

class ValAlgebra (R A : Type*) {ΓR ΓA : outParam Type*} [CommRing R] [Ring A]
  [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA]
  [vR : Valued R ΓR] [vA : Valued A ΓA] extends Algebra R A, ValRingHom R A

structure ValAlgHom (R A B : Type*) [CommRing R] [Ring A] [Ring B] {ΓR ΓA ΓB : outParam Type*}
  [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓA] [LinearOrderedCommGroupWithZero ΓB]
  [Valued R ΓR] [Valued A ΓA] [Valued B ΓB] [ValAlgebra R A] [ValAlgebra R B] extends AlgHom R A B, ValRingHom A B

notation:25 A " →ₐv[" R "] " B => ValAlgHom R A B

[Jiang Jiedong]

Adam Topaz said:

Also what if you just so happen to consider the $p$-adic valuation on $$\Q$$ as a valuation taking values in $\R$ as opposed to $\Z$, then take a finite extension of $$\Q$$ and an extension of the $p$-adic valuation which just so happens to take values in $\Z$?

This is exactly the case that this compatibility condition variable (h : vK.v.IsEquiv (vL.v.comap (algebraMap K L))) can deal with. In this case, the identity map would be an ValRingIso.

[Adam Topaz]

In any case, this seems like a very complicated way to say that the preorders induced by the valuations are compatible.

[Jiang Jiedong]

Kevin Buzzard said:

There is more than one equivalence in play here though, e.g. the diagram commutes on the nose, or the diagram commutes up to multiplication by a positive integer (i.e. the valuation rings are the same)

Yes, that is a big problem. The ValRingHom here has the weakest commutativity. It only requires IsEquiv. Currently if we require DiscreteValuation to be surjective valuation with range in ℤₘ₀, ValRingHom would be strong enough to fix the discrete valuation on L, given the discrete valuation on K, in the finite extension case. I don't know if there is other scenario that a stronger version of commutativity is inevitable.

[Adam Topaz]

This is true also in the higher rank discrete case.

[Antoine Chambert-Loir]

(I don't want to suggest a terrible mess, but one should probably try to take another route.
Up to now, math has two essentially disjoint frameworks for valued fields, the discrete valuation case, and the general valuation case. I say they are essentially disjoint because they are stated and taught in different books, often for different purposes.
Mathlib may wish to replicate this, may be forced to, but maybe there's a chance that the possibility of automation makes it possible that both things are framed in the same way.)

[Kevin Buzzard]

Adam Topaz said:

For fields this can all be handled if you just work with valuation subrings.

For general commutative rings this can all be handled just by asking that the map preserves the preorder induced by the valuation (which determines the valuation up to equivalence; this is the trick we used in the perfectoid project to prove that an affinoid adic space was a set ie didn't involve a universe bump)

[Jiang Jiedong]

Maybe a slightly better alternative way is that we define the Preorder R instance on Valued R and define ValRingHom extending RingHom, OrderHom, ContinuousMap (thus it can forget to OrderHom and ContinuousMap), then state the equivalence of valuation.

[Jiang Jiedong]

instance {R : Type*} {Γ : outParam Type*} [Ring R] [LinearOrderedCommGroupWithZero Γ] [Valued R Γ]: Preorder R := sorry

structure ValRingHom (R S : Type*) {ΓR ΓS : outParam Type*} [Ring R] [Ring S]
  [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS]
  [vR : Valued R ΓR] [vS : Valued S ΓS] extends OrderRingHom R S, ContinuousMap R S where
  val_isEquiv : vR.v.IsEquiv (vS.v.comap toOrderRingHom.toRingHom)

infixr:25 " →+*v " => ValRingHom

variable (R S : Type*) {ΓR ΓS : outParam Type*} [Ring R] [Ring S]
  [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS]
  [vR : Valued R ΓR] [vS : Valued S ΓS]
def ValRingHom.mk' (f : R →+* S) (hf : vR.v.IsEquiv (vS.v.comap f)) : R →+*v S := sorry

[Kevin Buzzard]

The sorry on the first line is just "pull back the preorder", is it docs#Preorder.comap or something like that? It's definitely there somewhere.

[Kevin Buzzard]

Aah there it is docs#Preorder.lift

[Jiang Jiedong]

Hi everyone,

After formalizing the basic parts of ValRingHom and ValAlgebra, I was trying to define a ValRingHom.mk' as below:

structure ValRingHom (R S : Type*) {ΓR ΓS : outParam Type*} [Ring R] [Ring S]
  [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS]
  [vR : Valued R ΓR] [vS : Valued S ΓS]
  extends OrderRingHom R S, ContinuousMap R S where
  /-- The proposition requiring the ring map preserves valuation. -/
  val_isEquiv_comap' : vR.v.IsEquiv (vS.v.comap toRingHom)

variable {R S : Type*} {ΓR ΓS : outParam Type*} [Ring R] [Ring S]
  [LinearOrderedCommGroupWithZero ΓR] [LinearOrderedCommGroupWithZero ΓS]
  [vR : Valued R ΓR] [vS : Valued S ΓS]

def ValRingHom.mk' {f : R →+* S} (hf : vR.v.IsEquiv (vS.v.comap f)) : R →+*v S := sorry

which reduces to the following proposition

theorem continuous_of_val_isEquiv_comap {f : R →+* S} (hf : vR.v.IsEquiv (vS.v.comap f)) :
  Continuous f := by sorry

To my surprise, this proposition does NOT hold at all. Consider the following counterexample:

Let $R = \mathbb{Q}[[x]], S = \mathbb{Q}[[x, y]]$ with inclusion map $f : R \to S$ sending $x$ to $x$. Let $v_R : R \to \mathbb{Z}\cup \{\infty\}$ be the usual discrete valuation on $R$ given by degree of the lowest term, that is

$$v_R ( a_n x^n + a_{n+1} x ^{n + 1} + \cdots) = n, \text{ if } a_i \in \mathbb{Q}, a_n \ne 0.$$

Let us equip $(\mathbb{Z} \oplus \mathbb{Z})\cup \{ \infty \}$ with the lexicographical order, then let $v_S : S \to \mathbb{Z} \oplus \mathbb{Z} \cup \{ \infty \}$ be the valuation that sends $x$ to $(0,1)$ and $y$ to $(1,0)$. More concretely,

$$v_S ( a_n(x) y^n + a_{n+1}(x) y ^{n + 1} + \cdots) = (n, m),$$

$\text{where each } a_i(x) \in R, a_n(x) \ne 0, \text{ and } m \text{ is the degree of lowest term in } a_n(x).$

Now this map $f$ indeed satisfies vR.v.IsEquiv (vS.v.comap f), however the map is not continuous when both ring is equipped with topology induced by their valuation. The image of $f$ in $S$ is equipped with the discrete topology, since $y S = \{ u \in S | v_S(u) \ge (1,0) \}$ is open in $S$ but $yS \cap f(R) = \{0\}$.

I have been thinking but still I cannot find an equivalent description of continuity that is purely stated in terms of valuation (or in terms of order induced by the valuation).

If you consider another valuation $v_S'$ that sends $x$ to $(1,0)$ and $y$ to $(0,1)$. More concretely,

$$v_S ( a_n(y) x^n + a_{n+1}(y) x ^{n + 1} + \cdots) = (n, m),$$

$\text{where each } a_i(y) \in \mathbb{Q}[[y]], a_n(y) \ne 0, \text{ and } m \text{ is the degree of lowest term in } a_n(y).$

Then everything is fine, $f(R)$ is homeomorphic to $R$. Both these two maps from $(R, v_R) \to (S, v_S)$ and $(R, v_R) \to (S, v_S')$ seems to me being what is called "extensions of valuation", but the first of them is not continuous, the second is continuous.

One possible remedy for continuity is that we require a "cofinality" condition of valuations on the top of val_isEquiv_comap, that is

$$\forall s \in S, \text{ s.t. } v_S(s) \ne 0, \text{ there exists some } r \in R, \text{ satisfying } v_R (r) \ne 0 \text{ and } v_S(f(r)) \ge v_S(s).$$

This is enough to force the map $f$ to be continuous. But this will certainly rule out the example $(R, v_R) \to (S, v_S)$ above.

Another possible but naive solution is to just give up the requirement of continuity.

Thank you for any suggestions or comments!

(Note that the cofinality condition above is automatically satisfied when $v_R, v_S$ is both rank $1$. So at least some good news is that this problem only occurs in higher rank cases (or lower, in trivial cases) )

[Antoine Chambert-Loir]

Most of the literature I know on valued fields says little about morphisms, and in his paper Continuous valuations (Math. Z., 1993), Huber restricts himself to adic rings and adic morphisms, for which continuity is imposed.
I would be wary of stating a general definition without a well established reference. Which one are you following?

[Jiang Jiedong]

Antoine Chambert-Loir said:

I would be wary of stating a general definition without a well established reference. Which one are you following?

You are right. Sorry that I was not cautious enough following a well-established reference. Originally I was just trying to formalize the definition of extension of valuations. (as the diagram in https://stacks.math.columbia.edu/tag/0ASG) Then I was trying to generalize to get rid of specific valued group using Valuation.IsEquiv without consulting a good reference.

[Antoine Chambert-Loir]

Mathlib seems to have only the very early definitions on valuation theory, it is really a good project to start formalizing the content of a book such as Engler/Prestel, Valued Fields, or Bourbaki's corresponding chapter.. I have no idea, though, how the current framework adopted by mathlib will be fit to that: as you noticed, the present definition immediately makes the link with topology, while the standard references more or less keep in distance of it, in particular because the Hensel lemma remains the anchor, while in higher rank, its validity is not implied by completeness. Consequently, I believe one has to be cautious and formalize those references from the very first pages on, as a check that mathlib's point of view will resist the rest of the book or the chapter.

[Jiang Jiedong]

Thank you for your advice and thank you for listing out the references! Now I see the importance of formalizing a good reference, especially when one need to test whether the current mathlib's point of view is in coordinate with mathematical conventions.

[Jiang Jiedong]

For the particular question concerning the definition of "extensions of valuations", I looked up for the corresponding part, Chap. 3 in Engler/Prestel's book Valued Field, and Chap. 6 Valuations, Section 3, Prop 5 in Bourbaki's Commutative Algebra.

In the book Valued Field, they define the extension of valuation on a valued field in terms of valuation subrings. They use the notation of $(K_1, \mathcal{O}_1) \subset (K_2, \mathcal{O}_2)$, where $\mathcal{O}_i$ is the valuation subring of $K_i$, meaning $\mathcal{O}_2 \cap K_1 = \mathcal{O}_1$. In the Bourbaki's book, they just state the proposition as "there exists a valuation on $v'$ on $K'$ whose restriction to $K$ is equivalent to $v$". This is the same as val_isEquiv_comap. These two definitions agree and include the example $(R, v_R) \to (S, v_S)$ (or at least $(\mathbb{Q}((x)), v_R) \to (\mathbb{Q}((x))((y)), v_S)$) earlier mentioned. It seems indeed that the continuity is not required when we talk about extension of valuations.