feat(linear_algebra/free_module): add lemmas (#7950)

Easy results about free modules.

src/algebra/category/Module/projective.lean

@@ -43,7 +43,7 @@ variables {R : Type u} [ring R] {M : Module.{(max u v)} R}
 -- We transport the corresponding result from `module.projective`.
 lemma projective_of_free {ι : Type*} (b : basis ι R M) : projective M :=
 projective.of_iso (Module.of_self_iso _)
-  ((is_projective.iff_projective).mp (module.projective_of_free b))
+  ((is_projective.iff_projective).mp (module.projective_of_basis b))
 
 /-- The category of modules has enough projectives, since every module is a quotient of a free
     module. -/

src/algebra/module/projective.lean

@@ -6,7 +6,7 @@ Authors: Kevin Buzzard
 
 import algebra.module.basic
 import linear_algebra.finsupp
-import linear_algebra.basis
+import linear_algebra.free_module
 
 /-!
 
@@ -166,9 +166,8 @@ begin
     simp },
 end
 
---TODO: use `module.free`
 /-- Free modules are projective. -/
-theorem projective_of_free {ι : Type*} (b : basis ι R P) : projective R P :=
+theorem projective_of_basis {ι : Type*} (b : basis ι R P) : projective R P :=
 begin
   -- need P →ₗ (P →₀ R) for definition of projective.
   -- get it from `ι → (P →₀ R)` coming from `b`.
@@ -179,6 +178,10 @@ begin
   exact b.total_repr m,
 end
 
+@[priority 100]
+instance projective_of_free [module.free R P] : module.projective R P :=
+projective_of_basis $ module.free.choose_basis R P
+
 end ring
 
 end module

src/linear_algebra/dfinsupp.lean

@@ -3,8 +3,8 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kenny Lau
 -/
-import data.dfinsupp
-import linear_algebra.basic
+import data.finsupp.to_dfinsupp
+import linear_algebra.basis
 
 /-!
 # Properties of the module `Π₀ i, M i`
@@ -189,4 +189,16 @@ lemma map_range.linear_equiv_symm (e : Π i, β₁ i ≃ₗ[R] β₂ i) :
 
 end map_range
 
+section basis
+
+/-- The direct sum of free modules is free.
+
+Note that while this is stated for `dfinsupp` not `direct_sum`, the types are defeq. -/
+noncomputable def basis {η : ι → Type*} (b : Π i, basis (η i) R (M i)) :
+  basis (Σ i, η i) R (Π₀ i, M i) :=
+basis.of_repr ((map_range.linear_equiv (λ i, (b i).repr)).trans
+  (sigma_finsupp_lequiv_dfinsupp R).symm)
+
+end basis
+
 end dfinsupp

src/linear_algebra/free_module.lean

@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
 
-import linear_algebra.basis
-import logic.small
 import linear_algebra.direct_sum.finsupp
+import linear_algebra.std_basis
+import logic.small
 
 /-!
 
@@ -25,13 +25,13 @@ universes u v w z
 
 variables (R : Type u) (M : Type v) (N : Type z)
 
-open_locale tensor_product
+open_locale tensor_product direct_sum
 
 section basic
 
 variables [semiring R] [add_comm_monoid M] [module R M]
 
-/-- `finite_free R M` is the statement that the `R`-module `R` is free of finite rank.-/
+/-- `module.free R M` is the statement that the `R`-module `M` is free.-/
 class module.free : Prop :=
 (exists_basis [] : nonempty (Σ (I : Type v), basis I R M))
 
@@ -117,6 +117,18 @@ instance self : module.free R R := of_basis $ basis.singleton unit R
 instance of_subsingleton [subsingleton N] : module.free R N :=
 of_basis (basis.empty N : basis pempty R N)
 
+instance dfinsupp {ι : Type*} (M : ι → Type*) [Π (i : ι), add_comm_monoid (M i)]
+  [Π (i : ι), module R (M i)] [Π (i : ι), module.free R (M i)] : module.free R (Π₀ i, M i) :=
+of_basis $ dfinsupp.basis $ λ i, choose_basis R (M i)
+
+instance direct_sum {ι : Type*} (M : ι → Type*) [Π (i : ι), add_comm_monoid (M i)]
+  [Π (i : ι), module R (M i)] [Π (i : ι), module.free R (M i)] : module.free R (⨁ i, M i) :=
+module.free.dfinsupp R M
+
+instance pi {ι : Type*} [fintype ι] {M : ι → Type*} [Π (i : ι), add_comm_group (M i)]
+[Π (i : ι), module R (M i)] [Π (i : ι), module.free R (M i)] : module.free R (Π i, M i) :=
+of_basis $ pi.basis $ λ i, choose_basis R (M i)
+
 end semiring
 
 section comm_ring

src/linear_algebra/std_basis.lean

@@ -158,10 +158,9 @@ variables {R : Type*}
 
 section module
 variables {η : Type*} {ιs : η → Type*} {Ms : η → Type*}
-variables [ring R] [∀i, add_comm_group (Ms i)] [∀i, module R (Ms i)]
 
-lemma linear_independent_std_basis [decidable_eq η]
-  (v : Πj, ιs j → (Ms j)) (hs : ∀i, linear_independent R (v i)) :
+lemma linear_independent_std_basis [ring R] [∀i, add_comm_group (Ms i)] [∀i, module R (Ms i)]
+  [decidable_eq η] (v : Πj, ιs j → (Ms j)) (hs : ∀i, linear_independent R (v i)) :
   linear_independent R (λ (ji : Σ j, ιs j), std_basis R Ms ji.1 (v ji.1 ji.2)) :=
 begin
   have hs' : ∀j : η, linear_independent R (λ i : ιs j, std_basis R Ms j (v j i)),
@@ -187,6 +186,8 @@ begin
     exact (disjoint_std_basis_std_basis _ _ _ _ h₃).mono h₁ h₂ }
 end
 
+variables [semiring R] [∀i, add_comm_monoid (Ms i)] [∀i, module R (Ms i)]
+
 variable [fintype η]
 
 section