Zulip Chat Archive

Stream: Is there code for X?

Topic: Ring of integers is a free ℤ-module


Xavier Roblot (Jan 30 2023 at 15:57):

Do you have the fact that the ring of integers of a number field is a free ℤ-module ?

Anne Baanen (Jan 30 2023 at 16:00):

I definitely use it so it should be available in some form.

Riccardo Brasca (Jan 30 2023 at 16:00):

See this issue

Riccardo Brasca (Jan 30 2023 at 16:00):

The proof that is free is very easy, but now also the rank should be immediate, thank's to Anne's work.

Xavier Roblot (Jan 30 2023 at 16:02):

Great! Thanks

Riccardo Brasca (Jan 30 2023 at 16:04):

If you are going to PR something read our discussion about not restricting anything to 𝓞 K, but considering anything that satisfies is_integral_closure.

Xavier Roblot (Jan 31 2023 at 13:10):

So I had a look at how to use basis.localization_localization to get a ℚ-basis of K from a ℤ-basis of 𝓞 K and I think what is missing is the following lemma (or something similar):

example {A R B : Type*} [comm_ring R] [comm_semiring A] [comm_ring B] [algebra R B] [algebra A B]
[algebra R A] (h1 : is_integral_closure A R B)  {N : submonoid A} (h2 : is_localization N B) :
  is_localization (algebra.algebra_map_submonoid A (submonoid.comap (algebra_map R A) N)) B :=

I could not find this lemma or anything close in mathlib.

Am I right to think that this lemma is missing? Or maybe there is a simpler way to use basis.localization_localization that I haven't found

Riccardo Brasca (Jan 31 2023 at 13:25):

Let me try

Riccardo Brasca (Jan 31 2023 at 13:26):

You want the statement about the rank?

Xavier Roblot (Jan 31 2023 at 13:27):

Riccardo Brasca said:

You want the statement about the rank?

Yes, as you said, it is easy to get a ℤ-basis of 𝓞 K but the rank is more work

Riccardo Brasca (Jan 31 2023 at 13:30):

So something like

def foo : basis (free.choose_basis_index  K)  (𝓞 K) := sorry

Xavier Roblot (Jan 31 2023 at 13:33):

Yes, that's what I need to prove.

Riccardo Brasca (Jan 31 2023 at 14:27):

I went the other way, first getting a basis of 𝓞 K and then deducing a base of K over the same type.

import number_theory.number_field.basic
import linear_algebra.free_module.pid
import ring_theory.localization.module

open_locale number_field

open module algebra

variables {K : Type*} [field K] [number_field K]

instance : free  (𝓞 K) :=
begin
  have basis : Σ n, basis (fin n)  (𝓞 K) := free_of_finite_type_torsion_free',
  obtain n, b := basis,
  exact free.of_basis b
end

instance foo : is_localization (algebra.algebra_map_submonoid (𝓞 K) (non_zero_divisors )) K :=
begin
  refine _, λ z, _, λ x y, λ h, 1, _⟩, _⟩⟩,
  { rintro y, hy⟩,
    simp only [subalgebra.algebra_map_eq, is_unit_iff_ne_zero, id.map_eq_id,
      ring_hom_comp_triple.comp_eq, set_like.coe_mk, alg_hom.coe_to_ring_hom, subalgebra.coe_val,
      ne.def],
    intro h0,
    simpa [(subalgebra.coe_eq_zero _).1 h0, algebra_map_submonoid,
      mem_non_zero_divisors_iff_ne_zero] using hy },
  { obtain ⟨⟨m, mzdiv⟩, hm := is_integral.exists_multiple_integral_of_is_localization
      (non_zero_divisors ) z (is_separable.is_integral  z),
    refine ⟨⟨⟨_, hm⟩, m, m, mzdiv, by simp⟩⟩⟩⟩, _⟩,
    simp [subalgebra.algebra_map_eq, submonoid.smul_def, mul_comm] },
  { simp [is_fraction_ring.injective (𝓞 K) K h] },
  { rintro ⟨⟨m, mzdiv⟩, hm⟩,
    suffices : m  0,
    { congr,
      simpa [this] using hm },
    intro h0,
    rw [h0] at mzdiv,
    simpa [algebra_map_submonoid, mem_non_zero_divisors_iff_ne_zero] using mzdiv }
end

noncomputable def bar : basis (free.choose_basis_index  (𝓞 K))  K :=
(free.choose_basis  (𝓞 K)).localization_localization  (non_zero_divisors ) K
begin
  intros x hx,
  refine mem_non_zero_divisors_iff_ne_zero.2 (λ h, _),
  rw [h] at hx,
  simpa [algebra_map_submonoid, mem_non_zero_divisors_iff_ne_zero] using hx,
end

Riccardo Brasca (Jan 31 2023 at 14:27):

Note that I didn't really try to optimize the proof of foo, I just used the definition of is_localization. It's very possible that some of the fields follow by something else.

Riccardo Brasca (Jan 31 2023 at 14:31):

Mathematically the only nontrivial fact is that given an algebraic number x there is an integer n such that n * x is an algebraic integer, and this is docs#is_integral.exists_multiple_integral_of_is_localization

Xavier Roblot (Jan 31 2023 at 14:33):

Thanks! That's great, I was following the same way but I was much much slower :wink:

I need this result to prove that the lattice given by the canonical embedding of the ring of integers is a full lattice.

Riccardo Brasca (Jan 31 2023 at 14:38):

It's funny because the horrible line refine ⟨⟨⟨_, hm⟩, ⟨m, ⟨m, ⟨mzdiv, by simp⟩⟩⟩⟩, _⟩, is motivated by the fact that intuitively the only thing we need is docs#is_integral.exists_multiple_integral_of_is_localization, and then I just wrote the only thing that typechecks and uses m. I honestly don't know what I am doing there :sweat_smile:


Last updated: Dec 20 2023 at 11:08 UTC