From 02508fd189adbefcdb7313a007e82fb779ab2700 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 20 Jul 2023 19:54:35 +0000 Subject: [PATCH 01/14] feat: heterogenize TensorProduct.congr and friends --- Mathlib/RingTheory/TensorProduct.lean | 59 ++++++++++++++++++++++++++- 1 file changed, 57 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index cfcd0102c24aa0..5e394b0d049779 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -36,7 +36,10 @@ The heterobasic definitions below such as: * `TensorProduct.AlgebraTensorModule.lift` * `TensorProduct.AlgebraTensorModule.lift.equiv` * `TensorProduct.AlgebraTensorModule.mk` + * `TensorProduct.AlgebraTensorModule.map` + * `TensorProduct.AlgebraTensorModule.congr` * `TensorProduct.AlgebraTensorModule.assoc` + * `TensorProduct.AlgebraTensorModule.left_comm` are just more general versions of the definitions already in `LinearAlgebra/TensorProduct`. We could thus consider replacing the less general definitions with these ones. If we do this, we @@ -53,7 +56,7 @@ open TensorProduct namespace TensorProduct -variable {R A M N P : Type _} +variable {R A M N P Q : Type _} /-! ### The `A`-module structure on `A ⊗[R] M` @@ -76,6 +79,8 @@ variable [AddCommMonoid N] [Module R N] variable [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] +variable [AddCommMonoid Q] [Module R Q] + theorem smul_eq_lsmul_rTensor (a : A) (x : M ⊗[R] N) : a • x = (lsmul R M a).rTensor N x := rfl #align tensor_product.algebra_tensor_module.smul_eq_lsmul_rtensor TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor @@ -124,6 +129,8 @@ variable [AddCommMonoid N] [Module R N] variable [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] +variable [AddCommMonoid Q] [Module R Q] + /-- Heterobasic version of `TensorProduct.lift`: Constructing a linear map `M ⊗[R] N →[A] P` given a bilinear map `M →[A] N →[R] P` with the @@ -154,7 +161,7 @@ theorem lift_tmul (f : M →ₗ[A] N →ₗ[R] P) (x : M) (y : N) : lift f (x rfl #align tensor_product.algebra_tensor_module.lift_tmul TensorProduct.AlgebraTensorModule.lift_tmul -variable (R A M N P) +variable (R A M N P Q) /-- Heterobasic version of `TensorProduct.uncurry`: @@ -199,6 +206,35 @@ nonrec def mk : M →ₗ[A] N →ₗ[R] M ⊗[R] N := #align tensor_product.algebra_tensor_module.mk TensorProduct.AlgebraTensorModule.mk #align tensor_product.algebra_tensor_module.mk_apply TensorProduct.AlgebraTensorModule.mk_apply +variable {R A M N P Q} + +/-- Heterobasic version of `TensorProduct.map` -/ +def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] Q := + lift $ (show (Q →ₗ[R] P ⊗ Q) →ₗ[A] N →ₗ[R] P ⊗[R] Q from + { toFun := fun h => h ∘ₗ g, + map_add' := fun h₁ h₂ => LinearMap.add_comp g h₂ h₁, + map_smul' := fun c h => LinearMap.smul_comp c h g }) ∘ₗ mk R A P Q ∘ₗ f + +@[simp] theorem map_tmul (f : M →ₗ[A] P) (g : N →ₗ[R] Q) (m : M) (n : N) : + map f g (m ⊗ₜ n) = f m ⊗ₜ g n := + rfl + +/-- Heterobasic version of `TensorProduct.congr` -/ +def congr (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) : (M ⊗[R] N) ≃ₗ[A] (P ⊗[R] Q) := + LinearEquiv.ofLinear (map f g) (map f.symm g.symm) + (ext fun m n => by simp) + (ext fun m n => by simp) + +@[simp] theorem congr_tmul (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) : + congr f g (m ⊗ₜ n) = f m ⊗ₜ g n := + rfl + +@[simp] theorem congr_symm_tmul (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) (p : P) (q : Q) : + (congr f g).symm (p ⊗ₜ q) = f.symm p ⊗ₜ g.symm q := + rfl + +variable (R A M N P Q) + attribute [local ext high] TensorProduct.ext /-- Heterobasic version of `TensorProduct.assoc`: @@ -221,6 +257,25 @@ def assoc : (M ⊗[A] P) ⊗[R] N ≃ₗ[A] M ⊗[A] P ⊗[R] N := rfl) #align tensor_product.algebra_tensor_module.assoc TensorProduct.AlgebraTensorModule.assoc +/-- Heterobasic version of `TensorProduct.leftComm` -/ +def leftComm : M ⊗[A] (P ⊗[R] Q) ≃ₗ[A] P ⊗[A] (M ⊗[R] Q) := + let e₁ := (assoc R A M Q P).symm + let e₂ := congr (TensorProduct.comm A M P) (1 : Q ≃ₗ[R] Q) + let e₃ := (assoc R A P Q M) + e₁ ≪≫ₗ (e₂ ≪≫ₗ e₃) + +variable {M N P Q} + +@[simp] +theorem leftComm_tmul (m : M) (p : P) (q : Q) : + leftComm R A M P Q (m ⊗ₜ (p ⊗ₜ q)) = p ⊗ₜ (m ⊗ₜ q) := + rfl + +@[simp] +theorem leftComm_symm_tmul (m : M) (p : P) (q : Q): + (leftComm R A M P Q).symm (p ⊗ₜ (m ⊗ₜ q)) = m ⊗ₜ (p ⊗ₜ q) := + rfl + end CommSemiring end AlgebraTensorModule From 187f03fd895d8e1f0bf0590a4c8fe3c2736d58d8 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 21 Jul 2023 09:55:42 +0000 Subject: [PATCH 02/14] more --- Mathlib/RingTheory/TensorProduct.lean | 125 ++++++++++++++++++-------- 1 file changed, 88 insertions(+), 37 deletions(-) diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index 5e394b0d049779..fe2b1ae1c2bce0 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -37,6 +37,7 @@ The heterobasic definitions below such as: * `TensorProduct.AlgebraTensorModule.lift.equiv` * `TensorProduct.AlgebraTensorModule.mk` * `TensorProduct.AlgebraTensorModule.map` + * `TensorProduct.AlgebraTensorModule.map_bilinear` * `TensorProduct.AlgebraTensorModule.congr` * `TensorProduct.AlgebraTensorModule.assoc` * `TensorProduct.AlgebraTensorModule.left_comm` @@ -56,7 +57,7 @@ open TensorProduct namespace TensorProduct -variable {R A M N P Q : Type _} +variable {R A B M N P Q : Type _} /-! ### The `A`-module structure on `A ⊗[R] M` @@ -71,13 +72,15 @@ namespace AlgebraTensorModule section Semiring -variable [CommSemiring R] [Semiring A] [Algebra R A] +variable [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] -variable [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] +variable [AddCommMonoid M] [Module R M] [Module A M] [Module B M] +variable [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] variable [AddCommMonoid N] [Module R N] -variable [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] +variable [AddCommMonoid P] [Module R P] [Module A P] [Module B P] +variable [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] variable [AddCommMonoid Q] [Module R Q] @@ -117,20 +120,6 @@ theorem ext {g h : M ⊗[R] N →ₗ[A] P} (H : ∀ x y, g (x ⊗ₜ y) = h (x curry_injective <| LinearMap.ext₂ H #align tensor_product.algebra_tensor_module.ext TensorProduct.AlgebraTensorModule.ext -end Semiring - -section CommSemiring - -variable [CommSemiring R] [CommSemiring A] [Algebra R A] - -variable [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] - -variable [AddCommMonoid N] [Module R N] - -variable [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] - -variable [AddCommMonoid Q] [Module R Q] - /-- Heterobasic version of `TensorProduct.lift`: Constructing a linear map `M ⊗[R] N →[A] P` given a bilinear map `M →[A] N →[R] P` with the @@ -161,7 +150,7 @@ theorem lift_tmul (f : M →ₗ[A] N →ₗ[R] P) (x : M) (y : N) : lift f (x rfl #align tensor_product.algebra_tensor_module.lift_tmul TensorProduct.AlgebraTensorModule.lift_tmul -variable (R A M N P Q) +variable (R A B M N P Q) /-- Heterobasic version of `TensorProduct.uncurry`: @@ -169,33 +158,36 @@ Linearly constructing a linear map `M ⊗[R] N →[A] P` given a bilinear map `M with the property that its composition with the canonical bilinear map `M →[A] N →[R] M ⊗[R] N` is the given bilinear map `M →[A] N →[R] P`. -/ @[simps] -def uncurry : (M →ₗ[A] N →ₗ[R] P) →ₗ[A] M ⊗[R] N →ₗ[A] P where +def uncurry : (M →ₗ[A] N →ₗ[R] P) →ₗ[B] M ⊗[R] N →ₗ[A] P where toFun := lift map_add' _ _ := ext fun x y => by simp only [lift_tmul, add_apply] map_smul' _ _ := ext fun x y => by simp only [lift_tmul, smul_apply, RingHom.id_apply] -#align tensor_product.algebra_tensor_module.uncurry TensorProduct.AlgebraTensorModule.uncurry +-- porting note: new `B` argument +#align tensor_product.algebra_tensor_module.uncurry TensorProduct.AlgebraTensorModule.uncurryₓ /-- Heterobasic version of `TensorProduct.lcurry`: Given a linear map `M ⊗[R] N →[A] P`, compose it with the canonical bilinear map `M →[A] N →[R] M ⊗[R] N` to form a bilinear map `M →[A] N →[R] P`. -/ @[simps] -def lcurry : (M ⊗[R] N →ₗ[A] P) →ₗ[A] M →ₗ[A] N →ₗ[R] P where +def lcurry : (M ⊗[R] N →ₗ[A] P) →ₗ[B] M →ₗ[A] N →ₗ[R] P where toFun := curry map_add' _ _ := rfl map_smul' _ _ := rfl -#align tensor_product.algebra_tensor_module.lcurry TensorProduct.AlgebraTensorModule.lcurry +-- porting note: new `B` argument +#align tensor_product.algebra_tensor_module.lcurry TensorProduct.AlgebraTensorModule.lcurryₓ /-- Heterobasic version of `TensorProduct.lift.equiv`: A linear equivalence constructing a linear map `M ⊗[R] N →[A] P` given a bilinear map `M →[A] N →[R] P` with the property that its composition with the canonical bilinear map `M →[A] N →[R] M ⊗[R] N` is the given bilinear map `M →[A] N →[R] P`. -/ -def lift.equiv : (M →ₗ[A] N →ₗ[R] P) ≃ₗ[A] M ⊗[R] N →ₗ[A] P := - LinearEquiv.ofLinear (uncurry R A M N P) (lcurry R A M N P) +def lift.equiv : (M →ₗ[A] N →ₗ[R] P) ≃ₗ[B] M ⊗[R] N →ₗ[A] P := + LinearEquiv.ofLinear (uncurry R A B M N P) (lcurry R A B M N P) (LinearMap.ext fun _ => ext fun x y => lift_tmul _ x y) (LinearMap.ext fun f => LinearMap.ext fun x => LinearMap.ext fun y => lift_tmul f x y) -#align tensor_product.algebra_tensor_module.lift.equiv TensorProduct.AlgebraTensorModule.lift.equiv +-- porting note: new `B` argument +#align tensor_product.algebra_tensor_module.lift.equiv TensorProduct.AlgebraTensorModule.lift.equivₓ /-- Heterobasic version of `TensorProduct.mk`: @@ -219,6 +211,16 @@ def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] map f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl +theorem map_add_left (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (f₁ + f₂) g = map f₁ g + map f₂ g := by + ext + simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul, + add_apply, add_tmul] + +theorem map_add_right (f : M →ₗ[A] P) (g₁ g₂ : N →ₗ[R] Q) : map f (g₁ + g₂) = map f g₁ + map f g₂ := by + ext + simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul, + add_apply, tmul_add] + /-- Heterobasic version of `TensorProduct.congr` -/ def congr (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) : (M ⊗[R] N) ≃ₗ[A] (P ⊗[R] Q) := LinearEquiv.ofLinear (map f g) (map f.symm g.symm) @@ -233,6 +235,62 @@ def congr (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) : (M ⊗[R] N) ≃ₗ[A] (P (congr f g).symm (p ⊗ₜ q) = f.symm p ⊗ₜ g.symm q := rfl +theorem map_smul_right (r : R) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : map f (r • g) = r • map f g := by + ext + simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul, + smul_apply, tmul_smul] + +end Semiring + +section CommSemiring + +variable [CommSemiring R] [CommSemiring A] [CommSemiring B] [Algebra R A] [Algebra R B] + +variable [AddCommMonoid M] [Module R M] [Module A M] [Module B M] +variable [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] + +variable [AddCommMonoid N] [Module R N] + +variable [AddCommMonoid P] [Module R P] [Module A P] [Module B P] +variable [IsScalarTower R A P] [IsScalarTower R B P] [SMulCommClass A B P] + +variable [AddCommMonoid Q] [Module R Q] + +-- TODO: generalize with https://github.com/leanprover-community/mathlib/pull/19143 +theorem map_smul_left (r : A) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (r • f) g = r • map f g := by + ext + simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul, + smul_apply, smul_tmul'] + +variable (R A M N P Q) + +/-- Heterobasic version of `TensorProduct.map_bilinear` -/ +def mapBilinear : (M →ₗ[A] P) →ₗ[A] (N →ₗ[R] Q) →ₗ[R] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) := + { toFun := fun f => + { toFun := fun g => map f g + map_add' := fun _g₁ _g₂ => map_add_right _ _ _ + map_smul' := fun _c _g => map_smul_right _ _ _ } + map_add' := fun _f₁ _f₂ => LinearMap.ext <| fun _g => map_add_left _ _ _ + map_smul' := fun _c _f => LinearMap.ext <| fun _g => map_smul_left _ _ _ } + +variable {R A M N P Q} + +@[simp] +theorem mapBilinear_apply (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : mapBilinear R A M N P Q f g = map f g := + rfl + +variable (R A M N P Q) + +/- Heterobasic version of `TensorProduct.homTensorHomMap` -/ +def homTensorHomMap : ((M →ₗ[A] P) ⊗[R] (N →ₗ[R] Q)) →ₗ[A] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) := + lift <| mapBilinear R A M N P Q + +variable {R A M N P Q} + +@[simp] theorem homTensorHomMap_apply (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : + homTensorHomMap R A M N P Q (f ⊗ₜ g) = map f g := + rfl + variable (R A M N P Q) attribute [local ext high] TensorProduct.ext @@ -243,9 +301,9 @@ Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. def assoc : (M ⊗[A] P) ⊗[R] N ≃ₗ[A] M ⊗[A] P ⊗[R] N := LinearEquiv.ofLinear (lift <| - TensorProduct.uncurry A _ _ _ <| comp (lcurry R A _ _ _) <| TensorProduct.mk A M (P ⊗[R] N)) + TensorProduct.uncurry A _ _ _ <| comp (lcurry R A A _ _ _) <| TensorProduct.mk A M (P ⊗[R] N)) (TensorProduct.uncurry A _ _ _ <| - comp (uncurry R A _ _ _) <| by + comp (uncurry R A A _ _ _) <| by apply TensorProduct.curry exact mk R A _ _) (by @@ -304,15 +362,8 @@ variable (r : R) (f g : M →ₗ[R] N) variable (A) /-- `base_change A f` for `f : M →ₗ[R] N` is the `A`-linear map `A ⊗[R] M →ₗ[A] A ⊗[R] N`. -/ -def baseChange (f : M →ₗ[R] N) : A ⊗[R] M →ₗ[A] A ⊗[R] N where - toFun := f.lTensor A - map_add' := (f.lTensor A).map_add - map_smul' a x := - show - (f.lTensor A) (rTensor M (LinearMap.mul R A a) x) = - (rTensor N ((LinearMap.mul R A) a)) ((lTensor A f) x) by - rw [← comp_apply, ← comp_apply] - simp only [lTensor_comp_rTensor, rTensor_comp_lTensor] +def baseChange (f : M →ₗ[R] N) : A ⊗[R] M →ₗ[A] A ⊗[R] N := + AlgebraTensorModule.map (LinearMap.id : A →ₗ[A] A) f #align linear_map.base_change LinearMap.baseChange variable {A} From 30b1cbe74594333f74e8f64185534d349355989d Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 21 Jul 2023 09:58:19 +0000 Subject: [PATCH 03/14] docstrings --- Mathlib/RingTheory/TensorProduct.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index fe2b1ae1c2bce0..82c8492c704106 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -37,10 +37,12 @@ The heterobasic definitions below such as: * `TensorProduct.AlgebraTensorModule.lift.equiv` * `TensorProduct.AlgebraTensorModule.mk` * `TensorProduct.AlgebraTensorModule.map` - * `TensorProduct.AlgebraTensorModule.map_bilinear` + * `TensorProduct.AlgebraTensorModule.mapBilinear` * `TensorProduct.AlgebraTensorModule.congr` + * `TensorProduct.AlgebraTensorModule.mapBilinear` + * `TensorProduct.AlgebraTensorModule.homTensorHomMap` * `TensorProduct.AlgebraTensorModule.assoc` - * `TensorProduct.AlgebraTensorModule.left_comm` + * `TensorProduct.AlgebraTensorModule.leftComm` are just more general versions of the definitions already in `LinearAlgebra/TensorProduct`. We could thus consider replacing the less general definitions with these ones. If we do this, we From 7ef1780c138f6c05c3c589ace83418cbb0327725 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 21 Jul 2023 09:58:59 +0000 Subject: [PATCH 04/14] long line --- Mathlib/RingTheory/TensorProduct.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index 82c8492c704106..9e03ba222f424d 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -213,12 +213,14 @@ def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] map f g (m ⊗ₜ n) = f m ⊗ₜ g n := rfl -theorem map_add_left (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (f₁ + f₂) g = map f₁ g + map f₂ g := by +theorem map_add_left (f₁ f₂ : M →ₗ[A] P) (g : N →ₗ[R] Q) : + map (f₁ + f₂) g = map f₁ g + map f₂ g := by ext simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul, add_apply, add_tmul] -theorem map_add_right (f : M →ₗ[A] P) (g₁ g₂ : N →ₗ[R] Q) : map f (g₁ + g₂) = map f g₁ + map f g₂ := by +theorem map_add_right (f : M →ₗ[A] P) (g₁ g₂ : N →ₗ[R] Q) : + map f (g₁ + g₂) = map f g₁ + map f g₂ := by ext simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul, add_apply, tmul_add] From 4264b66fc3e49b3a685a33beddcea478a9f2e22c Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 21 Jul 2023 10:03:33 +0000 Subject: [PATCH 05/14] wip --- Mathlib/LinearAlgebra/TensorProduct.lean | 13 ++++++++++++- Mathlib/RingTheory/TensorProduct.lean | 2 +- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct.lean b/Mathlib/LinearAlgebra/TensorProduct.lean index f7f34a79aa716f..47860a31382e15 100644 --- a/Mathlib/LinearAlgebra/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/TensorProduct.lean @@ -326,7 +326,18 @@ section -- Like `R'`, `R'₂` provides a `DistribMulAction R'₂ (M ⊗[R] N)` variable {R'₂ : Type _} [Monoid R'₂] [DistribMulAction R'₂ M] -variable [SMulCommClass R R'₂ M] [SMul R'₂ R'] +variable [SMulCommClass R R'₂ M] + +/-- `SMulCommClass R' R'₂ M` implies `SMulCommClass R' R'₂ (M ⊗[R] N)` -/ +instance smulCommClass_left [SMulCommClass R' R'₂ M] : SMulCommClass R' R'₂ (M ⊗[R] N) := +{ smul_comm := fun r' r'₂ x => TensorProduct.induction_on x + (by simp_rw [TensorProduct.smul_zero]) + (fun m n => by simp_rw [smul_tmul', smul_comm]) + (fun x y ihx ihy => by simp_rw [TensorProduct.smul_add]; rw [ihx, ihy]) } +-- TODO: add once https://github.com/leanprover-community/mathlib/pull/19143 is merged +-- #align tensor_product.smul_comm_class_left TensorProduct.smulCommClass_left + +variable [SMul R'₂ R'] /-- `IsScalarTower R'₂ R' M` implies `IsScalarTower R'₂ R' (M ⊗[R] N)` -/ instance isScalarTower_left [IsScalarTower R'₂ R' M] : IsScalarTower R'₂ R' (M ⊗[R] N) := diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index 9e03ba222f424d..bede40fe3d04db 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2020 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Scott Morrison, Johan Commelin +Authors: Scott Morrison, Johan Commelin, Eric Wieser -/ import Mathlib.LinearAlgebra.FiniteDimensional import Mathlib.RingTheory.Adjoin.Basic From dd7166c35990df7695afff239b1fbf463bde48e3 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 24 Jul 2023 14:32:25 +0000 Subject: [PATCH 06/14] bump timeout --- Mathlib/CategoryTheory/Monoidal/Internal/Module.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean b/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean index 5f2e72c5e4f964..2a1c0d440a5a0a 100644 --- a/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean +++ b/Mathlib/CategoryTheory/Monoidal/Internal/Module.lean @@ -168,7 +168,7 @@ end MonModuleEquivalenceAlgebra open MonModuleEquivalenceAlgebra -set_option maxHeartbeats 400000 in +set_option maxHeartbeats 500000 in /-- The category of internal monoid objects in `Module R` is equivalent to the category of "native" bundled `R`-algebras. -/ From d68de547d8afa3e3f259de2715eccb2bb3199822 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 27 Jul 2023 15:44:08 +0000 Subject: [PATCH 07/14] tensorTensorTensorComm --- Mathlib/RingTheory/TensorProduct.lean | 120 ++++++++++++++++++++------ 1 file changed, 94 insertions(+), 26 deletions(-) diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index 2f6facb0ec28f7..42eaf2b396ab7c 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -43,6 +43,7 @@ The heterobasic definitions below such as: * `TensorProduct.AlgebraTensorModule.homTensorHomMap` * `TensorProduct.AlgebraTensorModule.assoc` * `TensorProduct.AlgebraTensorModule.leftComm` + * `TensorProduct.AlgebraTensorModule.tensorTensorTensorComm` are just more general versions of the definitions already in `LinearAlgebra/TensorProduct`. We could thus consider replacing the less general definitions with these ones. If we do this, we @@ -285,7 +286,7 @@ theorem mapBilinear_apply (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : mapBilinear variable (R A M N P Q) -/- Heterobasic version of `TensorProduct.homTensorHomMap` -/ +/-- Heterobasic version of `TensorProduct.homTensorHomMap` -/ def homTensorHomMap : ((M →ₗ[A] P) ⊗[R] (N →ₗ[R] Q)) →ₗ[A] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) := lift <| mapBilinear R A M N P Q @@ -295,35 +296,46 @@ variable {R A M N P Q} homTensorHomMap R A M N P Q (f ⊗ₜ g) = map f g := rfl -variable (R A M N P Q) +variable (R A B M N P Q) attribute [local ext high] TensorProduct.ext +section assoc +variable [Algebra A B] [IsScalarTower A B M] + /-- Heterobasic version of `TensorProduct.assoc`: Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ -def assoc : (M ⊗[A] P) ⊗[R] N ≃ₗ[A] M ⊗[A] P ⊗[R] N := +def assoc : (M ⊗[A] P) ⊗[R] Q ≃ₗ[B] M ⊗[A] (P ⊗[R] Q) := LinearEquiv.ofLinear - (lift <| - TensorProduct.uncurry A _ _ _ <| comp (lcurry R A A _ _ _) <| TensorProduct.mk A M (P ⊗[R] N)) - (TensorProduct.uncurry A _ _ _ <| - comp (uncurry R A A _ _ _) <| by - apply TensorProduct.curry - exact mk R A _ _) - (by - ext - rfl) - (by - ext - -- porting note: was `simp only [...]` - rfl) -#align tensor_product.algebra_tensor_module.assoc TensorProduct.AlgebraTensorModule.assoc + (lift <| lift <| lcurry R A B P Q _ ∘ₗ mk A B M (P ⊗[R] Q)) + (lift <| uncurry R A B P Q _ ∘ₗ curry (mk R B _ Q)) + (by ext; rfl) + (by ext; rfl) +-- porting note: new `B` argument +#align tensor_product.algebra_tensor_module.assoc TensorProduct.AlgebraTensorModule.assocₓ + +variable {M P N Q} + +@[simp] +theorem assoc_tmul (m : M) (p : P) (q : Q) : + assoc R A B M P Q ((m ⊗ₜ p) ⊗ₜ q) = m ⊗ₜ (p ⊗ₜ q) := + rfl + +@[simp] +theorem assoc_symm_tmul (m : M) (p : P) (q : Q) : + (assoc R A B M P Q).symm (m ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ q := + rfl + +end assoc + +section leftComm /-- Heterobasic version of `TensorProduct.leftComm` -/ def leftComm : M ⊗[A] (P ⊗[R] Q) ≃ₗ[A] P ⊗[A] (M ⊗[R] Q) := - let e₁ := (assoc R A M Q P).symm + let e₁ := (assoc R A A M P Q).symm let e₂ := congr (TensorProduct.comm A M P) (1 : Q ≃ₗ[R] Q) - let e₃ := (assoc R A P Q M) + let e₃ := (assoc R A A P M Q) e₁ ≪≫ₗ (e₂ ≪≫ₗ e₃) variable {M N P Q} @@ -338,6 +350,62 @@ theorem leftComm_symm_tmul (m : M) (p : P) (q : Q): (leftComm R A M P Q).symm (p ⊗ₜ (m ⊗ₜ q)) = m ⊗ₜ (p ⊗ₜ q) := rfl +end leftComm + +section rightComm + +/-- A tensor product analogue of `mul_right_comm`. -/ +def rightComm : (M ⊗[A] P) ⊗[R] Q ≃ₗ[A] (M ⊗[R] Q) ⊗[A] P := + LinearEquiv.ofLinear + (lift <| TensorProduct.lift <| LinearMap.flip <| + lcurry R A A M Q ((M ⊗[R] Q) ⊗[A] P) ∘ₗ (mk A A (M ⊗[R] Q) P).flip) + (TensorProduct.lift <| lift <| LinearMap.flip <| + (TensorProduct.lcurry A M P ((M ⊗[A] P) ⊗[R] Q)).restrictScalars R + ∘ₗ (mk R A (M ⊗[A] P) Q).flip) + (by + refine (TensorProduct.ext <| ext <| fun m q => LinearMap.ext <| fun p => ?_) + exact Eq.refl ((m ⊗ₜ[R] q) ⊗ₜ[A] p)) + (by + refine (curry_injective <| TensorProduct.ext' <| fun m p => LinearMap.ext <| fun q => ?_) + exact Eq.refl ((m ⊗ₜ[A] p) ⊗ₜ[R] q)) + +variable {M N P Q} + +@[simp] +theorem rightComm_tmul (m : M) (p : P) (q : Q) : + rightComm R A M P Q ((m ⊗ₜ p) ⊗ₜ q) = (m ⊗ₜ q) ⊗ₜ p := + rfl + +@[simp] +theorem rightComm_symm_tmul (m : M) (p : P) (q : Q): + (rightComm R A M P Q).symm ((m ⊗ₜ q) ⊗ₜ p) = (m ⊗ₜ p) ⊗ₜ q := + rfl + +end rightComm + +section tensorTensorTensorComm + +/-- Heterobasic version of `tensorTensorTensorComm`. -/ +def tensorTensorTensorComm : + (M ⊗[R] N) ⊗[A] (P ⊗[R] Q) ≃ₗ[A] (M ⊗[A] P) ⊗[R] (N ⊗[R] Q) := +(assoc R A A (M ⊗[R] N) P Q).symm + ≪≫ₗ congr (rightComm R A M P N).symm (1 : Q ≃ₗ[R] Q) + ≪≫ₗ assoc R _ _ (M ⊗[A] P) N Q + +variable {M N P Q} + +@[simp] +theorem tensorTensorTensorComm_tmul (m : M) (n : N) (p : P) (q : Q) : + tensorTensorTensorComm R A M N P Q ((m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q)) = (m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q) := + rfl + +@[simp] +theorem tensorTensorTensorComm_symm_tmul (m : M) (p : P) (q : Q): + (tensorTensorTensorComm R A M N P Q).symm ((m ⊗ₜ p) ⊗ₜ (n ⊗ₜ q)) = (m ⊗ₜ n) ⊗ₜ (p ⊗ₜ q) := + rfl + +end tensorTensorTensorComm + end CommSemiring end AlgebraTensorModule @@ -662,15 +730,14 @@ theorem ext {g h : A ⊗[R] B →ₐ[R] C} (H : ∀ a b, g (a ⊗ₜ b) = h (a ext simp [H] #align algebra.tensor_product.ext Algebra.TensorProduct.ext - --- TODO: with `SMulCommClass R S A` we can have this as an `S`-algebra morphism /-- The `R`-algebra morphism `A →ₐ[R] A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/ -def includeLeft : A →ₐ[R] A ⊗[R] B := +def includeLeft [SMulCommClass R S A] : A →ₐ[S] A ⊗[R] B := { includeLeftRingHom with commutes' := by simp } #align algebra.tensor_product.include_left Algebra.TensorProduct.includeLeft @[simp] -theorem includeLeft_apply (a : A) : (includeLeft : A →ₐ[R] A ⊗[R] B) a = a ⊗ₜ 1 := +theorem includeLeft_apply [SMulCommClass R S A] (a : A) : + (includeLeft : A →ₐ[S] A ⊗[R] B) a = a ⊗ₜ 1 := rfl #align algebra.tensor_product.include_left_apply Algebra.TensorProduct.includeLeft_apply @@ -696,7 +763,7 @@ theorem includeRight_apply (b : B) : (includeRight : B →ₐ[R] A ⊗[R] B) b = theorem includeLeft_comp_algebraMap {R S T : Type _} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : - (includeLeft.toRingHom.comp (algebraMap R S) : R →+* S ⊗[R] T) = + (includeLeftRingHom.comp (algebraMap R S) : R →+* S ⊗[R] T) = includeRight.toRingHom.comp (algebraMap R T) := by ext simp @@ -1107,7 +1174,8 @@ theorem productMap_apply_tmul (a : A) (b : B) : productMap f g (a ⊗ₜ b) = f simp #align algebra.tensor_product.product_map_apply_tmul Algebra.TensorProduct.productMap_apply_tmul -theorem productMap_left_apply (a : A) : productMap f g ((includeLeft : A →ₐ[R] A ⊗ B) a) = f a := by +theorem productMap_left_apply (a : A) : + productMap f g (a ⊗ₜ 1) = f a := by simp #align algebra.tensor_product.product_map_left_apply Algebra.TensorProduct.productMap_left_apply @@ -1117,7 +1185,7 @@ theorem productMap_left : (productMap f g).comp includeLeft = f := #align algebra.tensor_product.product_map_left Algebra.TensorProduct.productMap_left theorem productMap_right_apply (b : B) : - productMap f g (includeRight (R := R) (A := A) (B := B) b) = g b := by simp + productMap f g (1 ⊗ₜ b) = g b := by simp #align algebra.tensor_product.product_map_right_apply Algebra.TensorProduct.productMap_right_apply @[simp] From 5f3c6df59b0f981480420df8cb25b462fe8b51ef Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 27 Jul 2023 15:51:33 +0000 Subject: [PATCH 08/14] revert --- Mathlib/RingTheory/TensorProduct.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index 42eaf2b396ab7c..e91848036ab36f 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -730,14 +730,15 @@ theorem ext {g h : A ⊗[R] B →ₐ[R] C} (H : ∀ a b, g (a ⊗ₜ b) = h (a ext simp [H] #align algebra.tensor_product.ext Algebra.TensorProduct.ext + +-- TODO: with `SMulCommClass R S A` we can have this as an `S`-algebra morphism /-- The `R`-algebra morphism `A →ₐ[R] A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/ def includeLeft [SMulCommClass R S A] : A →ₐ[S] A ⊗[R] B := { includeLeftRingHom with commutes' := by simp } #align algebra.tensor_product.include_left Algebra.TensorProduct.includeLeft @[simp] -theorem includeLeft_apply [SMulCommClass R S A] (a : A) : - (includeLeft : A →ₐ[S] A ⊗[R] B) a = a ⊗ₜ 1 := +theorem includeLeft_apply (a : A) : (includeLeft : A →ₐ[R] A ⊗[R] B) a = a ⊗ₜ 1 := rfl #align algebra.tensor_product.include_left_apply Algebra.TensorProduct.includeLeft_apply @@ -763,7 +764,7 @@ theorem includeRight_apply (b : B) : (includeRight : B →ₐ[R] A ⊗[R] B) b = theorem includeLeft_comp_algebraMap {R S T : Type _} [CommRing R] [CommRing S] [CommRing T] [Algebra R S] [Algebra R T] : - (includeLeftRingHom.comp (algebraMap R S) : R →+* S ⊗[R] T) = + (includeLeft.toRingHom.comp (algebraMap R S) : R →+* S ⊗[R] T) = includeRight.toRingHom.comp (algebraMap R T) := by ext simp @@ -1174,8 +1175,7 @@ theorem productMap_apply_tmul (a : A) (b : B) : productMap f g (a ⊗ₜ b) = f simp #align algebra.tensor_product.product_map_apply_tmul Algebra.TensorProduct.productMap_apply_tmul -theorem productMap_left_apply (a : A) : - productMap f g (a ⊗ₜ 1) = f a := by +theorem productMap_left_apply (a : A) : productMap f g ((includeLeft : A →ₐ[R] A ⊗ B) a) = f a := by simp #align algebra.tensor_product.product_map_left_apply Algebra.TensorProduct.productMap_left_apply @@ -1185,7 +1185,7 @@ theorem productMap_left : (productMap f g).comp includeLeft = f := #align algebra.tensor_product.product_map_left Algebra.TensorProduct.productMap_left theorem productMap_right_apply (b : B) : - productMap f g (1 ⊗ₜ b) = g b := by simp + productMap f g (includeRight (R := R) (A := A) (B := B) b) = g b := by simp #align algebra.tensor_product.product_map_right_apply Algebra.TensorProduct.productMap_right_apply @[simp] From e4ab5b6878c1ef8f949aec17ffe83eebe2da26a6 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 27 Jul 2023 15:53:11 +0000 Subject: [PATCH 09/14] finish revert --- Mathlib/RingTheory/TensorProduct.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index e91848036ab36f..f09c44e3f750ea 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -733,7 +733,7 @@ theorem ext {g h : A ⊗[R] B →ₐ[R] C} (H : ∀ a b, g (a ⊗ₜ b) = h (a -- TODO: with `SMulCommClass R S A` we can have this as an `S`-algebra morphism /-- The `R`-algebra morphism `A →ₐ[R] A ⊗[R] B` sending `a` to `a ⊗ₜ 1`. -/ -def includeLeft [SMulCommClass R S A] : A →ₐ[S] A ⊗[R] B := +def includeLeft : A →ₐ[R] A ⊗[R] B := { includeLeftRingHom with commutes' := by simp } #align algebra.tensor_product.include_left Algebra.TensorProduct.includeLeft From 7212072470b106133f3d441836916077c09b9ef2 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 28 Jul 2023 09:20:30 +0000 Subject: [PATCH 10/14] tidy --- Mathlib/LinearAlgebra/TensorProduct/Tower.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean index 7a3e7591c6a2b9..2b94460eec54e3 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean @@ -229,20 +229,20 @@ def mapBilinear : (M →ₗ[A] P) →ₗ[B] (N →ₗ[R] Q) →ₗ[R] (M ⊗[R] map_add' := fun _f₁ _f₂ => LinearMap.ext <| fun _g => map_add_left _ _ _ map_smul' := fun _c _f => LinearMap.ext <| fun _g => map_smul_left _ _ _ } -variable {R A M N P Q} +variable {R A B M N P Q} @[simp] theorem mapBilinear_apply (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : mapBilinear R A B M N P Q f g = map f g := rfl -variable (R A M N P Q) +variable (R A B M N P Q) /-- Heterobasic version of `TensorProduct.homTensorHomMap` -/ def homTensorHomMap : ((M →ₗ[A] P) ⊗[R] (N →ₗ[R] Q)) →ₗ[B] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) := lift <| mapBilinear R A B M N P Q -variable {R A M N P Q} +variable {R A B M N P Q} @[simp] theorem homTensorHomMap_apply (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : homTensorHomMap R A B M N P Q (f ⊗ₜ g) = map f g := From 9686573e6b30e67a4036aaffbaeb97b30f946653 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 31 Jul 2023 18:14:23 +0100 Subject: [PATCH 11/14] Update Tower.lean --- Mathlib/LinearAlgebra/TensorProduct/Tower.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean index 2b94460eec54e3..909a02b837e422 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2020 Scott Morrison. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Scott Morrison, Johan Commelin +Authors: Scott Morrison, Johan Commelin, Eric Wieser -/ import Mathlib.LinearAlgebra.TensorProduct import Mathlib.Algebra.Algebra.Tower From f7b026f9bd3b33a3e89fad54b62b5b64f42402e4 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 01:06:24 +0000 Subject: [PATCH 12/14] tidy --- .../LinearAlgebra/TensorProduct/Tower.lean | 24 +++++++------------ 1 file changed, 9 insertions(+), 15 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean index 909a02b837e422..3850ac24db340a 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean @@ -31,10 +31,10 @@ In this file, we use the convention that `M`, `N`, `P`, `Q` are all `R`-modules, * `TensorProduct.AlgebraTensorModule.map` * `TensorProduct.AlgebraTensorModule.mapBilinear` * `TensorProduct.AlgebraTensorModule.congr` - * `TensorProduct.AlgebraTensorModule.mapBilinear` * `TensorProduct.AlgebraTensorModule.homTensorHomMap` * `TensorProduct.AlgebraTensorModule.assoc` * `TensorProduct.AlgebraTensorModule.leftComm` + * `TensorProduct.AlgebraTensorModule.rightComm` * `TensorProduct.AlgebraTensorModule.tensorTensorTensorComm` ## Implementation notes @@ -187,10 +187,10 @@ variable {R A B M N P Q} /-- Heterobasic version of `TensorProduct.map` -/ def map (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : M ⊗[R] N →ₗ[A] P ⊗[R] Q := - lift $ (show (Q →ₗ[R] P ⊗ Q) →ₗ[A] N →ₗ[R] P ⊗[R] Q from - { toFun := fun h => h ∘ₗ g, - map_add' := fun h₁ h₂ => LinearMap.add_comp g h₂ h₁, - map_smul' := fun c h => LinearMap.smul_comp c h g }) ∘ₗ mk R A P Q ∘ₗ f + lift <| + { toFun := fun h => h ∘ₗ g, + map_add' := fun h₁ h₂ => LinearMap.add_comp g h₂ h₁, + map_smul' := fun c h => LinearMap.smul_comp c h g } ∘ₗ mk R A P Q ∘ₗ f @[simp] theorem map_tmul (f : M →ₗ[A] P) (g : N →ₗ[R] Q) (m : M) (n : N) : map f g (m ⊗ₜ n) = f m ⊗ₜ g n := @@ -213,7 +213,7 @@ theorem map_smul_right (r : R) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : map f ( simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul, smul_apply, tmul_smul] -theorem map_smul_left (r : B) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (r • f) g = r • map f g := by +theorem map_smul_left (b : B) (f : M →ₗ[A] P) (g : N →ₗ[R] Q) : map (b • f) g = b • map f g := by ext simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul, smul_apply, smul_tmul'] @@ -222,13 +222,7 @@ variable (R A B M N P Q) /-- Heterobasic version of `TensorProduct.map_bilinear` -/ def mapBilinear : (M →ₗ[A] P) →ₗ[B] (N →ₗ[R] Q) →ₗ[R] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) := - { toFun := fun f => - { toFun := fun g => map f g - map_add' := fun _g₁ _g₂ => map_add_right _ _ _ - map_smul' := fun _c _g => map_smul_right _ _ _ } - map_add' := fun _f₁ _f₂ => LinearMap.ext <| fun _g => map_add_left _ _ _ - map_smul' := fun _c _f => LinearMap.ext <| fun _g => map_smul_left _ _ _ } - + LinearMap.mk₂' _ _ map map_add_left map_smul_left map_add_right map_smul_right variable {R A B M N P Q} @[simp] @@ -317,8 +311,8 @@ section leftComm def leftComm : M ⊗[A] (P ⊗[R] Q) ≃ₗ[A] P ⊗[A] (M ⊗[R] Q) := let e₁ := (assoc R A A M P Q).symm let e₂ := congr (TensorProduct.comm A M P) (1 : Q ≃ₗ[R] Q) - let e₃ := (assoc R A A P M Q) - e₁ ≪≫ₗ (e₂ ≪≫ₗ e₃) + let e₃ := assoc R A A P M Q + e₁ ≪≫ₗ e₂ ≪≫ₗ e₃ variable {M N P Q} From 4dbcc441e09d349224cb2a77e39191de79e90021 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 01:07:14 +0000 Subject: [PATCH 13/14] reduce diff --- Mathlib/LinearAlgebra/TensorProduct/Tower.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean index 3850ac24db340a..2f522aefe1f695 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean @@ -52,8 +52,8 @@ universe uR uA uB uM uN uP uQ variable {R : Type uR} {A : Type uA} {B : Type uB} variable {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} -open Algebra (lsmul) open LinearMap +open Algebra (lsmul) section Semiring From 0b43277cec975fedc52e404fbb411c25a20b652b Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 12:06:04 +0000 Subject: [PATCH 14/14] golf --- .../LinearAlgebra/TensorProduct/Tower.lean | 26 +++++++++++-------- 1 file changed, 15 insertions(+), 11 deletions(-) diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean index 2f522aefe1f695..f4824d837ddeb2 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean @@ -14,8 +14,8 @@ import Mathlib.Algebra.Algebra.Tower When `M` is both an `R`-module and an `A`-module, and `Algebra R A`, then many of the morphisms preserve the actions by `A`. -This file provides more general versions of the definitions already in -`LinearAlgebra/TensorProduct`. +The `Module` instance itself is provided elsewhere as `TensorProduct.leftModule`. This file provides +more general versions of the definitions already in `LinearAlgebra/TensorProduct`. In this file, we use the convention that `M`, `N`, `P`, `Q` are all `R`-modules, but only `M` and `P` are simultaneously `A`-modules. @@ -223,6 +223,7 @@ variable (R A B M N P Q) /-- Heterobasic version of `TensorProduct.map_bilinear` -/ def mapBilinear : (M →ₗ[A] P) →ₗ[B] (N →ₗ[R] Q) →ₗ[R] (M ⊗[R] N →ₗ[A] P ⊗[R] Q) := LinearMap.mk₂' _ _ map map_add_left map_smul_left map_add_right map_smul_right + variable {R A B M N P Q} @[simp] @@ -245,8 +246,8 @@ variable {R A B M N P Q} /-- Heterobasic version of `TensorProduct.congr` -/ def congr (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) : (M ⊗[R] N) ≃ₗ[A] (P ⊗[R] Q) := LinearEquiv.ofLinear (map f g) (map f.symm g.symm) - (ext fun m n => by simp) - (ext fun m n => by simp) + (ext fun _m _n => congr_arg₂ (· ⊗ₜ ·) (f.apply_symm_apply _) (g.apply_symm_apply _)) + (ext fun _m _n => congr_arg₂ (· ⊗ₜ ·) (f.symm_apply_apply _) (g.symm_apply_apply _)) @[simp] theorem congr_tmul (f : M ≃ₗ[A] P) (g : N ≃ₗ[R] Q) (m : M) (n : N) : congr f g (m ⊗ₜ n) = f m ⊗ₜ g n := @@ -281,7 +282,10 @@ variable [Algebra A B] [IsScalarTower A B M] /-- Heterobasic version of `TensorProduct.assoc`: -Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/ +Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. + +Note this is especially useful with `A = R` (where it is a "more linear" version of +`TensorProduct.assoc`), or with `B = A`. -/ def assoc : (M ⊗[A] P) ⊗[R] Q ≃ₗ[B] M ⊗[A] (P ⊗[R] Q) := LinearEquiv.ofLinear (lift <| lift <| lcurry R A B P Q _ ∘ₗ mk A B M (P ⊗[R] Q)) @@ -338,12 +342,12 @@ def rightComm : (M ⊗[A] P) ⊗[R] Q ≃ₗ[A] (M ⊗[R] Q) ⊗[A] P := (TensorProduct.lift <| lift <| LinearMap.flip <| (TensorProduct.lcurry A M P ((M ⊗[A] P) ⊗[R] Q)).restrictScalars R ∘ₗ (mk R A (M ⊗[A] P) Q).flip) - (by - refine (TensorProduct.ext <| ext <| fun m q => LinearMap.ext <| fun p => ?_) - exact Eq.refl ((m ⊗ₜ[R] q) ⊗ₜ[A] p)) - (by - refine (curry_injective <| TensorProduct.ext' <| fun m p => LinearMap.ext <| fun q => ?_) - exact Eq.refl ((m ⊗ₜ[A] p) ⊗ₜ[R] q)) + -- explicit `Eq.refl`s here help with performance, but also make it clear that the `ext` are + -- letting us prove the result as an equality of pure tensors. + (TensorProduct.ext <| ext <| fun m q => LinearMap.ext <| fun p => Eq.refl <| + (m ⊗ₜ[R] q) ⊗ₜ[A] p) + (curry_injective <| TensorProduct.ext' <| fun m p => LinearMap.ext <| fun q => Eq.refl <| + (m ⊗ₜ[A] p) ⊗ₜ[R] q) variable {M N P Q}