From 53c79d561eec6b94be44bdaedeb2621361aa514f Mon Sep 17 00:00:00 2001
From: Haruhisa Enomoto <73296681+haruhisa-enomoto@users.noreply.github.com>
Date: Wed, 4 May 2022 11:10:46 +0000
Subject: [PATCH] feat(linear_algebra/span): add
 `finite_span_is_compact_element` (#13901)

This PR adds `finite_span_is_compact_element`, which extends `singleton_span_is_compact_element` to the spans of finite subsets.
This will be useful e.g. when proving the existence of a maximal submodule of a finitely generated module.
---
 src/linear_algebra/span.lean | 16 ++++++++++++++++
 1 file changed, 16 insertions(+)

diff --git a/src/linear_algebra/span.lean b/src/linear_algebra/span.lean
index b3e27235d2fb1..1b35892df4ab6 100644
--- a/src/linear_algebra/span.lean
+++ b/src/linear_algebra/span.lean
@@ -557,6 +557,22 @@ begin
   exact ⟨y, ⟨hyd, by simpa only [span_le, singleton_subset_iff]⟩⟩,
 end
 
+/-- The span of a finite subset is compact in the lattice of submodules. -/
+lemma finset_span_is_compact_element (S : finset M) :
+  complete_lattice.is_compact_element (span R S : submodule R M) :=
+begin
+  rw span_eq_supr_of_singleton_spans,
+  simp only [finset.mem_coe],
+  rw ←finset.sup_eq_supr,
+  exact complete_lattice.finset_sup_compact_of_compact S
+    (λ x _, singleton_span_is_compact_element x),
+end
+
+/-- The span of a finite subset is compact in the lattice of submodules. -/
+lemma finite_span_is_compact_element (S : set M) (h : S.finite) :
+  complete_lattice.is_compact_element (span R S : submodule R M) :=
+finite.coe_to_finset h ▸ (finset_span_is_compact_element h.to_finset)
+
 instance : is_compactly_generated (submodule R M) :=
 ⟨λ s, ⟨(λ x, span R {x}) '' s, ⟨λ t ht, begin
   rcases (set.mem_image _ _ _).1 ht with ⟨x, hx, rfl⟩,