feat: use suppress_compilation in tensor products (#7504)

More principled version of #7281.
leanprover-community · Oct 11, 2023 · 9ff5b6f · 9ff5b6f
1 parent fbb3ffb
commit 9ff5b6f
Show file tree

Hide file tree

Showing 35 changed files with 113 additions and 11 deletions.
diff --git a/Mathlib/Algebra/Algebra/Bilinear.lean b/Mathlib/Algebra/Algebra/Bilinear.lean
@@ -18,7 +18,6 @@ in order to avoid importing `LinearAlgebra.BilinearMap` and
 `LinearAlgebra.TensorProduct` unnecessarily.
 -/
 
-
 open TensorProduct Module
 
 namespace LinearMap
@@ -36,7 +35,7 @@ def mul : A →ₗ[R] A →ₗ[R] A :=
 #align linear_map.mul LinearMap.mul
 
 /-- The multiplication map on a non-unital algebra, as an `R`-linear map from `A ⊗[R] A` to `A`. -/
-def mul' : A ⊗[R] A →ₗ[R] A :=
+noncomputable def mul' : A ⊗[R] A →ₗ[R] A :=
   TensorProduct.lift (mul R A)
 #align linear_map.mul' LinearMap.mul'
 

diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -40,6 +40,8 @@ Let `R, S` be rings and `f : R →+* S`
   `s ⊗ m : S ⊗[R, f] M`.
 -/
 
+suppress_compilation
+
 set_option linter.uppercaseLean3 false -- Porting note: Module
 
 open CategoryTheory

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
@@ -33,6 +33,8 @@ use this as an interface and not need to interact much with the implementation d
 -- Porting note: Module
 set_option linter.uppercaseLean3 false
 
+suppress_compilation
+
 universe v w x u
 
 open CategoryTheory

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Closed.lean
@@ -12,6 +12,7 @@ import Mathlib.Algebra.Category.ModuleCat.Monoidal.Symmetric
 # The monoidal closed structure on `Module R`.
 -/
 
+suppress_compilation
 
 universe v w x u
 

diff --git a/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean b/Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean
@@ -12,6 +12,7 @@ import Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
 # The symmetric monoidal structure on `Module R`.
 -/
 
+suppress_compilation
 
 universe v w x u
 

diff --git a/Mathlib/Algebra/Category/Ring/Constructions.lean b/Mathlib/Algebra/Category/Ring/Constructions.lean
@@ -24,6 +24,7 @@ In this file we provide the explicit (co)cones for various (co)limits in `CommRi
 
 -/
 
+suppress_compilation
 
 universe u u'
 

diff --git a/Mathlib/Algebra/Lie/BaseChange.lean b/Mathlib/Algebra/Lie/BaseChange.lean
@@ -24,6 +24,7 @@ Lie algebras have a well-behaved theory of extension and restriction of scalars.
 lie ring, lie algebra, extension of scalars, restriction of scalars, base change
 -/
 
+suppress_compilation
 
 universe u v w w₁ w₂ w₃
 

diff --git a/Mathlib/Algebra/Lie/TensorProduct.lean b/Mathlib/Algebra/Lie/TensorProduct.lean
@@ -17,6 +17,7 @@ Tensor products of Lie modules carry natural Lie module structures.
 lie module, tensor product, universal property
 -/
 
+suppress_compilation
 
 universe u v w w₁ w₂ w₃
 

diff --git a/Mathlib/Algebra/Lie/Weights.lean b/Mathlib/Algebra/Lie/Weights.lean
@@ -464,6 +464,8 @@ def rootSpaceWeightSpaceProductAux {χ₁ χ₂ χ₃ : H → R} (hχ : χ₁ +
       SetLike.mk_smul_mk]
 #align lie_algebra.root_space_weight_space_product_aux LieAlgebra.rootSpaceWeightSpaceProductAux
 
+suppress_compilation
+
 -- Porting note: this def is _really_ slow
 -- See https://github.com/leanprover-community/mathlib4/issues/5028
 /-- Given a nilpotent Lie subalgebra `H ⊆ L` together with `χ₁ χ₂ : H → R`, there is a natural

diff --git a/Mathlib/AlgebraicGeometry/Limits.lean b/Mathlib/AlgebraicGeometry/Limits.lean
@@ -24,6 +24,8 @@ We construct various limits and colimits in the category of schemes.
 
 -/
 
+suppress_compilation
+
 set_option linter.uppercaseLean3 false
 
 universe u

diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean
@@ -18,6 +18,8 @@ is equivalent to the category of "native" bundled `R`-algebras.
 Moreover, this equivalence is compatible with the forgetful functors to `ModuleCat R`.
 -/
 
+suppress_compilation
+
 set_option linter.uppercaseLean3 false
 
 universe v u

diff --git a/Mathlib/Data/Matrix/Kronecker.lean b/Mathlib/Data/Matrix/Kronecker.lean
@@ -427,6 +427,8 @@ open Matrix TensorProduct
 
 section Module
 
+suppress_compilation
+
 variable [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ]
 
 variable [Module R α] [Module R β] [Module R γ]

diff --git a/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean b/Mathlib/LinearAlgebra/Alternating/DomCoprod.lean
@@ -16,6 +16,8 @@ taking values in the tensor product of the codomains of the original maps.
 
 #align_import linear_algebra.alternating from "leanprover-community/mathlib"@"0c1d80f5a86b36c1db32e021e8d19ae7809d5b79"
 
+suppress_compilation
+
 open BigOperators TensorProduct
 
 variable {ιa ιb : Type*} [Fintype ιa] [Fintype ιb]

diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean
@@ -21,6 +21,7 @@ import Mathlib.LinearAlgebra.TensorProduct.Tower
 
 -/
 
+suppress_compilation
 
 universe u v w uι uR uA uM₁ uM₂
 

diff --git a/Mathlib/LinearAlgebra/Contraction.lean b/Mathlib/LinearAlgebra/Contraction.lean
@@ -20,6 +20,8 @@ some basic properties of these maps.
 contraction, dual module, tensor product
 -/
 
+suppress_compilation
+
 -- Porting note: universe metavariables behave oddly
 universe w u v₁ v₂ v₃ v₄
 

diff --git a/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean b/Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
@@ -19,6 +19,8 @@ This file shows that taking `TensorProduct`s commutes with taking `DirectSum`s i
 * `TensorProduct.directSumRight`
 -/
 
+suppress_compilation
+
 universe u v₁ v₂ w₁ w₁' w₂ w₂'
 
 section Ring

diff --git a/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean b/Mathlib/LinearAlgebra/Multilinear/TensorProduct.lean
@@ -12,6 +12,7 @@ import Mathlib.LinearAlgebra.TensorProduct
 # Constructions relating multilinear maps and tensor products.
 -/
 
+suppress_compilation
 
 namespace MultilinearMap
 

diff --git a/Mathlib/LinearAlgebra/PiTensorProduct.lean b/Mathlib/LinearAlgebra/PiTensorProduct.lean
@@ -62,6 +62,7 @@ binary tensor product in `LinearAlgebra/TensorProduct.lean`.
 multilinear, tensor, tensor product
 -/
 
+suppress_compilation
 
 open Function
 
@@ -112,6 +113,7 @@ def PiTensorProduct : Type _ :=
 
 variable {R}
 
+unsuppress_compilation in
 -- This enables the notation `⨂[R] i : ι, s i` for the pi tensor product, given `s : ι → Type*`.
 --scoped[TensorProduct] -- Porting note: `scoped` caused an error, so I commented it out.
 /-- notation for tensor product over some indexed type -/
@@ -307,6 +309,7 @@ def tprod : MultilinearMap R s (⨂[R] i, s i) where
 
 variable {R}
 
+unsuppress_compilation in
 /-- pure tensor in tensor product over some index type -/
 -- Porting note: use `FunLike.coe` as an explicit coercion to help `notation3` pretty print,
 -- was just `tprod R f`.

diff --git a/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean b/Mathlib/LinearAlgebra/QuadraticForm/TensorProduct/Isometries.lean
@@ -20,6 +20,8 @@ These results are separate from the definition of `QuadraticForm.tmul` as that f
 * `QuadraticForm.tensorLId`: `TensorProduct.lid` as a `QuadraticForm.IsometryEquiv`
 -/
 
+suppress_compilation
+
 universe uR uM₁ uM₂ uM₃ uM₄
 variable {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} {M₃ : Type uM₃} {M₄ : Type uM₄}
 

diff --git a/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean b/Mathlib/LinearAlgebra/TensorAlgebra/ToTensorPower.lean
@@ -15,6 +15,7 @@ In this file we show that `TensorAlgebra R M` is isomorphic to a direct sum of t
 `TensorAlgebra.equivDirectSum`.
 -/
 
+suppress_compilation
 
 open scoped DirectSum TensorProduct
 

diff --git a/Mathlib/LinearAlgebra/TensorPower.lean b/Mathlib/LinearAlgebra/TensorPower.lean
@@ -29,6 +29,7 @@ In this file we use `ₜ1` and `ₜ*` as local notation for the graded multiplic
 tensor powers. Elsewhere, using `1` and `*` on `GradedMonoid` should be preferred.
 -/
 
+suppress_compilation
 
 open scoped TensorProduct
 

diff --git a/Mathlib/LinearAlgebra/TensorProduct.lean b/Mathlib/LinearAlgebra/TensorProduct.lean
@@ -5,6 +5,7 @@ Authors: Kenny Lau, Mario Carneiro
 -/
 import Mathlib.GroupTheory.Congruence
 import Mathlib.Algebra.Module.Submodule.Bilinear
+import Mathlib.Tactic.SuppressCompilation
 
 #align_import linear_algebra.tensor_product from "leanprover-community/mathlib"@"88fcdc3da43943f5b01925deddaa5bf0c0e85e4e"
 
@@ -33,6 +34,7 @@ as `m ⊗ₜ n` and `m ⊗ₜ[R] n` for `TensorProduct.tmul R m n`.
 bilinear, tensor, tensor product
 -/
 
+suppress_compilation
 
 section Semiring
 

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Opposite.lean b/Mathlib/LinearAlgebra/TensorProduct/Opposite.lean
@@ -13,6 +13,8 @@ The main result in this file is:
 * `Algebra.TensorProduct.opAlgEquiv R S A B : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₐ[S] (A ⊗[R] B)ᵐᵒᵖ`
 -/
 
+suppress_compilation
+
 open scoped TensorProduct
 
 variable (R S A B : Type*)

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Prod.lean b/Mathlib/LinearAlgebra/TensorProduct/Prod.lean
@@ -20,6 +20,8 @@ This file shows that taking `TensorProduct`s commutes with taking `Prod`s in bot
 universe uR uM₁ uM₂ uM₃
 variable (R : Type uR) (M₁ : Type uM₁) (M₂ : Type uM₂) (M₃ : Type uM₃)
 
+suppress_compilation
+
 namespace TensorProduct
 
 variable [CommSemiring R] [AddCommMonoid M₁] [AddCommMonoid M₂] [AddCommMonoid M₃]

diff --git a/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean b/Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
@@ -9,10 +9,10 @@ import Mathlib.RingTheory.TensorProduct
 
 /-! # Right-exactness properties of tensor product
 
-* `TensorProduct.rTensor.surjective` asserts that one on tensors
+* `TensorProduct.rTensor.surjective` asserts that one tensors
   a surjective map on the right, one still gets a surjective linear map.
 
-* `TensorProduct.lTensor.surjective` asserts that one on tensors
+* `TensorProduct.lTensor.surjective` asserts that one tensors
   a surjective map on the left, one still gets a surjective linear map.
 
 * `TensorProduct.rTensor_exact` says that when one tensors a short exact
@@ -49,6 +49,7 @@ The proofs are those of [bourbaki1989] (chap. 2, §3, n°6)
 * Treat algebras (further PR)
 -/
 
+suppress_compilation
 
 section Modules
 

diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean
@@ -45,6 +45,8 @@ probably should still implement the less general ones as abbreviations to the mo
 fewer type arguments.
 -/
 
+suppress_compilation
+
 namespace TensorProduct
 
 namespace AlgebraTensorModule

diff --git a/Mathlib/RepresentationTheory/Basic.lean b/Mathlib/RepresentationTheory/Basic.lean
@@ -356,7 +356,7 @@ open TensorProduct
 /-- Given representations of `G` on `V` and `W`, there is a natural representation of `G` on their
 tensor product `V ⊗[k] W`.
 -/
-def tprod : Representation k G (V ⊗[k] W) where
+noncomputable def tprod : Representation k G (V ⊗[k] W) where
   toFun g := TensorProduct.map (ρV g) (ρW g)
   map_one' := by simp only [_root_.map_one, TensorProduct.map_one]
   map_mul' g h := by simp only [_root_.map_mul, TensorProduct.map_mul]

diff --git a/Mathlib/RepresentationTheory/FdRep.lean b/Mathlib/RepresentationTheory/FdRep.lean
@@ -34,6 +34,7 @@ We verify that `FdRep k G` is a `k`-linear monoidal category, and rigid when `G`
 
 -/
 
+suppress_compilation
 
 universe u
 

diff --git a/Mathlib/RepresentationTheory/Invariants.lean b/Mathlib/RepresentationTheory/Invariants.lean
@@ -20,6 +20,7 @@ In order for the definition of the average element to make sense, we need to ass
 results that the order of `G` is invertible in `k` (e. g. `k` has characteristic `0`).
 -/
 
+suppress_compilation
 
 open scoped BigOperators
 

diff --git a/Mathlib/RepresentationTheory/Rep.lean b/Mathlib/RepresentationTheory/Rep.lean
@@ -26,6 +26,7 @@ We construct the categorical equivalence `Rep k G ≌ ModuleCat (MonoidAlgebra k
 We verify that `Rep k G` is a `k`-linear abelian symmetric monoidal category with all (co)limits.
 -/
 
+suppress_compilation
 
 universe u
 

diff --git a/Mathlib/RingTheory/Finiteness.lean b/Mathlib/RingTheory/Finiteness.lean
@@ -638,8 +638,9 @@ end Finite
 end Module
 
 /-- Porting note: reminding Lean about this instance for Module.Finite.base_change -/
-local instance [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] :
-  Module A (TensorProduct R A M) :=
+noncomputable local instance
+    [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] :
+    Module A (TensorProduct R A M) :=
   haveI : SMulCommClass R A A := IsScalarTower.to_smulCommClass
   TensorProduct.leftModule
 

diff --git a/Mathlib/RingTheory/Kaehler.lean b/Mathlib/RingTheory/Kaehler.lean
@@ -34,6 +34,8 @@ import Mathlib.RingTheory.IsTensorProduct
 - Define the `IsKaehlerDifferential` predicate.
 -/
 
+suppress_compilation
+
 section KaehlerDifferential
 
 open scoped TensorProduct
@@ -477,6 +479,7 @@ noncomputable def KaehlerDifferential.kerTotal : Submodule S (S →₀ S) :=
       Set.range fun x : R => single (algebraMap R S x) 1)
 #align kaehler_differential.ker_total KaehlerDifferential.kerTotal
 
+unsuppress_compilation in
 -- Porting note: was `local notation x "𝖣" y => (KaehlerDifferential.kerTotal R S).mkQ (single y x)`
 -- but `notation3` wants an explicit expansion to be able to generate a pretty printer.
 local notation3 x "𝖣" y =>
@@ -590,6 +593,7 @@ variable (A B : Type*) [CommRing A] [CommRing B] [Algebra R A] [Algebra S B] [Al
 
 variable [Algebra A B] [IsScalarTower R S B] [IsScalarTower R A B]
 
+unsuppress_compilation in
 -- The map `(A →₀ A) →ₗ[A] (B →₀ B)`
 local macro "finsupp_map" : term =>
   `((Finsupp.mapRange.linearMap (Algebra.linearMap A B)).comp

diff --git a/Mathlib/RingTheory/MatrixAlgebra.lean b/Mathlib/RingTheory/MatrixAlgebra.lean
@@ -12,6 +12,7 @@ import Mathlib.RingTheory.TensorProduct
 We show `Matrix n n A ≃ₐ[R] (A ⊗[R] Matrix n n R)`.
 -/
 
+suppress_compilation
 
 universe u v w
 

diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean
@@ -36,6 +36,8 @@ multiplication is characterized by `(a₁ ⊗ₜ b₁) * (a₂ ⊗ₜ b₂) = (a
 
 -/
 
+suppress_compilation
+
 open scoped TensorProduct
 
 open TensorProduct