[Merged by Bors] - chore(RingTheory/TensorProduct): split finite/free results into new files

Mathlib.lean

@@ -4284,6 +4284,8 @@ import Mathlib.RingTheory.Smooth.StandardSmooth
 import Mathlib.RingTheory.Support
 import Mathlib.RingTheory.SurjectiveOnStalks
 import Mathlib.RingTheory.TensorProduct.Basic
+import Mathlib.RingTheory.TensorProduct.Finite
+import Mathlib.RingTheory.TensorProduct.Free
 import Mathlib.RingTheory.TensorProduct.MvPolynomial
 import Mathlib.RingTheory.Trace.Basic
 import Mathlib.RingTheory.Trace.Defs

Mathlib/Algebra/Module/LinearMap/Polynomial.lean

@@ -5,9 +5,9 @@ Authors: Johan Commelin
 -/
 import Mathlib.Algebra.MvPolynomial.Monad
 import Mathlib.LinearAlgebra.Charpoly.ToMatrix
-import Mathlib.LinearAlgebra.Dimension.Finrank
 import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
 import Mathlib.LinearAlgebra.Matrix.Charpoly.Univ
+import Mathlib.RingTheory.TensorProduct.Free
 
 /-!
 # Characteristic polynomials of linear families of endomorphisms

Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean

@@ -5,6 +5,7 @@ Authors: Antoine Chambert-Loir
 -/
 
 import Mathlib.Algebra.Exact
+import Mathlib.RingTheory.Ideal.Maps
 import Mathlib.RingTheory.TensorProduct.Basic
 
 /-! # Right-exactness properties of tensor product

Mathlib/LinearAlgebra/TensorProduct/Vanishing.lean

@@ -5,6 +5,7 @@ Authors: Mitchell Lee
 -/
 import Mathlib.LinearAlgebra.TensorProduct.RightExactness
 import Mathlib.LinearAlgebra.TensorProduct.Finiteness
+import Mathlib.LinearAlgebra.DirectSum.Finsupp
 
 /-! # Vanishing of elements in a tensor product of two modules
 

Mathlib/LinearAlgebra/Trace.lean

@@ -5,6 +5,7 @@ Authors: Johannes Hölzl, Patrick Massot, Casper Putz, Anne Baanen, Antoine Labe
 -/
 import Mathlib.LinearAlgebra.Contraction
 import Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
+import Mathlib.RingTheory.TensorProduct.Free
 
 /-!
 # Trace of a linear map
