English
If the OreSet of nonZeroDivisors in R is empty, then the rank of R over itself is at least aleph_0 (infinite).
Русский
Пусть OreSet из ненулевых делителей пуст; тогда ранг R по модулю R не меньшеaleph_0 (бесконечный).
LaTeX
$$$\aleph_0 \le \operatorname{Module.rank} R R$$$
Lean4
/-- A domain that is not (left) Ore is of infinite rank.
See [cohn_1995] Proposition 1.3.6 -/
theorem aleph0_le_rank_of_isEmpty_oreSet (hS : IsEmpty (OreLocalization.OreSet R⁰)) : ℵ₀ ≤ Module.rank R R := by
classical
rw [← not_nonempty_iff, OreLocalization.nonempty_oreSet_iff_of_noZeroDivisors] at hS
push_neg at hS
obtain ⟨r, s, h⟩ := hS
refine Cardinal.aleph0_le.mpr fun n ↦ ?_
suffices LinearIndependent R (fun (i : Fin n) ↦ r * s ^ (i : ℕ)) by simpa using this.cardinal_lift_le_rank
suffices ∀ (g : ℕ → R) (x), (∑ i ∈ Finset.range n, g i • (r * s ^ (i + x))) = 0 → ∀ i < n, g i = 0
by
refine Fintype.linearIndependent_iff.mpr fun g hg i ↦ ?_
simpa only [dif_pos i.prop] using
this (fun i ↦ if h : i < n then g ⟨i, h⟩ else 0) 0 (by simp [← Fin.sum_univ_eq_sum_range, ← hg]) i i.prop
intro g x hg i hin
induction n generalizing g x i with
| zero => exact (hin.not_ge (zero_le i)).elim
| succ n IH =>
rw [Finset.sum_range_succ'] at hg
by_cases hg0 : g 0 = 0
· simp only [hg0, zero_smul, add_zero, add_assoc] at hg
cases i; exacts [hg0, IH _ _ hg _ (Nat.succ_lt_succ_iff.mp hin)]
simp only [zero_add, pow_add _ _ x, ← mul_assoc, pow_succ, ← Finset.sum_mul, smul_eq_mul] at hg
rw [← neg_eq_iff_add_eq_zero, ← neg_mul, ← neg_mul] at hg
have := mul_right_cancel₀ (mem_nonZeroDivisors_iff_ne_zero.mp (s ^ x).prop) hg
exact (h _ ⟨(g 0), mem_nonZeroDivisors_iff_ne_zero.mpr (by simpa)⟩ this.symm).elim
