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

…etherian`

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

@@ -59,14 +59,60 @@ 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
 
+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
+
 lemma sup_eq_top_iff_is_coprime {R : Type*} [comm_semiring R] (x y : R) :
   span ({x} : set R) ⊔ span {y} = ⊤ ↔ is_coprime x y :=
 begin

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⟩
+
 end ring
 
 end complete_lattice

src/linear_algebra/dimension.lean

@@ -285,6 +285,18 @@ 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 (λ 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
+
 /--
 Over any nontrivial ring, the existence of a finite spanning set implies that any basis is finite.
 -/
@@ -690,26 +702,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/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

@@ -790,6 +790,20 @@ end, λ H, linear_independent_iff.2 $ λ l hl, begin
   { simp [hl] }
 end⟩
 
+/-- See also `linear_independent_iff_independent_and_ne_zero`. -/
+lemma linear_independent.independent (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/span.lean

@@ -186,9 +186,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. -/
+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
@@ -306,10 +313,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) :=
@@ -766,7 +769,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/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.basic
 
 /-!
 # 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 ↔ _ 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,15 @@ 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
+  suffices : (set.range t).finite,
+  { haveI : finite (set.range t) := finite.of_fintype this.fintype,
+    exact finite.of_equiv (set.range t) (equiv.of_injective _ (ht.injective h_ne_bot)).symm, },
+  exact well_founded.finite_of_set_independent hwf ht.set_indepdent_range,
+end
+
 end complete_lattice
 
 /-- A complete lattice is said to be compactly generated if any

src/order/sup_indep.lean

@@ -161,7 +161,7 @@ end finset
 namespace complete_lattice
 variables [complete_lattice α]
 
-open set
+open set function
 
 /-- An independent set of elements in a complete lattice is one in which every element is disjoint
   from the `Sup` of the rest. -/
@@ -235,11 +235,11 @@ variables {t : ι → α} (ht : independent t)
 theorem independent_def : independent t ↔ ∀ i : ι, disjoint (t i) (⨆ (j ≠ i), t j) :=
 iff.rfl
 
-theorem independent_def' {ι : Type*} {t : ι → α} :
+theorem independent_def' :
   independent t ↔ ∀ i, disjoint (t i) (Sup (t '' {j | j ≠ i})) :=
 by {simp_rw Sup_image, refl}
 
-theorem independent_def'' {ι : Type*} {t : ι → α} :
+theorem independent_def'' :
   independent t ↔ ∀ i, disjoint (t i) (Sup {a | ∃ j ≠ i, t j = a}) :=
 by {rw independent_def', tidy}
 
@@ -253,21 +253,51 @@ lemma independent_pempty (t : pempty → α) : independent t.
 lemma independent.pairwise_disjoint : pairwise (disjoint on t) :=
 λ x y h, disjoint_Sup_right (ht x) ⟨y, supr_pos h.symm⟩
 
-lemma independent.mono {ι : Type*} {α : Type*} [complete_lattice α]
+lemma independent.mono
   {s t : ι → α} (hs : independent s) (hst : t ≤ s) :
   independent t :=
 λ i, (hs i).mono (hst i) $ supr₂_mono $ λ j _, hst j
 
 /-- Composing an independent indexed family with an injective function on the index results in
 another indepedendent indexed family. -/
-lemma independent.comp {ι ι' : Sort*} {α : Type*} [complete_lattice α]
-  {s : ι → α} (hs : independent s) (f : ι' → ι) (hf : function.injective f) :
-  independent (s ∘ f) :=
-λ i, (hs (f i)).mono_right $ begin
+lemma independent.comp
+  (f : ι' → ι) (hf : injective f) :
+  independent $ t ∘ f :=
+λ i, (ht (f i)).mono_right $ begin
   refine (supr_mono $ λ i, _).trans (supr_comp_le _ f),
   exact supr_const_mono hf.ne,
 end
 
+lemma independent.comp'
+  {f : ι' → ι} (hf : surjective f) (ht : independent $ t ∘ f) :
+  independent t :=
+begin
+  intros i,
+  obtain ⟨i', rfl⟩ := hf i,
+  rw ← hf.supr_comp,
+  exact (ht i').mono_right (bsupr_mono $ λ j' hij, mt (congr_arg f) hij),
+end
+
+lemma independent.set_indepdent_range (ht : independent t) :
+  set_independent $ range t :=
+begin
+  rw set_independent_iff,
+  rw ← coe_comp_range_factorization t at ht,
+  exact ht.comp' surjective_onto_range,
+end
+
+lemma independent.injective (ht : independent t) (h_ne_bot : ∀ i, t i ≠ ⊥) : injective t :=
+begin
+  intros i j h,
+  by_contra' contra,
+  apply h_ne_bot j,
+  suffices : t j ≤ ⨆ k (hk : k ≠ i), t k,
+  { replace ht := (ht i).mono_right this,
+    rwa [h, disjoint_self] at ht, },
+  replace contra : j ≠ i, { exact ne.symm contra, },
+  exact le_supr₂ j contra,
+end
+
 lemma independent_pair {i j : ι} (hij : i ≠ j) (huniv : ∀ k, k = i ∨ k = j):
   independent t ↔ disjoint (t i) (t j) :=
 begin