@@ -310,6 +311,7 @@ lemma trace_comp_eq_mul_of_commute_of_isNilpotent [IsReduced R] {f g : Module.En
   have : f ∘ₗ algebraMap R _ μ = μ • f := by ext; simp -- TODO Surely exists?
   rw [hμ, comp_add, map_add, hg, add_zero, this, LinearMap.map_smul, smul_eq_mul]
 
+-- This result requires `Mathlib.RingTheory.TensorProduct.Free`. Maybe it should move elsewhere?
 @[simp]
 lemma trace_baseChange [Module.Free R M] [Module.Finite R M]
     (f : M →ₗ[R] M) (A : Type*) [CommRing A] [Algebra R A] :

Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Category.ModuleCat.Projective
 import Mathlib.AlgebraicTopology.ExtraDegeneracy
 import Mathlib.CategoryTheory.Abelian.Ext
 import Mathlib.RepresentationTheory.Rep
+import Mathlib.RingTheory.TensorProduct.Free
 
 /-!
 # The structure of the `k[G]`-module `k[Gⁿ]`

Mathlib/RingTheory/LinearDisjoint.lean

@@ -3,15 +3,15 @@ Copyright (c) 2024 Jz Pan. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jz Pan
 -/
-import Mathlib.LinearAlgebra.LinearDisjoint
-import Mathlib.LinearAlgebra.TensorProduct.Subalgebra
-import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
-import Mathlib.LinearAlgebra.FreeModule.StrongRankCondition
-import Mathlib.LinearAlgebra.Basis.VectorSpace
 import Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
 import Mathlib.Algebra.Algebra.Subalgebra.Rank
+import Mathlib.LinearAlgebra.Basis.VectorSpace
+import Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
+import Mathlib.LinearAlgebra.LinearDisjoint
+import Mathlib.LinearAlgebra.TensorProduct.Subalgebra
 import Mathlib.RingTheory.IntegralClosure.Algebra.Defs
 import Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
+import Mathlib.RingTheory.TensorProduct.Finite
 
 /-!
 

Mathlib/RingTheory/LocalRing/Module.lean

@@ -3,13 +3,13 @@ Copyright (c) 2024 Andrew Yang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Andrew Yang
 -/
-import Mathlib.RingTheory.FiniteType
-import Mathlib.RingTheory.Nakayama
 import Mathlib.Algebra.Module.FinitePresentation
 import Mathlib.LinearAlgebra.FiniteDimensional
-import Mathlib.LinearAlgebra.TensorProduct.RightExactness
+import Mathlib.RingTheory.FiniteType
 import Mathlib.RingTheory.Flat.Basic
 import Mathlib.RingTheory.LocalRing.ResidueField.Basic
+import Mathlib.RingTheory.Nakayama
+import Mathlib.RingTheory.TensorProduct.Free
 
 /-!
 # Finite modules over local rings

Mathlib/RingTheory/Localization/BaseChange.lean

@@ -5,6 +5,7 @@ Authors: Andrew Yang, Jujian Zhang
 -/
 import Mathlib.RingTheory.IsTensorProduct
 import Mathlib.RingTheory.Localization.Module
+import Mathlib.LinearAlgebra.DirectSum.Finsupp
 
 /-!
 # Localized Module

Mathlib/RingTheory/QuotSMulTop.lean

@@ -5,6 +5,7 @@ Authors: Brendan Murphy
 -/
 import Mathlib.LinearAlgebra.TensorProduct.RightExactness
 import Mathlib.LinearAlgebra.TensorProduct.Quotient
+import Mathlib.LinearAlgebra.DFinsupp
 
 /-!
 # Reducing a module modulo an element of the ring

Mathlib/RingTheory/TensorProduct/Basic.lean

@@ -3,11 +3,10 @@ Copyright (c) 2020 Kim Morrison. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kim Morrison, Johan Commelin
 -/
+import Mathlib.Algebra.Algebra.RestrictScalars
 import Mathlib.GroupTheory.MonoidLocalization.Basic
-import Mathlib.LinearAlgebra.FreeModule.Basic
-import Mathlib.LinearAlgebra.Matrix.ToLin
+import Mathlib.LinearAlgebra.TensorProduct.Tower
 import Mathlib.RingTheory.Adjoin.Basic
-import Mathlib.RingTheory.Finiteness
 
 /-!
 # The tensor product of R-algebras
@@ -1092,89 +1091,6 @@ theorem productMap_range : (productMap f g).range = f.range ⊔ g.range := by
 
 end
 
-section Basis
-
-universe uM uι
-variable {M : Type uM} {ι : Type uι}
-variable [CommSemiring R] [Semiring A] [Algebra R A]
-variable [AddCommMonoid M] [Module R M] (b : Basis ι R M)
-variable (A)
-
-/-- Given an `R`-algebra `A` and an `R`-basis of `M`, this is an `R`-linear isomorphism
-`A ⊗[R] M ≃ (ι →₀ A)` (which is in fact `A`-linear). -/
-noncomputable def basisAux : A ⊗[R] M ≃ₗ[R] ι →₀ A :=
-  _root_.TensorProduct.congr (Finsupp.LinearEquiv.finsuppUnique R A PUnit.{uι+1}).symm b.repr ≪≫ₗ
-    (finsuppTensorFinsupp R R A R PUnit ι).trans
-      (Finsupp.lcongr (Equiv.uniqueProd ι PUnit) (_root_.TensorProduct.rid R A))
-
-variable {A}
-
-theorem basisAux_tmul (a : A) (m : M) :
-    basisAux A b (a ⊗ₜ m) = a • Finsupp.mapRange (algebraMap R A) (map_zero _) (b.repr m) := by
-  ext
-  simp [basisAux, ← Algebra.commutes, Algebra.smul_def]
-
-theorem basisAux_map_smul (a : A) (x : A ⊗[R] M) : basisAux A b (a • x) = a • basisAux A b x :=
-  TensorProduct.induction_on x (by simp)
-    (fun x y => by simp only [TensorProduct.smul_tmul', basisAux_tmul, smul_assoc])
-    fun x y hx hy => by simp [hx, hy]
-
-variable (A)
-
-/-- Given a `R`-algebra `A`, this is the `A`-basis of `A ⊗[R] M` induced by a `R`-basis of `M`. -/
-noncomputable def basis : Basis ι A (A ⊗[R] M) where
-  repr := { basisAux A b with map_smul' := basisAux_map_smul b }
-
-variable {A}
-
-@[simp]
-theorem basis_repr_tmul (a : A) (m : M) :
-    (basis A b).repr (a ⊗ₜ m) = a • Finsupp.mapRange (algebraMap R A) (map_zero _) (b.repr m) :=
-  basisAux_tmul b a m -- Porting note: Lean 3 had _ _ _
-
-theorem basis_repr_symm_apply (a : A) (i : ι) :
-    (basis A b).repr.symm (Finsupp.single i a) = a ⊗ₜ b.repr.symm (Finsupp.single i 1) := by
-  rw [basis, LinearEquiv.coe_symm_mk] -- Porting note: `coe_symm_mk` isn't firing in `simp`
-  simp [Equiv.uniqueProd_symm_apply, basisAux]
-
-@[simp]
-theorem basis_apply (i : ι) : basis A b i = 1 ⊗ₜ b i := basis_repr_symm_apply b 1 i
-
-theorem basis_repr_symm_apply' (a : A) (i : ι) : a • basis A b i = a ⊗ₜ b i := by
-  simpa using basis_repr_symm_apply b a i
-
-section baseChange
-
-open LinearMap
-
-variable [Fintype ι]
-variable {ι' N : Type*} [Fintype ι'] [DecidableEq ι'] [AddCommMonoid N] [Module R N]
-variable (A : Type*) [CommSemiring A] [Algebra R A]
-
-lemma _root_.Basis.baseChange_linearMap (b : Basis ι R M) (b' : Basis ι' R N) (ij : ι × ι') :
-    baseChange A (b'.linearMap b ij) = (basis A b').linearMap (basis A b) ij := by
-  apply (basis A b').ext
-  intro k
-  conv_lhs => simp only [basis_apply, baseChange_tmul]
-  simp_rw [Basis.linearMap_apply_apply, basis_apply]
-  split <;> simp only [TensorProduct.tmul_zero]
-
-variable [DecidableEq ι]
-
-lemma _root_.Basis.baseChange_end (b : Basis ι R M) (ij : ι × ι) :
-    baseChange A (b.end ij) = (basis A b).end ij :=
-  b.baseChange_linearMap A b ij
-
-end baseChange
-
-end Basis
-
-instance (R A M : Type*)
-    [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Free R M]
-    [CommSemiring A] [Algebra R A] :
-    Module.Free A (A ⊗[R] M) :=
-  Module.Free.of_basis <| Algebra.TensorProduct.basis A (Module.Free.chooseBasis R M)
-
 end TensorProduct
 
 end Algebra
@@ -1188,12 +1104,6 @@ variable {R M₁ M₂ ι ι₂ : Type*} (A : Type*)
   [CommSemiring R] [CommSemiring A] [Algebra R A]
   [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂]
 
-@[simp]
-lemma toMatrix_baseChange (f : M₁ →ₗ[R] M₂) (b₁ : Basis ι R M₁) (b₂ : Basis ι₂ R M₂) :
-    toMatrix (basis A b₁) (basis A b₂) (f.baseChange A) =
-    (toMatrix b₁ b₂ f).map (algebraMap R A) := by
-  ext; simp [toMatrix_apply]
-
 end LinearMap
 
 namespace LinearMap
@@ -1267,12 +1177,6 @@ theorem endTensorEndAlgHom_apply (f : End A M) (g : End R N) :
 
 end Module
 
-theorem Subalgebra.finite_sup {K L : Type*} [CommSemiring K] [CommSemiring L] [Algebra K L]
-    (E1 E2 : Subalgebra K L) [Module.Finite K E1] [Module.Finite K E2] :
-    Module.Finite K ↥(E1 ⊔ E2) := by
-  rw [← E1.range_val, ← E2.range_val, ← Algebra.TensorProduct.productMap_range]
-  exact Module.Finite.range (Algebra.TensorProduct.productMap E1.val E2.val).toLinearMap
-
 namespace TensorProduct.Algebra
 
 variable {R A B M : Type*}

Mathlib/RingTheory/TensorProduct/Finite.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2020 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Johan Commelin
+-/
+import Mathlib.RingTheory.Finiteness
+import Mathlib.RingTheory.TensorProduct.Basic
+
+/-!
+# Finiteness results related to tensor products
+
+In this file we show that the supremum of two subalgebras that are finitely generated as modules,
+is again finitely generated.
+
+-/
+
+theorem Subalgebra.finite_sup {K L : Type*} [CommSemiring K] [CommSemiring L] [Algebra K L]
+    (E1 E2 : Subalgebra K L) [Module.Finite K E1] [Module.Finite K E2] :
+    Module.Finite K ↥(E1 ⊔ E2) := by
+  rw [← E1.range_val, ← E2.range_val, ← Algebra.TensorProduct.productMap_range]
+  exact Module.Finite.range (Algebra.TensorProduct.productMap E1.val E2.val).toLinearMap

Mathlib/RingTheory/TensorProduct/Free.lean

@@ -0,0 +1,131 @@
+/-
+Copyright (c) 2020 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Johan Commelin
+-/
+import Mathlib.LinearAlgebra.FreeModule.Basic
+import Mathlib.LinearAlgebra.Matrix.ToLin
+import Mathlib.RingTheory.TensorProduct.Basic
+
+/-!
+# Results on bases of tensor products
+
+In the file we construct a basis for the base change of a module to an algebra,
+and deducde that `Module.Free` is stable under base change.
+
+## Main declarations
+
+- `Algebra.TensorProduct.basis`: given a basis of a module `M` over a commutative semiring `R`,
+  and an `R`-algebra `A`, this provides a basis for `A ⊗[R] M` over `A`.
+- `Algebra.TensorProduct.instFree`: if `M` is free, then so is `A ⊗[R] M`.
+
+-/
+
+suppress_compilation
+
+open scoped TensorProduct
+
+namespace Algebra
+
+namespace TensorProduct
+
+variable {R S A : Type*}
+
+section Basis
+
+universe uM uι
+variable {M : Type uM} {ι : Type uι}
+variable [CommSemiring R] [Semiring A] [Algebra R A]
+variable [AddCommMonoid M] [Module R M] (b : Basis ι R M)
+
+variable (A) in
+/-- Given an `R`-algebra `A` and an `R`-basis of `M`, this is an `R`-linear isomorphism
+`A ⊗[R] M ≃ (ι →₀ A)` (which is in fact `A`-linear). -/
+noncomputable def basisAux : A ⊗[R] M ≃ₗ[R] ι →₀ A :=
+  _root_.TensorProduct.congr (Finsupp.LinearEquiv.finsuppUnique R A PUnit.{uι+1}).symm b.repr ≪≫ₗ
+    (finsuppTensorFinsupp R R A R PUnit ι).trans
+      (Finsupp.lcongr (Equiv.uniqueProd ι PUnit) (_root_.TensorProduct.rid R A))
+
+theorem basisAux_tmul (a : A) (m : M) :
+    basisAux A b (a ⊗ₜ m) = a • Finsupp.mapRange (algebraMap R A) (map_zero _) (b.repr m) := by
+  ext
+  simp [basisAux, ← Algebra.commutes, Algebra.smul_def]
+
+theorem basisAux_map_smul (a : A) (x : A ⊗[R] M) : basisAux A b (a • x) = a • basisAux A b x :=
+  TensorProduct.induction_on x (by simp)
+    (fun x y => by simp only [TensorProduct.smul_tmul', basisAux_tmul, smul_assoc])
+    fun x y hx hy => by simp [hx, hy]
+
+variable (A) in
+/-- Given a `R`-algebra `A`, this is the `A`-basis of `A ⊗[R] M` induced by a `R`-basis of `M`. -/
+noncomputable def basis : Basis ι A (A ⊗[R] M) where
+  repr := { basisAux A b with map_smul' := basisAux_map_smul b }
+
+@[simp]
+theorem basis_repr_tmul (a : A) (m : M) :
+    (basis A b).repr (a ⊗ₜ m) = a • Finsupp.mapRange (algebraMap R A) (map_zero _) (b.repr m) :=
+  basisAux_tmul b a m -- Porting note: Lean 3 had _ _ _
+
+theorem basis_repr_symm_apply (a : A) (i : ι) :
+    (basis A b).repr.symm (Finsupp.single i a) = a ⊗ₜ b.repr.symm (Finsupp.single i 1) := by
+  rw [basis, LinearEquiv.coe_symm_mk] -- Porting note: `coe_symm_mk` isn't firing in `simp`
+  simp [Equiv.uniqueProd_symm_apply, basisAux]
+
+@[simp]
+theorem basis_apply (i : ι) : basis A b i = 1 ⊗ₜ b i := basis_repr_symm_apply b 1 i
+
+theorem basis_repr_symm_apply' (a : A) (i : ι) : a • basis A b i = a ⊗ₜ b i := by
+  simpa using basis_repr_symm_apply b a i
+
+section baseChange
+
+open LinearMap
+
+variable [Fintype ι]
+variable {ι' N : Type*} [Fintype ι'] [DecidableEq ι'] [AddCommMonoid N] [Module R N]
+variable (A : Type*) [CommSemiring A] [Algebra R A]
+
+lemma _root_.Basis.baseChange_linearMap (b : Basis ι R M) (b' : Basis ι' R N) (ij : ι × ι') :
+    baseChange A (b'.linearMap b ij) = (basis A b').linearMap (basis A b) ij := by
+  apply (basis A b').ext
+  intro k
+  conv_lhs => simp only [basis_apply, baseChange_tmul]
+  simp_rw [Basis.linearMap_apply_apply, basis_apply]
+  split <;> simp only [TensorProduct.tmul_zero]
+
+variable [DecidableEq ι]
+
+lemma _root_.Basis.baseChange_end (b : Basis ι R M) (ij : ι × ι) :
+    baseChange A (b.end ij) = (basis A b).end ij :=
+  b.baseChange_linearMap A b ij
+
+end baseChange
+
+end Basis
+
+instance instFree (R A M : Type*)
+    [CommSemiring R] [AddCommMonoid M] [Module R M] [Module.Free R M]
+    [CommSemiring A] [Algebra R A] :
+    Module.Free A (A ⊗[R] M) :=
+  Module.Free.of_basis <| Algebra.TensorProduct.basis A (Module.Free.chooseBasis R M)
+
+end TensorProduct
+
+end Algebra
+
+namespace LinearMap
+
+open Algebra.TensorProduct
+
+variable {R M₁ M₂ ι ι₂ : Type*} (A : Type*)
+  [Fintype ι] [Finite ι₂] [DecidableEq ι]
+  [CommSemiring R] [CommSemiring A] [Algebra R A]
+  [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂]
+
+@[simp]
+lemma toMatrix_baseChange (f : M₁ →ₗ[R] M₂) (b₁ : Basis ι R M₁) (b₂ : Basis ι₂ R M₂) :
+    toMatrix (basis A b₁) (basis A b₂) (f.baseChange A) =
+    (toMatrix b₁ b₂ f).map (algebraMap R A) := by
+  ext; simp [toMatrix_apply]
+
+end LinearMap