Rational basis of a number field

Stream: Is there code for X?

[Riccardo Brasca]

Let K be a number_field and suppose b : basis ι ℤ (𝓞 K). Do we have a way of obtaining the induced basis b' : basis ι ℚ K?

[Riccardo Brasca]

I mean, the basis morally is (coe : 𝓞 K → K) ∘ b.

[Johan Commelin]

I fear that we don't

[Riccardo Brasca]

I don't find anything like that. Let me see if I really need it or not.

[Kevin Buzzard]

The fact that O_K is a lattice in K is both obvious to us and also definitely needing of a proof. I guess you want that the canonical map O_K tensor Q to K is an isomorphism.

[Junyan Xu]

I guess you want that the canonical map O_K tensor Q to K is an isomorphism.

I think you would first prove that a basis maps to a basis (by coe) and then deduce that this is an isomorphism. I manage to prove the linear independence part of being a basis, but I had to introduce an instance (restriction of scalars, which would be cumbersome to inline); maybe we should state this in terms of an injective linear map of modules instead of a single module.

Interestingly, I thought I need T to be a submonoid of non_zero_divisors R, but I realized it's only needed in the reverse implication, just before I finished the proof.

import ring_theory.localization
import linear_algebra.linear_independent
open_locale classical

variables {ι : Type*} (R S : Type*)
  [comm_ring R] [comm_ring S] [algebra R S] (T : submonoid R)
  {M : Type*} (v : ι → M) [add_comm_monoid M] [module S M]

instance module_comp_hom : module R M := module.comp_hom M (algebra_map R S)

lemma map_linear_independent [is_localization T S]
  (hli : linear_independent R v) : linear_independent S v :=
begin
  rw linear_independent_iff at ⊢ hli, rintros ⟨s,g,hiff⟩ he0,
  let l' := finsupp.on_finset s (λ i, if hi : i ∈ s then
    is_localization.integer_multiple T s g ⟨i,hi⟩ else 0)
    (λ i, by { contrapose, intro h, simp [h] }),
  specialize hli l' _,
  convert smul_zero (is_localization.common_denom T s g),
  rw [← he0, finsupp.total_on_finset, finsupp.total_apply, finsupp.smul_sum],
  congr, ext i, split_ifs,
  { change algebra_map R S _ • _ = _, rw is_localization.map_integer_multiple,
    apply eq.trans _ (mul_smul _ _ _), rw ← algebra.smul_def, refl },
  { specialize hiff i, rw iff_not_comm at hiff, dsimp, rw hiff.2 h, simp },
  ext i, by_cases i ∈ s,
  { have := congr_arg (λ f : ι →₀ R, algebra_map R S (f i)) hli, simp [l', h] at this,
    refine (is_unit.mul_right_eq_zero _).1 ((algebra.smul_def _ _).symm.trans this),
    apply is_localization.map_units },
  { exact (iff_not_comm.1 (hiff i)).2 h },
end

[David Wärn]

Isn't there also an abstract argument where you don't assume $\mathcal O_K$ is free? If $A$ is any $\Z$-module and $B$ is a $\mathbb Q$-module, any (coe-semi-)-linear map $f : A \to B$ which is injective and whose range spans $B$ should be an 'extension of scalars' in the sense that $A \otimes_\Z \mathbb Q \to B \otimes_\Z \mathbb Q = B$ is an isomorphism, right? It's surjective because the range of $f$ spans $B$ and injective because $\mathbb Q$ is flat or something.

[Kevin Buzzard]

Yes this is what I was thinking of

[Kevin Buzzard]

You have to prove that for an algebraic number over Q there's some nonzero integer such that multiplying by this integer gives you an algebraic integer, and you do this by clearing the denominators in the min poly

[Anne Baanen]

Here's the iff version (which I thought I PR'd a while back, but apparently not!)

lemma linear_independent.of_fraction_ring (R K : Type*) [comm_ring R] [nontrivial R] [field K]
  [algebra R K] [is_fraction_ring R K] {ι V : Type*}
  [add_comm_group V] [module R V] [module K V] [is_scalar_tower R K V] {b : ι → V} :
  linear_independent R b ↔ linear_independent K b :=
begin
  refine ⟨_, linear_independent.restrict_scalars (smul_left_injective R one_ne_zero)⟩,
  rw [linear_independent_iff', linear_independent_iff'],
  intros hli s g hg i hi,
  choose a g' hg' using
    is_localization.exist_integer_multiples (non_zero_divisors R) s g,
  refine (smul_eq_zero.mp _).resolve_left (non_zero_divisors.coe_ne_zero a),
  rw [← hg' i hi, is_fraction_ring.to_map_eq_zero_iff],
  convert hli s (λ i, if hi : i ∈ s then g' i hi else 0) _ i hi,
  { rw dif_pos hi },
  { calc _ = (a : R) • ∑ i in s, g i • b i : _
       ... = 0 : by rw [hg, smul_zero],
    rw [finset.smul_sum, finset.sum_congr rfl],
    intros i hi,
    simp only [dif_pos hi, ← smul_assoc, ← hg' i hi, is_scalar_tower.algebra_map_smul] },
end

[Anne Baanen]

I used is_scalar_tower instead of module.comp_hom, this works better with the case that R = ℤ since you don't need to show that the module structure from comp_hom matches with the natural ℤ-module structure on any ring.

[Junyan Xu]

... and injective because Q is flat or something.

Yes linear independence is about the induced map from the free module being injective, and localizations are flat, so that's a natural way to view things. However ring_theory.flat is imported by exactly zero files... On the other hand the reverse implication only needs an injective ring hom, much less than faithful flatness (which is not even satisfied by fraction ring).

[Johan Commelin]

We're in dire need of a good API for flat.

[Johan Commelin]

But this in turn might need a good API for a characteristic predicate for tensor products.

[Matthew Ballard]

Johan Commelin said:

We're in dire need of a good API for flat.

Said every algebraic geometer at least once in their life.

[Kevin Buzzard]

I looked at a random source and it used Tor a lot so I was kind of waiting for Tor