Ring of integers is a free ℤ-module

Stream: Is there code for X?

[Xavier Roblot]

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

[Anne Baanen]

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

[Riccardo Brasca]

See this issue

[Riccardo Brasca]

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

[Xavier Roblot]

Great! Thanks

[Riccardo Brasca]

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]

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]

Let me try

[Riccardo Brasca]

You want the statement about the rank?

[Xavier Roblot]

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]

So something like

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

[Xavier Roblot]

Yes, that's what I need to prove.

[Riccardo Brasca]

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]

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]

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]

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]

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: