feat(linear_algebra): free_of_finite_type_torsion_free (#7341)

A finite type torsion free module over a PID is free.

There are also some tiny preliminaries, and I moved `submodule.map_span` to `linear_map.map_span` to allow using the dot notation more often.

src/algebra/lie/ideal_operations.lean

@@ -180,7 +180,7 @@ begin
   suffices : ⁅map f I₁, map f I₂⁆ ≤ map f ⁅I₁, I₂⁆, { exact le_antisymm (map_bracket_le f) this, },
   rw [← lie_submodule.coe_submodule_le_coe_submodule, coe_map_of_surjective h,
     lie_submodule.lie_ideal_oper_eq_linear_span,
-    lie_submodule.lie_ideal_oper_eq_linear_span, submodule.map_span],
+    lie_submodule.lie_ideal_oper_eq_linear_span, linear_map.map_span],
   apply submodule.span_mono,
   rintros x ⟨⟨z₁, h₁⟩, ⟨z₂, h₂⟩, rfl⟩,
   obtain ⟨y₁, rfl⟩ := mem_map_of_surjective h h₁,
@@ -206,7 +206,7 @@ begin
   rw [← lie_submodule.coe_to_submodule_eq_iff, comap_coe_submodule,
     lie_submodule.sup_coe_to_submodule, f.ker_coe_submodule, ← linear_map.comap_map_eq,
     lie_submodule.lie_ideal_oper_eq_linear_span, lie_submodule.lie_ideal_oper_eq_linear_span,
-    submodule.map_span],
+    linear_map.map_span],
   congr, simp only [lie_hom.coe_to_linear_map, set.mem_set_of_eq], ext y,
   split,
   { rintros ⟨⟨x₁, hx₁⟩, ⟨x₂, hx₂⟩, hy⟩, rw ← hy,

src/algebra/module/basic.lean

@@ -380,6 +380,7 @@ for the vanishing of elements (especially in modules over division rings).
 -/
 
 /-- `no_zero_smul_divisors R M` states that a scalar multiple is `0` only if either argument is `0`.
+This a version of saying that `M` is torsion free, without assuming `R` is zero-divisor free.
 
 The main application of `no_zero_smul_divisors R M`, when `M` is a module,
 is the result `smul_eq_zero`: a scalar multiple is `0` iff either argument is `0`.

src/analysis/calculus/tangent_cone.lean

@@ -329,7 +329,7 @@ begin
   simp only [unique_diff_within_at_iff, closure_pi_set] at h ⊢,
   refine ⟨(dense_pi univ (λ i _, (h i).1)).mono _, λ i _, (h i).2⟩,
   norm_cast,
-  simp only [← submodule.supr_map_single, supr_le_iff, submodule.map_span, submodule.span_le,
+  simp only [← submodule.supr_map_single, supr_le_iff, linear_map.map_span, submodule.span_le,
     ← maps_to'],
   exact λ i, (maps_to_tangent_cone_pi $ λ j hj, (h j).2).mono subset.rfl submodule.subset_span
 end

src/linear_algebra/basic.lean

@@ -762,11 +762,25 @@ lemma map_span (f : M →ₗ[R] M₂) (s : set M) :
 eq.symm $ span_eq_of_le _ (set.image_subset f subset_span) $
 map_le_iff_le_comap.2 $ span_le.2 $ λ x hx, subset_span ⟨x, hx, rfl⟩
 
+alias submodule.map_span ← linear_map.map_span
+
+lemma map_span_le {R M M₂ : Type*} [semiring R] [add_comm_monoid M]
+  [add_comm_monoid M₂] [module R M] [module R M₂] (f : M →ₗ[R] M₂)
+  (s : set M) (N : submodule R M₂) : map f (span R s) ≤ N ↔ ∀ m ∈ s, f m ∈ N :=
+begin
+  rw [f.map_span, span_le, set.image_subset_iff],
+  exact iff.rfl
+end
+
+alias submodule.map_span_le ← linear_map.map_span_le
+
 /- See also `span_preimage_eq` below. -/
 lemma span_preimage_le (f : M →ₗ[R] M₂) (s : set M₂) :
   span R (f ⁻¹' s) ≤ (span R s).comap f :=
 by { rw [span_le, comap_coe], exact preimage_mono (subset_span), }
 
+alias submodule.span_preimage_le  ← linear_map.span_preimage_le
+
 /-- An induction principle for span membership. If `p` holds for 0 and all elements of `s`, and is
 preserved under addition and scalar multiplication, then `p` holds for all elements of the span of
 `s`. -/
@@ -1148,7 +1162,7 @@ ext $ λ y, ⟨λ ⟨x, hx, hy⟩, hy ▸ ⟨-x, neg_mem _ hx, f.map_neg x⟩,
 
 @[simp] lemma span_neg (s : set M) : span R (-s) = span R s :=
 calc span R (-s) = span R ((-linear_map.id : M →ₗ[R] M) '' s) : by simp
- ... = map (-linear_map.id) (span R s) : (map_span _ _).symm
+ ... = map (-linear_map.id) (span R s) : ((-linear_map.id).map_span _).symm
 ... = span R s : by simp
 
 lemma mem_span_insert' {y} {s : set M} : x ∈ span R (insert y s) ↔ ∃(a:R), x + a • y ∈ span R s :=

src/linear_algebra/free_module.lean

@@ -244,7 +244,7 @@ end integral_domain
 
 section principal_ideal_domain
 
-open submodule.is_principal
+open submodule.is_principal set submodule
 
 variables {ι : Type*} {R : Type*} [integral_domain R] [is_principal_ideal_ring R]
 variables {M : Type*} [add_comm_group M] [module R M] {b : ι → M}
@@ -334,6 +334,56 @@ lemma submodule.exists_is_basis_of_le_span
   ∃ (n : ℕ) (b : fin n → N), is_basis R b :=
 submodule.exists_is_basis_of_le le (is_basis_span hb)
 
+
+variable {M}
+
+/-- A finite type torsion free module over a PID is free. -/
+lemma module.free_of_finite_type_torsion_free [fintype ι] {s : ι → M} (hs : span R (range s) = ⊤)
+  [no_zero_smul_divisors R M] :
+  ∃ (n : ℕ) (B : fin n → M), is_basis R B :=
+begin
+  classical,
+  -- We define `N` as the submodule spanned by a maximal linear independent subfamily of `s`
+  obtain ⟨I : set ι,
+          indepI : linear_independent R (s ∘ coe : I → M),
+          hI : ∀ i ∉ I, ∃ a : R, a ≠ 0 ∧ a • s i ∈ span R (s '' I)⟩ :=
+    exists_maximal_independent R s,
+  let N := span R (range $ (s ∘ coe : I → M)), -- same as `span R (s '' I)` but more convenient
+  let sI : I → N := λ i, ⟨s i.1, subset_span (mem_range_self i)⟩, -- `s` restricted to `I`
+  have sI_basis : is_basis R sI, -- `s` restricted to `I` is a basis of `N`
+    from is_basis_span indepI,
+  -- Our first goal is to build `A ≠ 0` such that `A • M ⊆ N`
+  have exists_a : ∀ i : ι, ∃ a : R, a ≠ 0 ∧ a • s i ∈ N,
+  { intro i,
+    by_cases hi : i ∈ I,
+    { use [1, zero_ne_one.symm],
+      rw one_smul,
+      exact subset_span (mem_range_self (⟨i, hi⟩ : I)) },
+    { simpa [image_eq_range s I] using hI i hi } },
+  choose a ha ha' using exists_a,
+  let A := ∏ i, a i,
+  have hA : A ≠ 0,
+  { rw finset.prod_ne_zero_iff,
+    simpa using ha },
+  -- `M ≃ A • M` because `M` is torsion free and `A ≠ 0`
+  let φ : M →ₗ[R] M := linear_map.lsmul R M A,
+  have : φ.ker = ⊥,
+    from linear_map.ker_lsmul hA,
+  let ψ : M ≃ₗ[R] φ.range := linear_equiv.of_injective φ this,
+  have : φ.range ≤ N, -- as announced, `A • M ⊆ N`
+  { suffices : ∀ i, φ (s i) ∈ N,
+    { rw [linear_map.range_eq_map, ← hs, φ.map_span_le],
+      rintros _ ⟨i, rfl⟩, apply this },
+    intro i,
+    calc (∏ j, a j) • s i = (∏ j in {i}ᶜ, a j) • a i • s i :
+                                                 by rw [fintype.prod_eq_prod_compl_mul i, mul_smul]
+                      ... ∈ N  : N.smul_mem _ (ha' i) },
+  -- Since a submodule of a free `R`-module is free, we get that `A • M` is free
+  obtain ⟨n, B : fin n → φ.range, hB : is_basis R B⟩ :=
+    submodule.exists_is_basis_of_le this sI_basis,
+  -- hence `M` is free.
+  exact ⟨n, ψ.symm ∘ B, linear_equiv.is_basis hB ψ.symm⟩
+end
 end principal_ideal_domain
 
 /-- A set of linearly independent vectors in a module `M` over a semiring `S` is also linearly

src/linear_algebra/tensor_product.lean

@@ -204,6 +204,10 @@ lemma lsmul_injective [no_zero_smul_divisors R M] {x : R} (hx : x ≠ 0) :
   function.injective (lsmul R M x) :=
 smul_injective hx
 
+lemma ker_lsmul [no_zero_smul_divisors R M] {a : R} (ha : a ≠ 0) :
+  (linear_map.lsmul R M a).ker = ⊥ :=
+linear_map.ker_eq_bot_of_injective (linear_map.lsmul_injective ha)
+
 end comm_ring
 
 end linear_map

src/ring_theory/noetherian.lean

@@ -130,7 +130,7 @@ lemma fg_of_fg_map {R M P : Type*} [ring R] [add_comm_group M] [module R M]
   [add_comm_group P] [module R P] (f : M →ₗ[R] P) (hf : f.ker = ⊥) {N : submodule R M}
   (hfn : (N.map f).fg) : N.fg :=
 let ⟨t, ht⟩ := hfn in ⟨t.preimage f $ λ x _ y _ h, linear_map.ker_eq_bot.1 hf h,
-linear_map.map_injective hf $ by { rw [map_span, finset.coe_preimage,
+linear_map.map_injective hf $ by { rw [f.map_span, finset.coe_preimage,
     set.image_preimage_eq_inter_range, set.inter_eq_self_of_subset_left, ht],
   rw [← linear_map.range_coe, ← span_le, ht, ← map_top], exact map_mono le_top }⟩