Intersection of localisations

Stream: Is there code for X?

[David Ang]

Do we have (or is it easy to prove given what we have) that the ring of integers of a number field is the intersection of all its local valuation rings? I think somewhere in the proof we need something like an integral domain is an intersection of its localisations at all primes?

[Johan Commelin]

I'm quite sure we do not have this yet. But we seem to have most of the ingredients.

[Filippo A. E. Nuccio]

I think that using docs#is_dedekind_domain.height_one_spectrum.int_valuation_def this should be very easy. Given r/s in the field of fractions K, you can use docs#is_dedekind_domain.height_one_spectrum.valuation_of_mk' to compute all its valuations and deduce that the s is a unit.

[Kevin Buzzard]

s isn't a well-defined thing so I'm not sure it's as easy as that (there's no notion of "lowest terms" in general). Given an element k in the field of fractions of an integral domain you can construct the ideal of denominators of that element, which is all the elements r of the ring such that r*k is in the ring. It's not principal in general.

[Filippo A. E. Nuccio]

But there is a docs#is_dedekind_domain.height_one_spectrum.int_valuation_div_eq_div so I think any choice would work.

[Filippo A. E. Nuccio]

(ops, link broken, I'll fix: it says it is indep. of the choices of s and r)

[Filippo A. E. Nuccio]

Oh no, I see the problem. I agree with @Kevin Buzzard .

[Adam Topaz]

The general assertion is that the integral closure of a domain in a field is the intersection of all valuation rings of the field field with a centre on your given domain.

[Adam Topaz]

You can probably find a proof in Zariski-Samuel

[Adam Topaz]

I don’t think mathlib even knows that valuation rings are normal!

[Adam Topaz]

That should be a quick PR.

[Junyan Xu]

There is another general statement and the first answer seems pretty easy to formalize (we do have docs#submodule.colon). But I suspect what @David Ang actually want is something like this:

import ring_theory.dedekind_domain.adic_valuation
open is_dedekind_domain
variables {R : Type*} [comm_ring R] [is_domain R] [is_dedekind_domain R]
variables {K : Type*} [field K] [algebra R K] [is_fraction_ring R K]

theorem height_one_spectrum.valuation_le_one' (x : K)
  (h : ∀ v : height_one_spectrum R, v.valuation x ≤ 1) : x ∈ (algebra_map R K).range := sorry
-- could also use is_localization.is_integer in statement --

My outline for proving this is to show if we write x = r/s, then the multiset of normalized factors of the ideal (s) is less than or equal to the multiset of normalized factors of (r) using the condition h. (The definition of docs#is_dedekind_domain.height_one_spectrum.valuation uses counts of factors of associate.mk, so there will need some glue.) Then you may write the latter multiset as the former multiset plus some other multiset, multiply up the multisets and use docs#prod_normalized_factors_eq_self to get that (r)=(s)I for some ideal I, so r is s times some element in the ideal; then x=r/s equals that element.
In fact I wrote down a more general statement a while ago but haven't got around to prove it:

lemma localization_subalgebra_eq_integer (M : submonoid R) (hM : M ≤ non_zero_divisors R) :
  localization.subalgebra.of_field K M hM =
  {v : height_one_spectrum R | ∃ m ∈ M, m ∈ v.as_ideal}.integer K := sorry

[David Ang]

Junyan Xu said:

There is another general statement and the first answer seems pretty easy to formalize (we do have docs#submodule.colon). But I suspect what David Ang actually want is something like this:

import ring_theory.dedekind_domain.adic_valuation
open is_dedekind_domain
variables {R : Type*} [comm_ring R] [is_domain R] [is_dedekind_domain R]
variables {K : Type*} [field K] [algebra R K] [is_fraction_ring R K]

theorem height_one_spectrum.valuation_le_one' (x : K)
  (h : ∀ v : height_one_spectrum R, v.valuation x ≤ 1) : x ∈ (algebra_map R K).range := sorry
-- could also use is_localization.is_integer in statement --

My outline for proving this is to show if we write x = r/s, then the multiset of normalized factors of the ideal (s) is less than or equal to the multiset of normalized factors of (r) using the condition h. (The definition of docs#is_dedekind_domain.height_one_spectrum.valuation uses counts of factors of associate.mk, so there will need some glue.) Then you may write the latter multiset as the former multiset plus some other multiset, multiply up the multisets and use docs#prod_normalized_factors_eq_self to get that (r)=(s)I for some ideal I, so r is s times some element in the ideal; then x=r/s equals that element.
In fact I wrote down a more general statement a while ago but haven't got around to prove it:

lemma localization_subalgebra_eq_integer (M : submonoid R) (hM : M ≤ non_zero_divisors R) :
  localization.subalgebra.of_field K M hM =
  {v : height_one_spectrum R | ∃ m ∈ M, m ∈ v.as_ideal}.integer K := sorry

I currently only have a proof of the statement you linked:

lemma maximal_spectrum.localization_infi_eq_bot :
    (⨅ v : {I : ideal R // I.is_maximal}, localization.subalgebra.of_field K
      (@ideal.prime_compl _ _ _ v.property.is_prime) $ le_non_zero_divisors_of_no_zero_divisors $
      not_not_intro v.val.zero_mem) = ⊥ := ...

I also have the prime_spectrum and height_one_spectrum versions that follow pretty much immediately.

[David Ang]

But yes, I also think that what I want is what you wrote after this.

[Adam Topaz]

Adam Topaz said:

That should be a quick PR.

scratch that, we have docs#valuation_ring.is_bezout

[Adam Topaz]

and docs#is_bezout.is_integrally_closed

[Kevin Buzzard]

Junyan Xu said:

There is another general statement

Right -- this is the ideal of denominators proof that I was hinting at earlier.

[Junyan Xu]

Just completed a proof of mem_integers_of_valuation_le_one!

import ring_theory.dedekind_domain.S_integer

namespace is_dedekind_domain

open unique_factorization_monoid height_one_spectrum

variables {R : Type*} [comm_ring R] [is_domain R] [is_dedekind_domain R]
variables {K : Type*} [field K] [algebra R K] [is_fraction_ring R K]

theorem height_one_spectrum.mem_integers_of_valuation_le_one (x : K)
  (h : ∀ v : height_one_spectrum R, v.valuation x ≤ 1) : x ∈ (algebra_map R K).range :=
begin
  obtain ⟨x, ⟨y, hy⟩, rfl⟩ := is_localization.mk'_surjective (non_zero_divisors R) x,
  obtain rfl | hx := eq_or_ne x 0,
  { rw is_localization.mk'_zero, apply subring.zero_mem },
  suffices : ideal.span {y} ∣ (ideal.span {x} : ideal R),
  { obtain ⟨z, rfl⟩ := ideal.span_singleton_le_span_singleton.1 (ideal.le_of_dvd this),
    use z, rw [is_localization.eq_mk'_iff_mul_eq, map_mul, mul_comm], refl },
  classical,
  rw [← associates.mk_le_mk_iff_dvd_iff, ← associates.factors_le],
  have hy' := non_zero_divisors.ne_zero hy,
  have ine := λ {r : R}, mt (@ideal.span_singleton_eq_bot R _ r).1,
  rw [associates.factors_mk _ (ine hx), associates.factors_mk _ (ine hy')],
  rw [with_top.coe_le_coe, multiset.le_iff_count],
  { rintro ⟨v, hv⟩, obtain ⟨v, rfl⟩ := associates.mk_surjective v,
    have hv' := hv, rw [associates.irreducible_mk, irreducible_iff_prime] at hv,
    specialize h ⟨v, ideal.is_prime_of_prime hv, hv.ne_zero⟩,
    rw [valuation_of_mk', int_valuation, ← valuation.to_fun_eq_coe] at h,
    dsimp only [subtype.coe_mk] at h,
    rw [int_valuation_def_if_neg _ hx, int_valuation_def_if_neg _ hy'] at h,
    rw [← with_zero.coe_div, ← with_zero.coe_one, with_zero.coe_le_coe,
      ← of_add_sub, ← of_add_zero] at h,
    replace h := @le_of_sub_nonpos ℤ _ _ _ _ _ h,
    rw [neg_le_neg_iff, int.coe_nat_le] at h,
    rw [associates.factors_mk _ (ine hx), associates.factors_mk _ (ine hy'), option.coe_def ] at h,
    simp_rw associates.count_some hv' at h, exact h },
end

end is_dedekind_domain

[David Ang]

David Ang said:

Junyan Xu said:

There is another general statement and the first answer seems pretty easy to formalize (we do have docs#submodule.colon). But I suspect what David Ang actually want is something like this:

import ring_theory.dedekind_domain.adic_valuation
open is_dedekind_domain
variables {R : Type*} [comm_ring R] [is_domain R] [is_dedekind_domain R]
variables {K : Type*} [field K] [algebra R K] [is_fraction_ring R K]

theorem height_one_spectrum.valuation_le_one' (x : K)
  (h : ∀ v : height_one_spectrum R, v.valuation x ≤ 1) : x ∈ (algebra_map R K).range := sorry
-- could also use is_localization.is_integer in statement --

My outline for proving this is to show if we write x = r/s, then the multiset of normalized factors of the ideal (s) is less than or equal to the multiset of normalized factors of (r) using the condition h. (The definition of docs#is_dedekind_domain.height_one_spectrum.valuation uses counts of factors of associate.mk, so there will need some glue.) Then you may write the latter multiset as the former multiset plus some other multiset, multiply up the multisets and use docs#prod_normalized_factors_eq_self to get that (r)=(s)I for some ideal I, so r is s times some element in the ideal; then x=r/s equals that element.
In fact I wrote down a more general statement a while ago but haven't got around to prove it:

lemma localization_subalgebra_eq_integer (M : submonoid R) (hM : M ≤ non_zero_divisors R) :
  localization.subalgebra.of_field K M hM =
  {v : height_one_spectrum R | ∃ m ∈ M, m ∈ v.as_ideal}.integer K := sorry

I currently only have a proof of the statement you linked:

lemma maximal_spectrum.localization_infi_eq_bot :
    (⨅ v : {I : ideal R // I.is_maximal}, localization.subalgebra.of_field K
      (@ideal.prime_compl _ _ _ v.property.is_prime) $ le_non_zero_divisors_of_no_zero_divisors $
      not_not_intro v.val.zero_mem) = ⊥ := ...

I also have the prime_spectrum and height_one_spectrum versions that follow pretty much immediately.

Here is the preliminary PR for this: https://github.com/leanprover-community/mathlib/pull/16860

[David Ang]

@Junyan Xu I don't think the result on localisations (the one I just proved :/) will be all that useful for the result I actually want (the one you have!), so perhaps they should be separate PRs?

[David Ang]

Actually, was there a discussion before on whether maximal_spectrum is a good thing to have, instead of just using prime_spectrum or height_one_spectrum?

[Junyan Xu]

Yeah I think they should be separate PRs. In order to use your work, we need that for every maximal ideal p, localization at p gives exactly the {p}ᶜ-integers; the ⊆ direction seems nontrivial and likely requires a proof like mine above. I think I'd better extract some lemmas and add some related results like localization_subalgebra_eq_integer before PR'ing my proof above.

[Junyan Xu]

I think it would make things easier if we redefine docs#is_dedekind_domain.height_one_spectrum.int_valuation_def in terms of docs#unique_factorization_monoid.normalized_factors instead of docs#associates.factors. Since we have docs#ideal.normalization_monoid there is no need to pass to normalized_factors. In fact, I propose to generalize docs#associates.factors and docs#associates.factors' to arbitrary docs#normalization_monoid, and since docs#associates always form a normalization_monoid (which is already known to Lean via docs#normalization_monoid_of_unique_units and docs#associates.unique_units), they can always be specialized to the associates monoid. associates.factors is easier to work with than normalized_factors because the former is a multiset of irreducible elements, so when you apply e.g. docs#multiset.le_iff_count you don't have to deal with the counts of reducible elements which are zero. If anyone would like to take up this that would be great.

BTW, docs#is_dedekind_domain.height_one_spectrum.int_valuation is missing a @[simps] attribute or a lemma to simplify it to int_valuation_def.

[Junyan Xu]

Regarding maximal_spectrum, I think it's harmless to add it as a definition, and it could potentially be used elsewhere, e.g. in these notes on non-archimedean geometry it's denoted MaxSpec or M(A) and used throughout. @Jireh Loreaux is working on some C*-algebra stuff and there are likely some parallels with the non-archimedean Banach algebras (complete docs#normed_algebra) studied in the notes.

I don't know whether we want to put the Zariski topology on it now, as it may not be predominantly the topology we want on the set as is the case for prime_spectrum. It's interesting to note that in the context of #16719, although the Zariski topology (whose closed sets are generated by zero loci of functions) is ostensibly coarser than the weak topology on docs#weak_dual.character_space, they are actually the same, because any compact t2_space is completely regular (cf. link 1, link 2).

[Jireh Loreaux]

In case my input matters at all: I have no issue with adding maximal_spectrum. We won't use it directly for the C⋆-algebra work I'm currently doing because we will also be concerned (eventually) with the non-unital case, so the character space is the way to go. However, I will probably add an equiv for convenience. You're welcome to put the Zariski topology on it. Some authors just use the maximal ideal space and the Zariski topology directly instead of (or in addition to) the character space.

[Junyan Xu]

In fact mem_integers_of_valuation_le_one is the second defining property of a Krull ring, which are higher dimensional generalization of Dedekind domains.