Some more about valuation rings

Stream: maths

[Adam Topaz]

I just opened another WIP/RFC PR about valuation rings: #13429

This PR shows that for a valuation ring $\mathcal{O}$ of a field $K$, the collection of coarsesnings of $\mathcal{O}$ (i.e. the subrings of $K$ containing $\mathcal{O}$, all of which are again valuation rings) are in (ordered) bijection with the prime ideals of $\mathcal{O}$.

There is still some cleanup to do before this is ready for consumption, but any comments would be much appreciated!

[Junyan Xu]

Interesting result and nice work! I went through half of valuation_subring.lean and golfed some proofs; this is for today and I may continue later.

[Adam Topaz]

Thanks @Junyan Xu ! Feel free to push these to my branch!

[Junyan Xu]

Just observed: we can define

def ideal_of_le (R S : valuation_subring K) (h : R ≤ S) : ideal R :=
(local_ring.maximal_ideal S).comap (R.inclusion S h)

then it's automatically prime.
If we prefer defeq property of the original definition we may use docs#submodule.copy.

[Adam Topaz]

Sure, we could do that, but, in my experience, proving that the ideal was prime was not that hard. I don't know how much this would help.

[Junyan Xu]

I'll check in the evening if it helps.
I also wonder whether APIs around docs#subring.closure simplifies localization.subring.
Only the last instance in as_subring.lean requires is_fraction_ring although some the first lemma and the is_localization instance requires injectivity, but I'm not sure if that's a good generalization to make.

[Adam Topaz]

For the purposes of the stuff involving valuations, it's useful to have the set underlying this subring localization to be as defined, as one can then easily get inequalities of the form $v(x) \le v(y)$ for elements in such a localization. If we defined it using subring.closure, it would require some additional work to get such inequalities.

[Junyan Xu]

The new definition of ideal_of_le seems working fine, and simplifies proofs, especially ideal_of_le_of_prime. I'll push to your branch once you confirm this definitional change.
I haven't looked as deeply into as_subring.lean, but yes using subring.closure as definition probably doesn't help much, since to show every element in the closure can be written as a quotient you probably need to show the quotients form a subring first.