spanRank_finite_iff_fg — Mathlib

English

The spanRank of p is finite if and only if p is finitely generated.

Русский

spanRank p конечен тогда и только тогда, когда p конечнопорождено.

LaTeX

$$$p.spanRank < \aleph_0 \;\Leftrightarrow\; p.FG$$

Lean4

/-- A submodule's `spanRank` is finite if and only if it is finitely generated. -/
@[simp]
theorem spanRank_finite_iff_fg {p : Submodule R M} : p.spanRank < aleph0 ↔ p.FG :=
  by
  rw [spanRank, Submodule.fg_def]
  constructor
  · rintro h
    obtain ⟨s, hs⟩ :
      ⨅ (s : { s : Set M // span R s = p }), #s ∈ Set.range (fun (s : { s : Set M // span R s = p }) ↦ #s) :=
      csInf_mem ⟨#p, ⟨⟨p, by simp⟩, rfl⟩⟩
    refine ⟨s.1, ?_, s.2⟩
    simpa [← hs] using h
  · rintro ⟨s, hs₁, hs₂⟩
    exact (ciInf_le' _ ⟨s, hs₂⟩).trans_lt (by simpa)

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