The ring of integers of a number field `K` is free of dimension `[K : ℚ]` / develop the theory of lattices

[riccardobrasca]

We are absolutely ready to prove this. For example the fact that 𝓞 K is free over ℤ is very easy

instance {K : Type*} [field K] [number_field K] : module.free ℤ (𝓞 K) :=
begin
  have basis : Σ n, basis (fin n) ℤ (𝓞 K) := module.free_of_finite_type_torsion_free',
  obtain ⟨n, b⟩ := basis,
  exact module.free.of_basis b
end

But the correct thing to do is to develop the theory of lattices, proving that a ℤ-basis gives also a ℚ-basis. Note that we have basis.localization, but this is the wrong statement, since it take a ℤ-basis of M and produces a ℚ-basis of M (in practice it only applies in trivial cases).

A sketch would be something like (of course one should not use tactic mode for the whole definition)

def foo {I K : Type*} [field K] [number_field K] (b : basis I ℤ (𝓞 K)) : basis I ℚ K :=
begin
  let b' : I → K := λ i, b i,
  have hb'li : linear_independent ℚ b',
  { rw [← linear_independent.iff_fraction_ring ℤ ℚ, linear_independent_iff'],
    intros s f H i hi,
    refine linear_independent_iff'.1 b.linear_independent s f ((𝓞 K).coe_eq_zero.1 _) i hi,
    convert H,
    simp only [zsmul_eq_mul, add_submonoid_class.coe_finset_sum, mul_mem_class.coe_mul,
      subring_class.coe_int_cast],
    apply_instance },
  refine basis.mk hb'li (λ x hx, _),
  obtain ⟨n, hn⟩ := (is_separable.is_integral ℚ x).exists_multiple_integral_of_is_localization
      (non_zero_divisors ℤ) x,
      sorry
end

See this comment for a nice application.

[Vierkantor]

I have the following result on my ideal-span-norm branch:

noncomputable def basis.localization_localization {R S : Type*} [comm_ring R] [comm_ring S]
  [algebra R S] {ι : Type*} [fintype ι] (b : basis ι R S)
  (M : submonoid R) (Rₘ Sₘ : Type*)
  [comm_ring Rₘ] [algebra R Rₘ] [comm_ring Sₘ] [algebra S Sₘ]
  [algebra Rₘ Sₘ] [algebra R Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ]
  [is_localization M Rₘ] [is_localization (M.map (algebra_map R S)) Sₘ]
  (hM : submonoid.map (algebra_map R S) M ≤ S ⁰) :
  basis ι Rₘ Sₘ :=

That is what we're looking for, right?

[riccardobrasca]

I have the following result on my ideal-span-norm branch:

noncomputable def basis.localization_localization {R S : Type*} [comm_ring R] [comm_ring S]
  [algebra R S] {ι : Type*} [fintype ι] (b : basis ι R S)
  (M : submonoid R) (Rₘ Sₘ : Type*)
  [comm_ring Rₘ] [algebra R Rₘ] [comm_ring Sₘ] [algebra S Sₘ]
  [algebra Rₘ Sₘ] [algebra R Sₘ] [is_scalar_tower R Rₘ Sₘ] [is_scalar_tower R S Sₘ]
  [is_localization M Rₘ] [is_localization (M.map (algebra_map R S)) Sₘ]
  (hM : submonoid.map (algebra_map R S) M ≤ S ⁰) :
  basis ι Rₘ Sₘ :=

That is what we're looking for, right?

Yes! This should replace basis.localization, whose assumptions essentially never apply (we take a ℤ-basis of a ℚ-vector space).

[Vierkantor]

I PR'd the result above in #18261.