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