finrank_eq_zero_of_basis_imp_not_finite

English

If every basis on every subset is infinite, then finrank_R(M) = 0.

Русский

Если база для любой подмножества бесконечна, то finrank_R(M) = 0.

LaTeX

$$$$ \forall s \subseteq M,\\ (\\\\text{Basis}(s, R, M) \\\\Rightarrow \\\\neg (s \\\\text{ finite})) \\\\Rightarrow \\\\operatorname{finrank}_R M = 0.$$$$

Lean4

theorem finrank_eq_zero_of_basis_imp_not_finite (h : ∀ s : Set M, Basis.{v} (s : Set M) R M → ¬s.Finite) :
    finrank R M = 0 := by
  cases subsingleton_or_nontrivial R
  · have := Module.subsingleton R M
    exact (h ∅ ⟨LinearEquiv.ofSubsingleton _ _⟩ Set.finite_empty).elim
  obtain ⟨_, ⟨b⟩⟩ := (Module.free_iff_set R M).mp ‹_›
  have := Set.Infinite.to_subtype (h _ b)
  exact b.linearIndependent.finrank_eq_zero_of_infinite

Похожие утверждения