feat(linear_algebra/*): add lemma `linear_independent.finite_of_is_no…

…etherian` (#14714)

This replaces `fintype_of_is_noetherian_linear_independent` which gave the same
conclusion except demanded `strong_rank_condition R` instead of just `nontrivial R`.

Also some other minor gaps filled.

src/algebra/module/torsion.lean

@@ -60,14 +60,62 @@ Torsion, submodule, module, quotient
 
 namespace ideal
 
-section
+section torsion_of
+
 variables (R M : Type*) [semiring R] [add_comm_monoid M] [module R M]
+
 /--The torsion ideal of `x`, containing all `a` such that `a • x = 0`.-/
 @[simps] def torsion_of (x : M) : ideal R := (linear_map.to_span_singleton R M x).ker
+
+@[simp] lemma torsion_of_zero : torsion_of R M (0 : M) = ⊤ := by simp [torsion_of]
+
 variables {R M}
+
 @[simp] lemma mem_torsion_of_iff (x : M) (a : R) : a ∈ torsion_of R M x ↔ a • x = 0 := iff.rfl
+
+variables (R)
+
+@[simp] lemma torsion_of_eq_top_iff (m : M) : torsion_of R M m = ⊤ ↔ m = 0 :=
+begin
+  refine ⟨λ h, _, λ h, by simp [h]⟩,
+  rw [← one_smul R m, ← mem_torsion_of_iff m (1 : R), h],
+  exact submodule.mem_top,
+end
+
+@[simp] lemma torsion_of_eq_bot_iff_of_no_zero_smul_divisors
+  [nontrivial R] [no_zero_smul_divisors R M] (m : M) :
+  torsion_of R M m = ⊥ ↔ m ≠ 0 :=
+begin
+  refine ⟨λ h contra, _, λ h, (submodule.eq_bot_iff _).mpr $ λ r hr, _⟩,
+  { rw [contra, torsion_of_zero] at h,
+    exact bot_ne_top.symm h, },
+  { rw [mem_torsion_of_iff, smul_eq_zero] at hr,
+    tauto, },
 end
 
+/-- See also `complete_lattice.independent.linear_independent` which provides the same conclusion
+but requires the stronger hypothesis `no_zero_smul_divisors R M`. -/
+lemma complete_lattice.independent.linear_independent' {ι R M : Type*} {v : ι → M}
+  [ring R] [add_comm_group M] [module R M]
+  (hv : complete_lattice.independent $ λ i, (R ∙ v i))
+  (h_ne_zero : ∀ i, ideal.torsion_of R M (v i) = ⊥) :
+  linear_independent R v :=
+begin
+  refine linear_independent_iff_not_smul_mem_span.mpr (λ i r hi, _),
+  replace hv := complete_lattice.independent_def.mp hv i,
+  simp only [supr_subtype', ← submodule.span_range_eq_supr, disjoint_iff] at hv,
+  have : r • v i ∈ ⊥,
+  { rw [← hv, submodule.mem_inf],
+    refine ⟨submodule.mem_span_singleton.mpr ⟨r, rfl⟩, _⟩,
+    convert hi,
+    ext,
+    simp, },
+  rw [← submodule.mem_bot R, ← h_ne_zero i],
+  simpa using this,
+end
+
+end torsion_of
+
 section
 variables (R M : Type*) [ring R] [add_comm_group M] [module R M]
 /--The span of `x` in `M` is isomorphic to `R` quotiented by the torsion ideal of `x`.-/

src/analysis/box_integral/partition/measure.lean

@@ -55,7 +55,7 @@ end
 lemma measurable_set_Icc : measurable_set I.Icc := measurable_set_Icc
 
 lemma measurable_set_Ioo : measurable_set I.Ioo :=
-(measurable_set_pi (finite.of_fintype _).countable).2 $ or.inl $ λ i hi, measurable_set_Ioo
+(measurable_set_pi (set.finite.of_fintype _).countable).2 $ or.inl $ λ i hi, measurable_set_Ioo
 
 lemma coe_ae_eq_Icc : (I : set (ι → ℝ)) =ᵐ[volume] I.Icc :=
 by { rw coe_eq_pi, exact measure.univ_pi_Ioc_ae_eq_Icc }

src/data/finite/set.lean

@@ -159,3 +159,10 @@ set.finite_univ_iff.mp ‹_›
 lemma finite.set.finite_of_finite_image (s : set α)
   {f : α → β} (h : s.inj_on f) [finite (f '' s)] : finite s :=
 finite.of_equiv _ (equiv.of_bijective _ h.bij_on_image.bijective).symm
+
+lemma finite.of_injective_finite_range {f : α → β}
+  (hf : function.injective f) [finite (range f)] : finite α :=
+begin
+  refine finite.of_injective (set.range_factorization f) (λ x y h, hf _),
+  simpa only [range_factorization_coe] using congr_arg (coe : range f → β) h,
+end

src/linear_algebra/affine_space/finite_dimensional.lean

@@ -75,7 +75,7 @@ begin
   let q := (not_is_empty_iff.mp hι).some,
   rw affine_independent_iff_linear_independent_vsub k p q at hi,
   letI : is_noetherian k V := is_noetherian.iff_fg.2 infer_instance,
-  exact fintype_of_fintype_ne _ (fintype_of_is_noetherian_linear_independent hi)
+  exact fintype_of_fintype_ne _ (@fintype.of_finite _ hi.finite_of_is_noetherian),
 end
 
 /-- An affine-independent subset of a finite-dimensional affine space is finite. -/

src/linear_algebra/dfinsupp.lean

@@ -443,10 +443,13 @@ lemma independent_iff_dfinsupp_sum_add_hom_injective (p : ι → add_subgroup N)
 ⟨independent.dfinsupp_sum_add_hom_injective, independent_of_dfinsupp_sum_add_hom_injective' p⟩
 
 omit dec_ι
+
 /-- If a family of submodules is `independent`, then a choice of nonzero vector from each submodule
-forms a linearly independent family. -/
+forms a linearly independent family.
+
+See also `complete_lattice.independent.linear_independent'`. -/
 lemma independent.linear_independent [no_zero_smul_divisors R N] (p : ι → submodule R N)
-  (hp : complete_lattice.independent p) {v : ι → N} (hv : ∀ i, v i ∈ p i) (hv' : ∀ i, v i ≠ 0) :
+  (hp : independent p) {v : ι → N} (hv : ∀ i, v i ∈ p i) (hv' : ∀ i, v i ≠ 0) :
   linear_independent R v :=
 begin
   classical,
@@ -463,6 +466,12 @@ begin
   simp [this, ha],
 end
 
+lemma independent_iff_linear_independent_of_ne_zero [no_zero_smul_divisors R N] {v : ι → N}
+  (h_ne_zero : ∀ i, v i ≠ 0) :
+  independent (λ i, R ∙ v i) ↔ linear_independent R v :=
+⟨λ hv, hv.linear_independent _ (λ i, submodule.mem_span_singleton_self $ v i) h_ne_zero,
+ λ hv, hv.independent_span_singleton⟩
+
 end ring
 
 end complete_lattice

src/linear_algebra/dimension.lean

@@ -283,6 +283,23 @@ end
 
 variables {R M}
 
+/-- A linearly-independent family of vectors in a module over a non-trivial ring must be finite if
+the module is Noetherian. -/
+lemma linear_independent.finite_of_is_noetherian [is_noetherian R M]
+  {v : ι → M} (hv : linear_independent R v) : finite ι :=
+begin
+  have hwf := is_noetherian_iff_well_founded.mp (by apply_instance : is_noetherian R M),
+  refine complete_lattice.well_founded.finite_of_independent hwf
+    hv.independent_span_singleton (λ i contra, _),
+  apply hv.ne_zero i,
+  have : v i ∈ R ∙ v i := submodule.mem_span_singleton_self (v i),
+  rwa [contra, submodule.mem_bot] at this,
+end
+
+lemma linear_independent.set_finite_of_is_noetherian [is_noetherian R M]
+  {s : set M} (hi : linear_independent R (coe : s → M)) : s.finite :=
+@set.finite_of_finite _ _ hi.finite_of_is_noetherian
+
 /--
 Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.
 -/
@@ -434,7 +451,7 @@ begin
     exact i.prop },
   choose v hvV hv using hI,
   have : linear_independent R v,
-  { exact (hV.comp _ subtype.coe_injective).linear_independent _ hvV hv },
+  { exact (hV.comp subtype.coe_injective).linear_independent _ hvV hv },
   exact cardinal_lift_le_dim_of_linear_independent' this
 end
 
@@ -681,26 +698,6 @@ begin
   exact le_top,
 end
 
-/-- A linearly-independent family of vectors in a module over a ring satisfying the strong rank
-condition must be finite if the module is Noetherian. -/
-noncomputable def fintype_of_is_noetherian_linear_independent [is_noetherian R M]
-  {v : ι → M} (hi : linear_independent R v) : fintype ι :=
-begin
-  have hfg : (⊤ : submodule R M).fg,
-  { exact is_noetherian_def.mp infer_instance ⊤, },
-  rw submodule.fg_def at hfg,
-  choose s hs hs' using hfg,
-  haveI : fintype s := hs.fintype,
-  apply linear_independent_fintype_of_le_span_fintype v hi s,
-  simp only [hs', set.subset_univ, submodule.top_coe, set.le_eq_subset],
-end
-
-/-- A linearly-independent subset of a module over a ring satisfying the strong rank condition
-must be finite if the module is Noetherian. -/
-lemma finite_of_is_noetherian_linear_independent [is_noetherian R M]
-  {s : set M} (hi : linear_independent R (coe : s → M)) : s.finite :=
-⟨fintype_of_is_noetherian_linear_independent hi⟩
-
 /--
 An auxiliary lemma for `linear_independent_le_basis`:
 we handle the case where the basis `b` is infinite.

src/linear_algebra/eigenspace.lean

@@ -326,7 +326,7 @@ lemma eigenvectors_linear_independent (f : End K V) (μs : set K) (xs : μs →
   (h_eigenvec : ∀ μ : μs, f.has_eigenvector μ (xs μ)) :
   linear_independent K xs :=
 complete_lattice.independent.linear_independent _
-  (f.eigenspaces_independent.comp (coe : μs → K) subtype.coe_injective)
+  (f.eigenspaces_independent.comp subtype.coe_injective)
   (λ μ, (h_eigenvec μ).1) (λ μ, (h_eigenvec μ).2)
 
 /-- The generalized eigenspace for a linear map `f`, a scalar `μ`, and an exponent `k ∈ ℕ` is the

src/linear_algebra/finite_dimensional.lean

@@ -167,7 +167,7 @@ end
 /-- A quotient of a finite-dimensional space is also finite-dimensional. -/
 instance finite_dimensional_quotient [finite_dimensional K V] (S : submodule K V) :
   finite_dimensional K (V ⧸ S) :=
-finite.of_surjective (submodule.mkq S) $ surjective_quot_mk _
+module.finite.of_surjective (submodule.mkq S) $ surjective_quot_mk _
 
 /-- The rank of a module as a natural number.
 

src/linear_algebra/linear_independent.lean

@@ -791,6 +791,20 @@ end, λ H, linear_independent_iff.2 $ λ l hl, begin
   { simp [hl] }
 end⟩
 
+/-- See also `complete_lattice.independent_iff_linear_independent_of_ne_zero`. -/
+lemma linear_independent.independent_span_singleton (hv : linear_independent R v) :
+  complete_lattice.independent $ λ i, R ∙ v i :=
+begin
+  refine complete_lattice.independent_def.mp (λ i m hm, (mem_bot R).mpr _),
+  simp only [mem_inf, mem_span_singleton, supr_subtype', ← span_range_eq_supr] at hm,
+  obtain ⟨⟨r, rfl⟩, hm⟩ := hm,
+  suffices : r = 0, { simp [this], },
+  apply linear_independent_iff_not_smul_mem_span.mp hv i,
+  convert hm,
+  ext,
+  simp,
+end
+
 variable (R)
 
 lemma exists_maximal_independent' (s : ι → M) :

src/linear_algebra/matrix/diagonal.lean

@@ -58,7 +58,7 @@ begin
   simp only [comap_infi, ← this, proj_diagonal, ker_smul'],
   have : univ ⊆ {i : m | w i = 0} ∪ {i : m | w i = 0}ᶜ, { rw set.union_compl_self },
   exact (supr_range_std_basis_eq_infi_ker_proj K (λi:m, K)
-    disjoint_compl_right this (finite.of_fintype _)).symm
+    disjoint_compl_right this (set.finite.of_fintype _)).symm
 end
 
 lemma range_diagonal [decidable_eq m] (w : m → K) :
@@ -75,7 +75,7 @@ lemma rank_diagonal [decidable_eq m] [decidable_eq K] (w : m → K) :
 begin
   have hu : univ ⊆ {i : m | w i = 0}ᶜ ∪ {i : m | w i = 0}, { rw set.compl_union_self },
   have hd : disjoint {i : m | w i ≠ 0} {i : m | w i = 0} := disjoint_compl_left,
-  have B₁ := supr_range_std_basis_eq_infi_ker_proj K (λi:m, K) hd hu (finite.of_fintype _),
+  have B₁ := supr_range_std_basis_eq_infi_ker_proj K (λi:m, K) hd hu (set.finite.of_fintype _),
   have B₂ := @infi_ker_proj_equiv K _ _ (λi:m, K) _ _ _ _ (by simp; apply_instance) hd hu,
   rw [rank, range_diagonal, B₁, ←@dim_fun' K],
   apply linear_equiv.dim_eq,

src/linear_algebra/span.lean

@@ -200,9 +200,16 @@ by rw [submodule.span_union, p.span_eq]
 lemma span_sup : span R s ⊔ p = span R (s ∪ p) :=
 by rw [submodule.span_union, p.span_eq]
 
-lemma span_eq_supr_of_singleton_spans (s : set M) : span R s = ⨆ x ∈ s, span R {x} :=
+/- Note that the character `∙` U+2219 used below is different from the scalar multiplication
+character `•` U+2022 and the matrix multiplication character `⬝` U+2B1D. -/
+notation R`∙`:1000 x := span R (@singleton _ _ set.has_singleton x)
+
+lemma span_eq_supr_of_singleton_spans (s : set M) : span R s = ⨆ x ∈ s, R ∙ x :=
 by simp only [←span_Union, set.bUnion_of_singleton s]
 
+lemma span_range_eq_supr {ι : Type*} {v : ι → M} : span R (range v) = ⨆ i, R ∙ v i :=
+by rw [span_eq_supr_of_singleton_spans, supr_range]
+
 lemma span_smul_le (s : set M) (r : R) :
   span R (r • s) ≤ span R s :=
 begin
@@ -320,10 +327,6 @@ end
 
 end
 
-/- This is the character `∙`, with escape sequence `\.`, and is thus different from the scalar
-multiplication character `•`, with escape sequence `\bub`. -/
-notation R`∙`:1000 x := span R (@singleton _ _ set.has_singleton x)
-
 lemma mem_span_singleton_self (x : M) : x ∈ R ∙ x := subset_span rfl
 
 lemma nontrivial_span_singleton {x : M} (h : x ≠ 0) : nontrivial (R ∙ x) :=
@@ -780,7 +783,9 @@ variables (R) (M) [semiring R] [add_comm_monoid M] [module R M]
 lemma span_singleton_eq_range (x : M) : (R ∙ x) = (to_span_singleton R M x).range :=
 submodule.ext $ λ y, by {refine iff.trans _ linear_map.mem_range.symm, exact mem_span_singleton }
 
-lemma to_span_singleton_one (x : M) : to_span_singleton R M x 1 = x := one_smul _ _
+@[simp] lemma to_span_singleton_one (x : M) : to_span_singleton R M x 1 = x := one_smul _ _
+
+@[simp] lemma to_span_singleton_zero : to_span_singleton R M 0 = 0 := by { ext, simp, }
 
 end
 

src/measure_theory/constructions/pi.lean

@@ -428,7 +428,7 @@ lemma ae_le_pi {β : ι → Type*} [Π i, preorder (β i)] {f f' : Π i, α i 
 
 lemma ae_le_set_pi {I : set ι} {s t : Π i, set (α i)} (h : ∀ i ∈ I, s i ≤ᵐ[μ i] t i) :
   (set.pi I s) ≤ᵐ[measure.pi μ] (set.pi I t) :=
-((eventually_all_finite (finite.of_fintype I)).2
+((eventually_all_finite (set.finite.of_fintype I)).2
   (λ i hi, tendsto_eval_ae_ae.eventually (h i hi))).mono $
     λ x hst hx i hi, hst i hi $ hx i hi
 

src/measure_theory/integral/divergence_theorem.lean

@@ -333,7 +333,7 @@ calc ∫ x in Icc a b, DF x = ∫ x in Icc a b, ∑ i, f' i x (eL.symm $ e i) :
       rw ← hIcc,
       refine preimage_interior_subset_interior_preimage eL.continuous _,
       simp only [set.mem_preimage, eL.apply_symm_apply, ← pi_univ_Icc,
-        interior_pi_set (finite.of_fintype _), interior_Icc],
+        interior_pi_set (set.finite.of_fintype _), interior_Icc],
       exact hx.1 },
     { rw [← he_vol.integrable_on_comp_preimage he_emb, hIcc],
       simp [← hDF, (∘), Hi] }

src/measure_theory/measurable_space.lean

@@ -204,7 +204,7 @@ end
 
 lemma measurable_of_fintype [fintype α] [measurable_singleton_class α] (f : α → β) :
   measurable f :=
-λ s hs, (finite.of_fintype (f ⁻¹' s)).measurable_set
+λ s hs, (set.finite.of_fintype (f ⁻¹' s)).measurable_set
 
 end typeclass_measurable_space
 

src/measure_theory/measure/haar_lebesgue.lean

@@ -51,7 +51,7 @@ def topological_space.positive_compacts.pi_Icc01 (ι : Type*) [fintype ι] :
   positive_compacts (ι → ℝ) :=
 { carrier := pi univ (λ i, Icc 0 1),
   compact' := is_compact_univ_pi (λ i, is_compact_Icc),
-  interior_nonempty' := by simp only [interior_pi_set, finite.of_fintype, interior_Icc,
+  interior_nonempty' := by simp only [interior_pi_set, set.finite.of_fintype, interior_Icc,
     univ_pi_nonempty_iff, nonempty_Ioo, implies_true_iff, zero_lt_one] }
 
 namespace measure_theory

src/order/compactly_generated.lean

@@ -9,6 +9,7 @@ import order.order_iso_nat
 import order.sup_indep
 import order.zorn
 import data.finset.order
+import data.finite.default
 
 /-!
 # Compactness properties for complete lattices
@@ -228,6 +229,8 @@ alias is_Sup_finite_compact_iff_is_sup_closed_compact ↔
       _ is_sup_closed_compact.is_Sup_finite_compact
 alias is_sup_closed_compact_iff_well_founded ↔ _ _root_.well_founded.is_sup_closed_compact
 
+variables {α}
+
 lemma well_founded.finite_of_set_independent (h : well_founded ((>) : α → α → Prop))
   {s : set α} (hs : set_independent s) : s.finite :=
 begin
@@ -247,6 +250,13 @@ begin
   exact le_Sup hx₀,
 end
 
+lemma well_founded.finite_of_independent (hwf : well_founded ((>) : α → α → Prop))
+  {ι : Type*} {t : ι → α} (ht : independent t) (h_ne_bot : ∀ i, t i ≠ ⊥) : finite ι :=
+begin
+  haveI := (well_founded.finite_of_set_independent hwf ht.set_independent_range).finite,
+  exact finite.of_injective_finite_range (ht.injective h_ne_bot),
+end
+
 end complete_lattice
 
 /-- A complete lattice is said to be compactly generated if any