English
Finitely generated submodules are precisely the compact elements of the submodule lattice.
Русский
Конечнопорожденные подпмодули являются точными компактными элементами решетки подпмодуля.
LaTeX
$$s.FG ↔ CompleteLattice.IsCompactElement s$$
Lean4
/-- Finitely generated submodules are precisely compact elements in the submodule lattice. -/
theorem fg_iff_compact (s : Submodule R M) : s.FG ↔ CompleteLattice.IsCompactElement s := by
classical
-- Introduce shorthand for span of an element
let sp : M → Submodule R M := fun a =>
span R
{ a }
-- Trivial rewrite lemma; a small hack since simp (only) & rw can't accomplish this smoothly.
have supr_rw : ∀ t : Finset M, ⨆ x ∈ t, sp x = ⨆ x ∈ (↑t : Set M), sp x := fun t => by rfl
constructor
· rintro ⟨t, rfl⟩
rw [span_eq_iSup_of_singleton_spans, ← supr_rw, ← Finset.sup_eq_iSup t sp]
apply CompleteLattice.isCompactElement_finsetSup
exact fun n _ => singleton_span_isCompactElement n
· intro h
have sSup' : s = sSup (sp '' ↑s) := by
rw [sSup_eq_iSup, iSup_image, ← span_eq_iSup_of_singleton_spans, eq_comm, span_eq]
-- by h, s is then below (and equal to) the sup of the spans of finitely many elements.
obtain ⟨u, ⟨huspan, husup⟩⟩ := h (sp '' ↑s) (le_of_eq sSup')
have ssup : s = u.sup id := by
suffices u.sup id ≤ s from le_antisymm husup this
rw [sSup', Finset.sup_id_eq_sSup]
exact sSup_le_sSup huspan
obtain ⟨t, -, rfl⟩ := Finset.subset_set_image_iff.mp huspan
rw [Finset.sup_image, Function.id_comp, Finset.sup_eq_iSup, supr_rw, ← span_eq_iSup_of_singleton_spans,
eq_comm] at ssup
exact ⟨t, ssup⟩
