feat(data/complex/is_R_or_C): generalize `is_R_or_C.proper_space_span…

…_singleton` to all finite dimensional submodules (#12877)

Also goes on to show that finite supremums of finite_dimensional submodules are finite-dimensional.

src/data/complex/is_R_or_C.lean

@@ -705,8 +705,9 @@ end
 
 variable {E}
 
-instance is_R_or_C.proper_space_span_singleton (x : E) : proper_space (K ∙ x) :=
-proper_is_R_or_C K (K ∙ x)
+instance is_R_or_C.proper_space_submodule (S : submodule K E) [finite_dimensional K ↥S] :
+  proper_space S :=
+proper_is_R_or_C K S
 
 end finite_dimensional
 

src/linear_algebra/finite_dimensional.lean

@@ -393,7 +393,12 @@ theorem span_of_finite {A : set V} (hA : set.finite A) :
 iff_fg.1 $ is_noetherian_span_of_finite K hA
 
 /-- The submodule generated by a single element is finite-dimensional. -/
-instance (x : V) : finite_dimensional K (K ∙ x) := by {apply span_of_finite, simp}
+instance span_singleton (x : V) : finite_dimensional K (K ∙ x) :=
+span_of_finite K $ set.finite_singleton _
+
+/-- The submodule generated by a finset is finite-dimensional. -/
+instance span_finset (s : finset V) : finite_dimensional K (span K (s : set V)) :=
+span_of_finite K $ s.finite_to_set
 
 /-- Pushforwards of finite-dimensional submodules are finite-dimensional. -/
 instance (f : V →ₗ[K] V₂) (p : submodule K V) [h : finite_dimensional K p] :
@@ -729,6 +734,41 @@ begin
   exact (fg_top _).2 (submodule.fg_sup ((fg_top S₁).1 h₁) ((fg_top S₂).1 h₂)),
 end
 
+/-- The submodule generated by a finite supremum of finite dimensional submodules is
+finite-dimensional.
+
+Note that strictly this only needs `∀ i ∈ s, finite_dimensional K (S i)`, but that doesn't
+work well with typeclass search. -/
+instance finite_dimensional_finset_sup {ι : Type*} (s : finset ι) (S : ι → submodule K V)
+  [Π i, finite_dimensional K (S i)] : finite_dimensional K (s.sup S : submodule K V) :=
+begin
+  refine @finset.sup_induction _ _ _ _ s S (λ i, finite_dimensional K ↥i)
+    (finite_dimensional_bot K V) _ (λ i hi, by apply_instance),
+  { introsI S₁ hS₁ S₂ hS₂,
+    exact submodule.finite_dimensional_sup S₁ S₂ },
+end
+
+/-- The submodule generated by a supremum of finite dimensional submodules, indexed by a finite
+type is finite-dimensional. -/
+instance finite_dimensional_supr {ι : Type*} [fintype ι] (S : ι → submodule K V)
+  [Π i, finite_dimensional K (S i)] : finite_dimensional K ↥(⨆ i, S i) :=
+begin
+  rw ←finset.sup_univ_eq_supr,
+  exact submodule.finite_dimensional_finset_sup _ _,
+end
+
+/-- The submodule generated by a supremum indexed by a proposition is finite-dimensional if
+the submodule is. -/
+instance finite_dimensional_supr_prop {P : Prop} (S : P → submodule K V)
+  [Π h, finite_dimensional K (S h)] : finite_dimensional K ↥(⨆ h, S h) :=
+begin
+  by_cases hp : P,
+  { rw supr_pos hp,
+    apply_instance },
+  { rw supr_neg hp,
+    apply_instance },
+end
+
 /-- In a finite-dimensional vector space, the dimensions of a submodule and of the corresponding
 quotient add up to the dimension of the space. -/
 theorem finrank_quotient_add_finrank [finite_dimensional K V] (s : submodule K V) :