chore(LinearAlgebra/DFinsupp): remove dependency on Basis (#6706)

The motivation here is to explore re-defining `Basis` with `DFinsupp` instead of `Finsupp`, in order to make it computable.
leanprover-community · Sep 12, 2023 · 5128540 · 5128540
1 parent a9f079b
commit 5128540
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 14 deletions.
diff --git a/Mathlib/Algebra/DirectSum/Module.lean b/Mathlib/Algebra/DirectSum/Module.lean
@@ -5,6 +5,7 @@ Authors: Kenny Lau
 -/
 import Mathlib.Algebra.DirectSum.Basic
 import Mathlib.LinearAlgebra.DFinsupp
+import Mathlib.LinearAlgebra.Basis
 
 #align_import algebra.direct_sum.module from "leanprover-community/mathlib"@"6623e6af705e97002a9054c1c05a980180276fc1"
 

diff --git a/Mathlib/LinearAlgebra/DFinsupp.lean b/Mathlib/LinearAlgebra/DFinsupp.lean
@@ -4,7 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kenny Lau
 -/
 import Mathlib.Data.Finsupp.ToDFinsupp
-import Mathlib.LinearAlgebra.Basis
+import Mathlib.LinearAlgebra.Finsupp
+import Mathlib.LinearAlgebra.LinearIndependent
 
 #align_import linear_algebra.dfinsupp from "leanprover-community/mathlib"@"a148d797a1094ab554ad4183a4ad6f130358ef64"
 
@@ -279,19 +280,6 @@ theorem coprodMap_apply_single (f : ∀ i : ι, M i →ₗ[R] N) (i : ι) (x : M
 
 end CoprodMap
 
-section Basis
-
-/-- The direct sum of free modules is free.
-
-Note that while this is stated for `DFinsupp` not `DirectSum`, the types are defeq. -/
-noncomputable def basis {η : ι → Type*} (b : ∀ i, Basis (η i) R (M i)) :
-    Basis (Σi, η i) R (Π₀ i, M i) :=
-  .ofRepr
-    ((mapRange.linearEquiv fun i => (b i).repr).trans (sigmaFinsuppLequivDFinsupp R).symm)
-#align dfinsupp.basis DFinsupp.basis
-
-end Basis
-
 end DFinsupp
 
 namespace Submodule

diff --git a/Mathlib/LinearAlgebra/FinsuppVectorSpace.lean b/Mathlib/LinearAlgebra/FinsuppVectorSpace.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
+import Mathlib.LinearAlgebra.DFinsupp
 import Mathlib.LinearAlgebra.StdBasis
 
 #align_import linear_algebra.finsupp_vector_space from "leanprover-community/mathlib"@"59628387770d82eb6f6dd7b7107308aa2509ec95"
@@ -136,6 +137,21 @@ end Semiring
 
 end Finsupp
 
+namespace DFinsupp
+variable {ι : Type*} {R : Type*} {M : ι → Type*}
+variable [Semiring R] [∀ i, AddCommMonoid (M i)] [∀ i, Module R (M i)]
+
+/-- The direct sum of free modules is free.
+
+Note that while this is stated for `DFinsupp` not `DirectSum`, the types are defeq. -/
+noncomputable def basis {η : ι → Type*} (b : ∀ i, Basis (η i) R (M i)) :
+    Basis (Σi, η i) R (Π₀ i, M i) :=
+  .ofRepr
+    ((mapRange.linearEquiv fun i => (b i).repr).trans (sigmaFinsuppLequivDFinsupp R).symm)
+#align dfinsupp.basis DFinsupp.basis
+
+end DFinsupp
+
 /-! TODO: move this section to an earlier file. -/