Acl/reorg tensor product (#11282)

Move: * `Mathlib/Algebra/Module/DirectLimitAndTensorProduct.lean` to `LinearAlgebra/TensorProduct/DirectLimit.lean` * `Mathlib/LinearAlgebra/TensorProduct` to `Mathlib/LinearAlgebra.TensorProduct.Basic.lean` * `Mathlib/RingTheory/TensorProduct` to `Mathlib/RingTheory/TensorProduct/Basic.lean`. This follows suggestions 1, 2, 3 of https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Tensor.20Products.20of.20modules.20and.20rings/near/424605543 Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>
leanprover-community · Mar 11, 2024 · 0ee5f82 · 0ee5f82
1 parent f8a97cf
commit 0ee5f82
Show file tree

Hide file tree

Showing 32 changed files with 32 additions and 32 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -333,7 +333,6 @@ import Mathlib.Algebra.Module.BigOperators
 import Mathlib.Algebra.Module.Bimodule
 import Mathlib.Algebra.Module.CharacterModule
 import Mathlib.Algebra.Module.DedekindDomain
-import Mathlib.Algebra.Module.DirectLimitAndTensorProduct
 import Mathlib.Algebra.Module.Equiv
 import Mathlib.Algebra.Module.GradedModule
 import Mathlib.Algebra.Module.Hom
@@ -2652,15 +2651,16 @@ import Mathlib.LinearAlgebra.TensorAlgebra.Basis
 import Mathlib.LinearAlgebra.TensorAlgebra.Grading
 import Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
 import Mathlib.LinearAlgebra.TensorPower
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
+import Mathlib.LinearAlgebra.TensorProduct.Basis
+import Mathlib.LinearAlgebra.TensorProduct.DirectLimit
 import Mathlib.LinearAlgebra.TensorProduct.Graded.External
 import Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
 import Mathlib.LinearAlgebra.TensorProduct.Matrix
 import Mathlib.LinearAlgebra.TensorProduct.Opposite
 import Mathlib.LinearAlgebra.TensorProduct.Prod
 import Mathlib.LinearAlgebra.TensorProduct.RightExactness
 import Mathlib.LinearAlgebra.TensorProduct.Tower
-import Mathlib.LinearAlgebra.TensorProductBasis
 import Mathlib.LinearAlgebra.Trace
 import Mathlib.LinearAlgebra.UnitaryGroup
 import Mathlib.LinearAlgebra.Vandermonde
@@ -3404,7 +3404,7 @@ import Mathlib.RingTheory.Subring.Units
 import Mathlib.RingTheory.Subsemiring.Basic
 import Mathlib.RingTheory.Subsemiring.Order
 import Mathlib.RingTheory.Subsemiring.Pointwise
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.RingTheory.Trace
 import Mathlib.RingTheory.UniqueFactorizationDomain
 import Mathlib.RingTheory.Valuation.Basic

diff --git a/Mathlib/Algebra/Algebra/Bilinear.lean b/Mathlib/Algebra/Algebra/Bilinear.lean
@@ -6,7 +6,7 @@ Authors: Kenny Lau, Yury Kudryashov
 import Mathlib.Algebra.Algebra.Basic
 import Mathlib.Algebra.Algebra.NonUnitalHom
 import Mathlib.Algebra.GroupPower.IterateHom
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 
 #align_import algebra.algebra.bilinear from "leanprover-community/mathlib"@"657df4339ae6ceada048c8a2980fb10e393143ec"
 

diff --git a/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean b/Mathlib/Algebra/Category/AlgebraCat/Monoidal.lean
@@ -6,7 +6,7 @@ Authors: Eric Wieser
 import Mathlib.CategoryTheory.Monoidal.Transport
 import Mathlib.Algebra.Category.AlgebraCat.Basic
 import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 /-!
 # The monoidal category structure on R-algebras

diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jujian Zhang
 -/
 import Mathlib.Algebra.Category.ModuleCat.EpiMono
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import algebra.category.Module.change_of_rings from "leanprover-community/mathlib"@"56b71f0b55c03f70332b862e65c3aa1aa1249ca1"
 

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kevin Buzzard, Scott Morrison, Jakob von Raumer
 -/
 import Mathlib.Algebra.Category.ModuleCat.Basic
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 import Mathlib.CategoryTheory.Monoidal.Linear
 
 #align_import algebra.category.Module.monoidal.basic from "leanprover-community/mathlib"@"74403a3b2551b0970855e14ef5e8fd0d6af1bfc2"

diff --git a/Mathlib/Algebra/Category/Ring/Constructions.lean b/Mathlib/Algebra/Category/Ring/Constructions.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
 import Mathlib.CategoryTheory.Limits.Shapes.Pullbacks
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.Algebra.Category.Ring.Limits
 import Mathlib.Algebra.Category.Ring.Instances
 import Mathlib.CategoryTheory.Limits.Shapes.StrictInitial

diff --git a/Mathlib/Algebra/Lie/BaseChange.lean b/Mathlib/Algebra/Lie/BaseChange.lean
@@ -6,7 +6,7 @@ Authors: Oliver Nash
 import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.Algebra.Lie.TensorProduct
 import Mathlib.LinearAlgebra.TensorProduct.Tower
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import algebra.lie.base_change from "leanprover-community/mathlib"@"9264b15ee696b7ca83f13c8ad67c83d6eb70b730"
 

diff --git a/Mathlib/Algebra/Module/Bimodule.lean b/Mathlib/Algebra/Module/Bimodule.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Oliver Nash. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import algebra.module.bimodule from "leanprover-community/mathlib"@"58cef51f7a819e7227224461e392dee423302f2d"
 

diff --git a/Mathlib/Data/Matrix/Kronecker.lean b/Mathlib/Data/Matrix/Kronecker.lean
@@ -7,8 +7,8 @@ import Mathlib.Data.Matrix.Basic
 import Mathlib.Data.Matrix.Block
 import Mathlib.LinearAlgebra.Matrix.Determinant
 import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
-import Mathlib.LinearAlgebra.TensorProduct
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import data.matrix.kronecker from "leanprover-community/mathlib"@"3e068ece210655b7b9a9477c3aff38a492400aa1"
 

diff --git a/Mathlib/FieldTheory/Adjoin.lean b/Mathlib/FieldTheory/Adjoin.lean
@@ -6,7 +6,7 @@ Authors: Thomas Browning, Patrick Lutz
 import Mathlib.FieldTheory.IntermediateField
 import Mathlib.FieldTheory.Separable
 import Mathlib.FieldTheory.SplittingField.IsSplittingField
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import field_theory.adjoin from "leanprover-community/mathlib"@"df76f43357840485b9d04ed5dee5ab115d420e87"
 

diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/BaseChange.lean
@@ -6,7 +6,7 @@ Authors: Eric Wieser
 import Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
 import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
 import Mathlib.LinearAlgebra.TensorProduct.Opposite
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 /-!
 # The base change of a clifford algebra

diff --git a/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean b/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
@@ -3,7 +3,7 @@ Copyright (c) 2018 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau, Mario Carneiro, Eric Wieser
 -/
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 import Mathlib.Algebra.DirectSum.Module
 
 #align_import linear_algebra.direct_sum.tensor_product from "leanprover-community/mathlib"@"9b9d125b7be0930f564a68f1d73ace10cf46064d"

diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean
@@ -9,7 +9,7 @@ import Mathlib.LinearAlgebra.FreeModule.Finite.Basic
 import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 import Mathlib.LinearAlgebra.Projection
 import Mathlib.LinearAlgebra.SesquilinearForm
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import linear_algebra.dual from "leanprover-community/mathlib"@"b1c017582e9f18d8494e5c18602a8cb4a6f843ac"
 

diff --git a/Mathlib/LinearAlgebra/FreeModule/Basic.lean b/Mathlib/LinearAlgebra/FreeModule/Basic.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Riccardo Brasca
 -/
 import Mathlib.Data.Finsupp.Fintype
-import Mathlib.LinearAlgebra.TensorProductBasis
+import Mathlib.LinearAlgebra.TensorProduct.Basis
 
 #align_import linear_algebra.free_module.basic from "leanprover-community/mathlib"@"4e7e7009099d4a88a750de710909b95487bf0124"
 

diff --git a/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean b/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
 import Mathlib.LinearAlgebra.Multilinear.Basic
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 
 #align_import linear_algebra.multilinear.tensor_product from "leanprover-community/mathlib"@"ce11c3c2a285bbe6937e26d9792fda4e51f3fe1a"
 

diff --git a/Mathlib/LinearAlgebra/TensorProduct.lean → ...ib/LinearAlgebra/TensorProduct/Basic.lean b/Mathlib/LinearAlgebra/TensorProduct.lean → ...ib/LinearAlgebra/TensorProduct/Basic.lean
diff --git a/...lib/LinearAlgebra/TensorProductBasis.lean → ...ib/LinearAlgebra/TensorProduct/Basis.lean b/...lib/LinearAlgebra/TensorProductBasis.lean → ...ib/LinearAlgebra/TensorProduct/Basis.lean
diff --git a/...a/Module/DirectLimitAndTensorProduct.lean → ...earAlgebra/TensorProduct/DirectLimit.lean b/...a/Module/DirectLimitAndTensorProduct.lean → ...earAlgebra/TensorProduct/DirectLimit.lean
diff --git a/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean b/Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
@@ -5,7 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.Data.Int.Order.Units
 import Mathlib.Data.ZMod.IntUnitsPower
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.LinearAlgebra.DirectSum.TensorProduct
 import Mathlib.Algebra.DirectSum.Algebra
 

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Matrix.lean b/Mathlib/LinearAlgebra/TensorProduct/Matrix.lean
@@ -5,7 +5,7 @@ Authors: Eric Wieser
 -/
 import Mathlib.Data.Matrix.Kronecker
 import Mathlib.LinearAlgebra.Matrix.ToLin
-import Mathlib.LinearAlgebra.TensorProductBasis
+import Mathlib.LinearAlgebra.TensorProduct.Basis
 
 #align_import linear_algebra.tensor_product.matrix from "leanprover-community/mathlib"@"f784cc6142443d9ee623a20788c282112c322081"
 

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Opposite.lean b/Mathlib/LinearAlgebra/TensorProduct/Opposite.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.Algebra.Algebra.Opposite
 
 /-! # `MulOpposite` distributes over `⊗`

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Prod.lean b/Mathlib/LinearAlgebra/TensorProduct/Prod.lean
@@ -3,7 +3,7 @@ Copyright (c) 2023 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 import Mathlib.LinearAlgebra.Prod
 
 /-!

diff --git a/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean b/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
@@ -5,7 +5,7 @@ Authors: Antoine Chambetr-Loir
 -/
 
 import Mathlib.Algebra.Exact
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 /-! # Right-exactness properties of tensor product
 

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
@@ -5,7 +5,7 @@ Authors: Scott Morrison, Johan Commelin, Eric Wieser
 -/
 import Mathlib.Algebra.Algebra.Tower
 import Mathlib.LinearAlgebra.Basic
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 
 #align_import ring_theory.tensor_product from "leanprover-community/mathlib"@"88fcdc3da43943f5b01925deddaa5bf0c0e85e4e"
 

diff --git a/Mathlib/RepresentationTheory/Basic.lean b/Mathlib/RepresentationTheory/Basic.lean
@@ -9,7 +9,7 @@ import Mathlib.Algebra.Module.LinearMap.Basic
 import Mathlib.Algebra.MonoidAlgebra.Basic
 import Mathlib.LinearAlgebra.Dual
 import Mathlib.LinearAlgebra.Contraction
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import representation_theory.basic from "leanprover-community/mathlib"@"c04bc6e93e23aa0182aba53661a2211e80b6feac"
 

diff --git a/Mathlib/RingTheory/Bialgebra.lean b/Mathlib/RingTheory/Bialgebra.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ali Ramsey, Kevin Buzzard
 -/
 import Mathlib.RingTheory.Coalgebra
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 /-!
 # Bialgebras

diff --git a/Mathlib/RingTheory/Coalgebra.lean b/Mathlib/RingTheory/Coalgebra.lean
@@ -5,7 +5,7 @@ Authors: Ali Ramsey, Eric Wieser
 -/
 import Mathlib.LinearAlgebra.Finsupp
 import Mathlib.LinearAlgebra.Prod
-import Mathlib.LinearAlgebra.TensorProduct
+import Mathlib.LinearAlgebra.TensorProduct.Basic
 
 /-!
 # Coalgebras

diff --git a/Mathlib/RingTheory/IntegralClosure.lean b/Mathlib/RingTheory/IntegralClosure.lean
@@ -10,7 +10,7 @@ import Mathlib.RingTheory.Adjoin.FG
 import Mathlib.RingTheory.FiniteType
 import Mathlib.RingTheory.Polynomial.ScaleRoots
 import Mathlib.RingTheory.Polynomial.Tower
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import ring_theory.integral_closure from "leanprover-community/mathlib"@"641b6a82006416ec431b2987b354af9311fed4f2"
 

diff --git a/Mathlib/RingTheory/IsTensorProduct.lean b/Mathlib/RingTheory/IsTensorProduct.lean
@@ -3,7 +3,7 @@ Copyright (c) 2022 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 import Mathlib.Algebra.Module.ULift
 
 #align_import ring_theory.is_tensor_product from "leanprover-community/mathlib"@"c4926d76bb9c5a4a62ed2f03d998081786132105"

diff --git a/Mathlib/RingTheory/MatrixAlgebra.lean b/Mathlib/RingTheory/MatrixAlgebra.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Scott Morrison, Eric Wieser
 -/
 import Mathlib.Data.Matrix.Basis
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 #align_import ring_theory.matrix_algebra from "leanprover-community/mathlib"@"6c351a8fb9b06e5a542fdf427bfb9f46724f9453"
 

diff --git a/Mathlib/RingTheory/TensorProduct.lean → Mathlib/RingTheory/TensorProduct/Basic.lean b/Mathlib/RingTheory/TensorProduct.lean → Mathlib/RingTheory/TensorProduct/Basic.lean
diff --git a/test/instance_diamonds.lean b/test/instance_diamonds.lean
@@ -10,7 +10,7 @@ import Mathlib.GroupTheory.GroupAction.Units
 import Mathlib.Data.Complex.Module
 import Mathlib.RingTheory.Algebraic
 import Mathlib.Data.ZMod.Basic
-import Mathlib.RingTheory.TensorProduct
+import Mathlib.RingTheory.TensorProduct.Basic
 
 /-! # Tests that instances do not form diamonds -/