Positive finrank doesn't imply finite

Stream: mathlib4

[Kevin Buzzard]

In the module docstring for docs#Module.finrank we have an example of a module that is not finitely-generated but has positive finrank, and it's $\Z\oplus(\mathbb{Q}/\Z)$. But it seems to me that $\mathbb{Q}$ works fine as a simpler example; I even checked it although it was pretty painful and I got stuck on a cardinal bound which I just asked about on #Is there code for X? > a cardinal <= 1 is 0 or 1

import Mathlib

open Cardinal

lemma aargh {c : Cardinal} (h1 : c ≤ 1) (h0 : c ≠ 0) : c = 1 :=
  sorry


example : Module.finrank ℤ ℚ = 1 := by
  rw [← Module.rank_eq_one_iff_finrank_eq_one]
  suffices Module.rank ℤ ℚ ≤ 1 ∧ Module.rank ℤ ℚ ≠ 0 by
    obtain ⟨h1, h0⟩ := this
    apply aargh h1 h0
  constructor
  · apply rank_le (R := ℤ) (M := ℚ) (n := 1)
    intro s hs
    by_contra! h
    rw [Finset.one_lt_card] at h
    obtain ⟨a, ha, b, hb, h⟩ := h
    obtain rfl | ha0 := eq_or_ne a 0
    · specialize @hs (Finsupp.single ⟨0, ha⟩ 1) 0
      simp at hs
    obtain rfl | hb0 := eq_or_ne b 0
    · specialize @hs (Finsupp.single ⟨0, hb⟩ 1) 0
      simp at hs
    have han : a.num ≠ 0 := Rat.num_ne_zero.mpr ha0
    have hbn : b.num ≠ 0 := Rat.num_ne_zero.mpr hb0
    have had : (a.den : ℤ) ≠ 0 := by norm_cast; exact a.den_nz
    have hbd : (b.den : ℤ) ≠ 0 := by norm_cast; exact b.den_nz
    -- clear denominators
    let D := a.den * b.den
    let A := a.num * b.den
    let B := a.den * b.num
    have hD0 : D ≠ 0 := by positivity
    have hA0 : A ≠ 0 := by positivity
    have hB0 : B ≠ 0 := by positivity
    have hA : a = A / D := by simp [A,D]; field_simp; rw [← mul_assoc, Rat.mul_den_eq_num]
    have hB : b = B / D := by simp [B,D]; field_simp; rw [mul_comm, mul_assoc, mul_comm _ b, Rat.mul_den_eq_num]
    specialize @hs (Finsupp.single ⟨a, ha⟩ B) (Finsupp.single ⟨b, hb⟩ A)
    simp [hA, hB] at hs
    have foo : (B : ℚ) * (A / D) = A * (B / D) := by field_simp; ring
    specialize hs foo
    rw [Finsupp.ext_iff] at hs
    specialize hs ⟨A / D, hA ▸ ha⟩
    simp at hs
    apply hB0
    rw [hs]
    apply Finsupp.single_eq_of_ne
    simpa [← hB, ← hA] using h.symm
  · intro h
    rw [rank_eq_zero_iff (R := ℤ) (M := ℚ)] at h
    obtain ⟨a, ha0, ha⟩ := h 1
    simp at ha
    contradiction

[Kevin Buzzard]

#24363

[Riccardo Brasca]

It's possible the definition was different at some moment. IIRC this has been written by @Andrew Yang

[Riccardo Brasca]

or maybe by me after andrew's comment

[Andrew Yang]

To me the reason why this phenomenon occurs is because of some infinitely generated torsion group, of which $\mathbb{Q}/\mathbb{Z}$ is a typical example. And as a extension of $\mathbb{Q}/\mathbb{Z}$ by $\mathbb{Z}$, $\Z\oplus(\mathbb{Q}/\Z)$ might be simpler than $\mathbb{Q}$ (but to be fair I could have just written $\mathbb{Q}/\mathbb{Z}$). That was the reasoning when I wrote the docstring, but I don't mind it being changed.

[Junyan Xu]

import Mathlib.LinearAlgebra.Dimension.Localization
import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition

example : Module.finrank ℤ ℚ = 1 :=
  (IsLocalizedModule.finrank_eq _ (Algebra.linearMap ℤ ℚ) le_rfl).trans (Module.finrank_self ℤ)

[Junyan Xu]

Of course, if Submodule.spanFinrank is nonzero then the module must be finite. It seems we don't have the counterpart for the behavior of Submodule.spanRank under localizations. The proof that Pic(UFD)=1 requires that the localization of a principal module is principal, and I wrote an initial draft for it at PKU when a student requested:

import Mathlib

variable {R A M N : Type*} [CommSemiring R] [AddCommMonoid M] [AddCommMonoid N] [Module R M]
  [Module R N] (S : Submonoid R) (f : M →ₗ[R] N) [IsLocalizedModule S f]
  [CommSemiring A] [Algebra R A] [IsLocalization S A] [Module A N] [IsScalarTower R A N]

example [Module.Finite R M] (n : N) (hn : Submodule.span A {n} = ⊤) :
    ∃ s : S, ∃ m : M, Submodule.span
      (Localization (.powers s.1)) {LocalizedModule.mkLinearMap (.powers s.1) M m} = ⊤ := by
  have ⟨⟨m, s⟩, eq⟩ := IsLocalizedModule.surj S f n
  have ⟨gen, hgen⟩ := Module.finite_def.mp ‹Module.Finite R M›
  have (g : gen) : ∃ r : R, ∃ s' : S, s' • f g = r • n := by
    sorry -- use IsLocalizedModule.surj
  have (g : gen) : ∃ r : R, ∃ s' : S, s' • g = r • m := by
    sorry -- use IsLocalizedModule.exists_iff_eq
  choose rgen sgen hrs using this
  let s := ∏ s : gen, sgen s
  let S' := Submonoid.powers s.1
  refine ⟨s, m, top_unique <| (span_eq_top_of_isLocalizedModule (Localization S') S'
    (LocalizedModule.mkLinearMap S' M) hgen).ge.trans <| Submodule.span_le.mpr ?_⟩