isCompact_of_fg — Mathlib

English

If R is compact and N is finitely generated as an R-submodule of M, then N is compact in M.

Русский

Если R компактно, и N является конечно порожденным подмодулем M, то N компактно в M.

LaTeX

$$$\text{isCompact}(N) \text{ for } N \text{ FG submodule of } M$$$

Lean4

theorem isCompact_of_fg [CompactSpace R] {N : Submodule R M} (hN : N.FG) : IsCompact (X := M) N :=
  by
  obtain ⟨s, hs⟩ := hN
  have : LinearMap.range (Fintype.linearCombination R (α := s) Subtype.val) = N := by simp [hs]
  rw [← this]
  refine isCompact_range ?_
  simp only [Fintype.linearCombination, Finset.univ_eq_attach, LinearMap.coe_mk, AddHom.coe_mk]
  fun_prop

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