From 02508fd189adbefcdb7313a007e82fb779ab2700 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 20 Jul 2023 19:54:35 +0000 Subject: [PATCH 01/37] 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/37] 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/37] 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/37] 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/37] 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/37] 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/37] 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/37] 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/37] 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/37] 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 307f8ffe263132bf356eace5f7417745eb9df484 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 28 Jul 2023 09:45:35 +0000 Subject: [PATCH 11/37] refactor(Algebra/Module/LinearMap): generalize the endomorphism algebra instance This also moves some lemmas about `IsUnit (_ : Module.End R M)` to an earlier file as they are nothing to do with `Algebra`. --- Mathlib/Algebra/Algebra/Basic.lean | 44 +++++++++------------------ Mathlib/Algebra/Module/Equiv.lean | 12 ++++++++ Mathlib/Algebra/Module/LinearMap.lean | 13 ++++++++ 3 files changed, 39 insertions(+), 30 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Basic.lean b/Mathlib/Algebra/Algebra/Basic.lean index 0420e918f71e8b..4fcad53f7ff095 100644 --- a/Mathlib/Algebra/Algebra/Basic.lean +++ b/Mathlib/Algebra/Algebra/Basic.lean @@ -615,19 +615,23 @@ end MulOpposite namespace Module -variable (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] +variable (R : Type u) (S : Type v) (M : Type w) +variable [CommSemiring R] [Semiring S] [AddCommMonoid M] [Module R M] [Module S M] +variable [SMulCommClass S R M] [SMul R S] [IsScalarTower R S M] -instance : Algebra R (Module.End R M) := +instance End.instAlgebra : Algebra R (Module.End S M) := Algebra.ofModule smul_mul_assoc fun r f g => (smul_comm r f g).symm -theorem algebraMap_end_eq_smul_id (a : R) : (algebraMap R (End R M)) a = a • LinearMap.id := +-- to prove this is a special case of the above +example : Algebra R (Module.End R M) := End.instAlgebra _ _ _ + +theorem algebraMap_end_eq_smul_id (a : R) : algebraMap R (End S M) a = a • LinearMap.id := rfl -#align module.algebra_map_End_eq_smul_id Module.algebraMap_end_eq_smul_id @[simp] -theorem algebraMap_end_apply (a : R) (m : M) : (algebraMap R (End R M)) a m = a • m := +theorem algebraMap_end_apply (a : R) (m : M) : algebraMap R (End S M) a m = a • m := rfl -#align module.algebra_map_End_apply Module.algebraMap_end_apply +#align module.algebra_map_End_apply Module.algebraMap_end_applyₓ @[simp] theorem ker_algebraMap_end (K : Type u) (V : Type v) [Field K] [AddCommGroup V] [Module K V] (a : K) @@ -639,29 +643,9 @@ section variable {R M} -theorem End_isUnit_apply_inv_apply_of_isUnit {f : Module.End R M} (h : IsUnit f) (x : M) : - f (h.unit.inv x) = x := - show (f * h.unit.inv) x = x by simp -#align module.End_is_unit_apply_inv_apply_of_is_unit Module.End_isUnit_apply_inv_apply_of_isUnit - -theorem End_isUnit_inv_apply_apply_of_isUnit {f : Module.End R M} (h : IsUnit f) (x : M) : - h.unit.inv (f x) = x := - (by simp : (h.unit.inv * f) x = x) -#align module.End_is_unit_inv_apply_apply_of_is_unit Module.End_isUnit_inv_apply_apply_of_isUnit - -theorem End_isUnit_iff (f : Module.End R M) : IsUnit f ↔ Function.Bijective f := - ⟨fun h => - Function.bijective_iff_has_inverse.mpr <| - ⟨h.unit.inv, - ⟨End_isUnit_inv_apply_apply_of_isUnit h, End_isUnit_apply_inv_apply_of_isUnit h⟩⟩, - fun H => - let e : M ≃ₗ[R] M := { f, Equiv.ofBijective f H with } - ⟨⟨_, e.symm, LinearMap.ext e.right_inv, LinearMap.ext e.left_inv⟩, rfl⟩⟩ -#align module.End_is_unit_iff Module.End_isUnit_iff - theorem End_algebraMap_isUnit_inv_apply_eq_iff {x : R} - (h : IsUnit (algebraMap R (Module.End R M) x)) (m m' : M) : - (↑(h.unit⁻¹) : Module.End R M) m = m' ↔ m = x • m' := + (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) : + (↑(h.unit⁻¹) : Module.End S M) m = m' ↔ m = x • m' := { mp := fun H => ((congr_arg h.unit H).symm.trans (End_isUnit_apply_inv_apply_of_isUnit h _)).symm mpr := fun H => H.symm ▸ by @@ -671,8 +655,8 @@ theorem End_algebraMap_isUnit_inv_apply_eq_iff {x : R} #align module.End_algebra_map_is_unit_inv_apply_eq_iff Module.End_algebraMap_isUnit_inv_apply_eq_iff theorem End_algebraMap_isUnit_inv_apply_eq_iff' {x : R} - (h : IsUnit (algebraMap R (Module.End R M) x)) (m m' : M) : - m' = (↑h.unit⁻¹ : Module.End R M) m ↔ m = x • m' := + (h : IsUnit (algebraMap R (Module.End S M) x)) (m m' : M) : + m' = (↑h.unit⁻¹ : Module.End S M) m ↔ m = x • m' := { mp := fun H => ((congr_arg h.unit H).trans (End_isUnit_apply_inv_apply_of_isUnit h _)).symm mpr := fun H => H.symm ▸ by diff --git a/Mathlib/Algebra/Module/Equiv.lean b/Mathlib/Algebra/Module/Equiv.lean index fe952a47bfae50..1f1b1f8e294562 100644 --- a/Mathlib/Algebra/Module/Equiv.lean +++ b/Mathlib/Algebra/Module/Equiv.lean @@ -635,6 +635,18 @@ theorem restrictScalars_inj (f g : M ≃ₗ[S] M₂) : end RestrictScalars +theorem _root_.Module.End_isUnit_iff [Module R M] (f : Module.End R M) : + IsUnit f ↔ Function.Bijective f := + ⟨fun h => + Function.bijective_iff_has_inverse.mpr <| + ⟨h.unit.inv, + ⟨Module.End_isUnit_inv_apply_apply_of_isUnit h, + Module.End_isUnit_apply_inv_apply_of_isUnit h⟩⟩, + fun H => + let e : M ≃ₗ[R] M := { f, Equiv.ofBijective f H with } + ⟨⟨_, e.symm, LinearMap.ext e.right_inv, LinearMap.ext e.left_inv⟩, rfl⟩⟩ +#align module.End_is_unit_iff Module.End_isUnit_iff + section Automorphisms variable [Module R M] diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index f848395812c26c..eae8174ca1db18 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -1102,6 +1102,19 @@ instance _root_.Module.End.smulCommClass' [SMul S R] [IsScalarTower S R M] : SMulCommClass.symm _ _ _ #align module.End.smul_comm_class' Module.End.smulCommClass' + +theorem _root_.Module.End_isUnit_apply_inv_apply_of_isUnit + {f : Module.End R M} (h : IsUnit f) (x : M) : + f (h.unit.inv x) = x := + show (f * h.unit.inv) x = x by simp +#align module.End_is_unit_apply_inv_apply_of_is_unit Module.End_isUnit_apply_inv_apply_of_isUnit + +theorem _root_.Module.End_isUnit_inv_apply_apply_of_isUnit + {f : Module.End R M} (h : IsUnit f) (x : M) : + h.unit.inv (f x) = x := + (by simp : (h.unit.inv * f) x = x) +#align module.End_is_unit_inv_apply_apply_of_is_unit Module.End_isUnit_inv_apply_apply_of_isUnit + end /-! ### Action by a module endomorphism. -/ From 9faa43000d09e7ab054bb2fc457be95ea615b75a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 28 Jul 2023 09:47:10 +0000 Subject: [PATCH 12/37] whitespace --- Mathlib/Algebra/Module/LinearMap.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/Mathlib/Algebra/Module/LinearMap.lean b/Mathlib/Algebra/Module/LinearMap.lean index eae8174ca1db18..7477012014e533 100644 --- a/Mathlib/Algebra/Module/LinearMap.lean +++ b/Mathlib/Algebra/Module/LinearMap.lean @@ -1102,7 +1102,6 @@ instance _root_.Module.End.smulCommClass' [SMul S R] [IsScalarTower S R M] : SMulCommClass.symm _ _ _ #align module.End.smul_comm_class' Module.End.smulCommClass' - theorem _root_.Module.End_isUnit_apply_inv_apply_of_isUnit {f : Module.End R M} (h : IsUnit f) (x : M) : f (h.unit.inv x) = x := From 782758b55bcc67abad63202e49ec5adfe687326e Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 28 Jul 2023 10:40:37 +0000 Subject: [PATCH 13/37] fix --- Mathlib/Algebra/Module/LocalizedModule.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Module/LocalizedModule.lean b/Mathlib/Algebra/Module/LocalizedModule.lean index f3df238ef2f824..d5969be43330c4 100644 --- a/Mathlib/Algebra/Module/LocalizedModule.lean +++ b/Mathlib/Algebra/Module/LocalizedModule.lean @@ -1000,7 +1000,7 @@ theorem mk'_mul_mk'_of_map_mul {M M' : Type _} [Semiring M] [Semiring M'] [Modul [IsLocalizedModule S f] (m₁ m₂ : M) (s₁ s₂ : S) : mk' f m₁ s₁ * mk' f m₂ s₂ = mk' f (m₁ * m₂) (s₁ * s₂) := by symm - apply (Module.End_algebraMap_isUnit_inv_apply_eq_iff _ _ _).mpr + apply (Module.End_algebraMap_isUnit_inv_apply_eq_iff _ _ _ _).mpr simp_rw [Submonoid.coe_mul, ← smul_eq_mul] rw [smul_smul_smul_comm, ← mk'_smul, ← mk'_smul] simp_rw [← Submonoid.smul_def, mk'_cancel, smul_eq_mul, hf] From af5660167c17fcb75bacf0a7467a721e3a8b9e00 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 28 Jul 2023 10:57:24 +0000 Subject: [PATCH 14/37] feat: generalize scalars in Algebra.lsmul --- Mathlib/Algebra/Algebra/Tower.lean | 27 ++++++++++++++------------- 1 file changed, 14 insertions(+), 13 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Tower.lean b/Mathlib/Algebra/Algebra/Tower.lean index a0c51214184e22..8c6ee0b4f181c0 100644 --- a/Mathlib/Algebra/Algebra/Tower.lean +++ b/Mathlib/Algebra/Algebra/Tower.lean @@ -30,28 +30,29 @@ variable (R : Type u) (S : Type v) (A : Type w) (B : Type u₁) (M : Type v₁) namespace Algebra -variable [CommSemiring R] [Semiring A] [Algebra R A] - -variable [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] +variable [CommSemiring R] [Semiring A] [CommSemiring S] [Algebra R A] +variable [AddCommMonoid M] [SMul R S] [Module R M] [Module S M] [Module A M] +variable [IsScalarTower R A M] [IsScalarTower R S M] [SMulCommClass S R M] [SMulCommClass A S M] variable {A} + /-- The `R`-algebra morphism `A → End (M)` corresponding to the representation of the algebra `A` -on the `R`-module `M`. +on the `S`-module `M`. This is a stronger version of `DistribMulAction.toLinearMap`, and could also have been called `Algebra.toModuleEnd`. -/ -def lsmul : A →ₐ[R] Module.End R M where - toFun := DistribMulAction.toLinearMap R M +def lsmul : A →ₐ[R] Module.End S M where + toFun := DistribMulAction.toLinearMap S M map_one' := LinearMap.ext fun _ => one_smul A _ map_mul' a b := LinearMap.ext <| smul_assoc a b map_zero' := LinearMap.ext fun _ => zero_smul A _ map_add' _a _b := LinearMap.ext fun _ => add_smul _ _ _ commutes' r := LinearMap.ext <| algebraMap_smul A r -#align algebra.lsmul Algebra.lsmul +#align algebra.lsmul Algebra.lsmulₓ @[simp] -theorem lsmul_coe (a : A) : (lsmul R M a : M → M) = (· • ·) a := rfl +theorem lsmul_coe (a : A) : (lsmul R S M a : M → M) = (· • ·) a := rfl #align algebra.lsmul_coe Algebra.lsmul_coe end Algebra @@ -354,13 +355,13 @@ section Ring namespace Algebra -variable [CommSemiring R] [Semiring A] [Algebra R A] - -variable [AddCommGroup M] [Module A M] [Module R M] [IsScalarTower R A M] +variable [CommSemiring R] [Semiring A] [Semiring S] [Algebra R A] +variable [AddCommGroup M] [SMul R S] [Module R M] [Module S M] [Module A M] +variable [IsScalarTower R A M] [IsScalarTower R S M] [SMulCommClass S R M] [SMulCommClass A S M] theorem lsmul_injective [NoZeroSMulDivisors A M] {x : A} (hx : x ≠ 0) : - Function.Injective (lsmul R M x) := - smul_right_injective _ hx + Function.Injective (lsmul R S M x) := + smul_right_injective M hx #align algebra.lsmul_injective Algebra.lsmul_injective end Algebra From 13567e687ac0920d453306fc422dc7ed99009701 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 28 Jul 2023 10:58:09 +0000 Subject: [PATCH 15/37] oops --- Mathlib/Algebra/Algebra/Tower.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Algebra/Tower.lean b/Mathlib/Algebra/Algebra/Tower.lean index 8c6ee0b4f181c0..5475df1d9f8432 100644 --- a/Mathlib/Algebra/Algebra/Tower.lean +++ b/Mathlib/Algebra/Algebra/Tower.lean @@ -30,7 +30,7 @@ variable (R : Type u) (S : Type v) (A : Type w) (B : Type u₁) (M : Type v₁) namespace Algebra -variable [CommSemiring R] [Semiring A] [CommSemiring S] [Algebra R A] +variable [CommSemiring R] [Semiring A] [Semiring S] [Algebra R A] variable [AddCommMonoid M] [SMul R S] [Module R M] [Module S M] [Module A M] variable [IsScalarTower R A M] [IsScalarTower R S M] [SMulCommClass S R M] [SMulCommClass A S M] From dfce7df25adbd2e85206ffccfe4c98faebafbc57 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 28 Jul 2023 11:24:10 +0000 Subject: [PATCH 16/37] fixes --- Mathlib/Algebra/Algebra/RestrictScalars.lean | 2 +- Mathlib/Algebra/Algebra/Subalgebra/Tower.lean | 2 +- Mathlib/LinearAlgebra/Matrix/ToLin.lean | 2 +- Mathlib/LinearAlgebra/TensorProduct/Tower.lean | 6 +++--- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/Mathlib/Algebra/Algebra/RestrictScalars.lean b/Mathlib/Algebra/Algebra/RestrictScalars.lean index c10dc638f82de2..1144cd90a94477 100644 --- a/Mathlib/Algebra/Algebra/RestrictScalars.lean +++ b/Mathlib/Algebra/Algebra/RestrictScalars.lean @@ -140,7 +140,7 @@ def RestrictScalars.lsmul [Module S M] : S →ₐ[R] Module.End R (RestrictScala letI-- We use `RestrictScalars.moduleOrig` in the implementation, -- but not in the type. : Module S (RestrictScalars R S M) := RestrictScalars.moduleOrig R S M - Algebra.lsmul R (RestrictScalars R S M) + Algebra.lsmul R R (RestrictScalars R S M) #align restrict_scalars.lsmul RestrictScalars.lsmul end diff --git a/Mathlib/Algebra/Algebra/Subalgebra/Tower.lean b/Mathlib/Algebra/Algebra/Subalgebra/Tower.lean index 1132228caf3f07..f199394bfe659c 100644 --- a/Mathlib/Algebra/Algebra/Subalgebra/Tower.lean +++ b/Mathlib/Algebra/Algebra/Subalgebra/Tower.lean @@ -43,7 +43,7 @@ variable [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M] variable {A} -theorem lmul_algebraMap (x : R) : Algebra.lmul R A (algebraMap R A x) = Algebra.lsmul R A x := +theorem lmul_algebraMap (x : R) : Algebra.lmul R A (algebraMap R A x) = Algebra.lsmul R R A x := Eq.symm <| LinearMap.ext <| smul_def x #align algebra.lmul_algebra_map Algebra.lmul_algebraMap diff --git a/Mathlib/LinearAlgebra/Matrix/ToLin.lean b/Mathlib/LinearAlgebra/Matrix/ToLin.lean index 74419fa97fd9a9..663adbf58cf8c5 100644 --- a/Mathlib/LinearAlgebra/Matrix/ToLin.lean +++ b/Mathlib/LinearAlgebra/Matrix/ToLin.lean @@ -850,7 +850,7 @@ theorem toMatrix_lmul' (x : S) (i j) : @[simp] theorem toMatrix_lsmul (x : R) : - LinearMap.toMatrix b b (Algebra.lsmul R S x) = Matrix.diagonal fun _ => x := + LinearMap.toMatrix b b (Algebra.lsmul R R S x) = Matrix.diagonal fun _ => x := toMatrix_distrib_mul_action_toLinearMap b x #align algebra.to_matrix_lsmul Algebra.toMatrix_lsmul diff --git a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean index 878b6120894e7d..1ec86d8347ae60 100644 --- a/Mathlib/LinearAlgebra/TensorProduct/Tower.lean +++ b/Mathlib/LinearAlgebra/TensorProduct/Tower.lean @@ -53,7 +53,7 @@ variable [AddCommMonoid N] [Module R N] variable [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P] -theorem smul_eq_lsmul_rTensor (a : A) (x : M ⊗[R] N) : a • x = (lsmul R M a).rTensor N x := +theorem smul_eq_lsmul_rTensor (a : A) (x : M ⊗[R] N) : a • x = (lsmul R R M a).rTensor N x := rfl #align tensor_product.algebra_tensor_module.smul_eq_lsmul_rtensor TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor @@ -111,8 +111,8 @@ nonrec def lift (f : M →ₗ[A] N →ₗ[R] P) : M ⊗[R] N →ₗ[A] P := map_smul' := fun c => show ∀ x : M ⊗[R] N, - (lift (f.restrictScalars R)).comp (lsmul R _ c) x = - (lsmul R _ c).comp (lift (f.restrictScalars R)) x + (lift (f.restrictScalars R)).comp (lsmul R R _ c) x = + (lsmul R R _ c).comp (lift (f.restrictScalars R)) x from ext_iff.1 <| TensorProduct.ext' fun x y => by From 7e128b07200469565e05ca2ccd47ef5f42e777d6 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 28 Jul 2023 12:06:46 +0000 Subject: [PATCH 17/37] fix --- Mathlib/Analysis/NormedSpace/OperatorNorm.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean index a9a9ceefec428c..cb294ef7d8b8c9 100644 --- a/Mathlib/Analysis/NormedSpace/OperatorNorm.lean +++ b/Mathlib/Analysis/NormedSpace/OperatorNorm.lean @@ -1188,7 +1188,7 @@ variable [NormedAlgebra 𝕜 𝕜'] [NormedSpace 𝕜' E] [IsScalarTower 𝕜 /-- Scalar multiplication as a continuous bilinear map. -/ def lsmul : 𝕜' →L[𝕜] E →L[𝕜] E := - ((Algebra.lsmul 𝕜 E).toLinearMap : 𝕜' →ₗ[𝕜] E →ₗ[𝕜] E).mkContinuous₂ 1 fun c x => by + ((Algebra.lsmul 𝕜 𝕜 E).toLinearMap : 𝕜' →ₗ[𝕜] E →ₗ[𝕜] E).mkContinuous₂ 1 fun c x => by simpa only [one_mul] using norm_smul_le c x #align continuous_linear_map.lsmul ContinuousLinearMap.lsmul From 6f20ebf1b265e9d9787b063373b806c2d42f63fc Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 28 Jul 2023 12:12:43 +0000 Subject: [PATCH 18/37] fix --- 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 b55f40508424f5..6485cc7e4c467f 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -969,7 +969,7 @@ variable [IsScalarTower R A M] [IsScalarTower R B M] `TensorProduct.Algebra.module` below. -/ def moduleAux : A ⊗[R] B →ₗ[R] M →ₗ[R] M := TensorProduct.lift - { toFun := fun a => a • (Algebra.lsmul R M : B →ₐ[R] Module.End R M).toLinearMap + { toFun := fun a => a • (Algebra.lsmul R R M : B →ₐ[R] Module.End R M).toLinearMap map_add' := fun r t => by ext simp only [add_smul, LinearMap.add_apply] From a42a1ee6790d72af3d48fadb7b511abd5c215df8 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 28 Jul 2023 13:44:57 +0100 Subject: [PATCH 19/37] Update Basic.lean --- Mathlib/RepresentationTheory/Basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RepresentationTheory/Basic.lean b/Mathlib/RepresentationTheory/Basic.lean index fd61cee19c0f0a..4ab4190de728d5 100644 --- a/Mathlib/RepresentationTheory/Basic.lean +++ b/Mathlib/RepresentationTheory/Basic.lean @@ -164,7 +164,7 @@ only on a type synonym of the original module.) -/ noncomputable def ofModule' (M : Type _) [AddCommMonoid M] [Module k M] [Module (MonoidAlgebra k G) M] [IsScalarTower k (MonoidAlgebra k G) M] : Representation k G M := - (MonoidAlgebra.lift k G (M →ₗ[k] M)).symm (Algebra.lsmul k M) + (MonoidAlgebra.lift k G (M →ₗ[k] M)).symm (Algebra.lsmul k k M) #align representation.of_module' Representation.ofModule' section From 90f237b5e78b247acaf3429ecd7f14a29a6b9656 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Fri, 28 Jul 2023 13:46:00 +0100 Subject: [PATCH 20/37] Update MatrixAlgebra.lean --- Mathlib/RingTheory/MatrixAlgebra.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/RingTheory/MatrixAlgebra.lean b/Mathlib/RingTheory/MatrixAlgebra.lean index 55dc936c62485d..fde5e7fb7f4b0f 100644 --- a/Mathlib/RingTheory/MatrixAlgebra.lean +++ b/Mathlib/RingTheory/MatrixAlgebra.lean @@ -40,7 +40,7 @@ The function underlying `(A ⊗[R] Matrix n n R) →ₐ[R] Matrix n n A`, as an `R`-bilinear map. -/ def toFunBilinear : A →ₗ[R] Matrix n n R →ₗ[R] Matrix n n A := - (Algebra.lsmul R (Matrix n n A)).toLinearMap.compl₂ (Algebra.linearMap R A).mapMatrix + (Algebra.lsmul R R (Matrix n n A)).toLinearMap.compl₂ (Algebra.linearMap R A).mapMatrix #align matrix_equiv_tensor.to_fun_bilinear MatrixEquivTensor.toFunBilinear @[simp] From 6577af3cfd76bd449876b1693174b27c0b69d44b Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 31 Jul 2023 17:12:48 +0000 Subject: [PATCH 21/37] comment --- Mathlib/Algebra/Algebra/Tower.lean | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Algebra/Tower.lean b/Mathlib/Algebra/Algebra/Tower.lean index 5475df1d9f8432..a231b789d95b09 100644 --- a/Mathlib/Algebra/Algebra/Tower.lean +++ b/Mathlib/Algebra/Algebra/Tower.lean @@ -41,7 +41,16 @@ variable {A} on the `S`-module `M`. This is a stronger version of `DistribMulAction.toLinearMap`, and could also have been -called `Algebra.toModuleEnd`. -/ +called `Algebra.toModuleEnd`. + +Note this can be used to get the fact that left-multiplication by `A` is right `A`-linear, and vice +versa, as +```lean +example : A →ₐ[R] Module.End Aᵐᵒᵖ A := Algebra.lsmul R Aᵐᵒᵖ A +example : Aᵐᵒᵖ →ₐ[R] Module.End A A := Algebra.lsmul R A A +``` +respectively; though `LinearMap.mulLeft` and `LinearMap.mulRight` can also be used here. +-/ def lsmul : A →ₐ[R] Module.End S M where toFun := DistribMulAction.toLinearMap S M map_one' := LinearMap.ext fun _ => one_smul A _ From 9686573e6b30e67a4036aaffbaeb97b30f946653 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 31 Jul 2023 18:14:23 +0100 Subject: [PATCH 22/37] 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 23/37] 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 24/37] 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 7b3573358b10f1eb381069e509de37d70969327a Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 11:04:55 +0000 Subject: [PATCH 25/37] ungeneralize slightly --- Mathlib/Algebra/Algebra/Tower.lean | 30 +++++++++++++++++++++--------- 1 file changed, 21 insertions(+), 9 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Tower.lean b/Mathlib/Algebra/Algebra/Tower.lean index a231b789d95b09..4924387e53316b 100644 --- a/Mathlib/Algebra/Algebra/Tower.lean +++ b/Mathlib/Algebra/Algebra/Tower.lean @@ -30,29 +30,41 @@ variable (R : Type u) (S : Type v) (A : Type w) (B : Type u₁) (M : Type v₁) namespace Algebra -variable [CommSemiring R] [Semiring A] [Semiring S] [Algebra R A] -variable [AddCommMonoid M] [SMul R S] [Module R M] [Module S M] [Module A M] -variable [IsScalarTower R A M] [IsScalarTower R S M] [SMulCommClass S R M] [SMulCommClass A S M] +variable [CommSemiring R] [Semiring A] [Semiring 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 {A} /-- The `R`-algebra morphism `A → End (M)` corresponding to the representation of the algebra `A` -on the `S`-module `M`. +on the `B`-module `M`. This is a stronger version of `DistribMulAction.toLinearMap`, and could also have been called `Algebra.toModuleEnd`. -Note this can be used to get the fact that left-multiplication by `A` is right `A`-linear, and vice -versa, as +The typeclasses correspond to the situation where the types act on each other as +``` +R ----→ B +| ⟍ | +| ⟍ | +↓ ↘ ↓ +A ----→ M +``` +where the diagram commutes, the action by `R` commutes with everything, and the action by `A` and +`B` on `M` commute. + +Typically this is most useful with `B = R` as `Algebra.lsmul R R A : A →ₐ[R] Module.End R M`. +However this can be used to get the fact that left-multiplication by `A` is right `A`-linear, and +vice versa, as ```lean example : A →ₐ[R] Module.End Aᵐᵒᵖ A := Algebra.lsmul R Aᵐᵒᵖ A example : Aᵐᵒᵖ →ₐ[R] Module.End A A := Algebra.lsmul R A A ``` respectively; though `LinearMap.mulLeft` and `LinearMap.mulRight` can also be used here. -/ -def lsmul : A →ₐ[R] Module.End S M where - toFun := DistribMulAction.toLinearMap S M +def lsmul : A →ₐ[R] Module.End B M where + toFun := DistribMulAction.toLinearMap B M map_one' := LinearMap.ext fun _ => one_smul A _ map_mul' a b := LinearMap.ext <| smul_assoc a b map_zero' := LinearMap.ext fun _ => zero_smul A _ @@ -61,7 +73,7 @@ def lsmul : A →ₐ[R] Module.End S M where #align algebra.lsmul Algebra.lsmulₓ @[simp] -theorem lsmul_coe (a : A) : (lsmul R S M a : M → M) = (· • ·) a := rfl +theorem lsmul_coe (a : A) : (lsmul R B M a : M → M) = (· • ·) a := rfl #align algebra.lsmul_coe Algebra.lsmul_coe end Algebra From 0b43277cec975fedc52e404fbb411c25a20b652b Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 12:06:04 +0000 Subject: [PATCH 26/37] 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} From de0022851086c918ccb421ce9d5eef152381ecc3 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 13:01:19 +0000 Subject: [PATCH 27/37] oops --- Mathlib/Algebra/Algebra/Tower.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Algebra/Tower.lean b/Mathlib/Algebra/Algebra/Tower.lean index 4924387e53316b..f30a90badc6227 100644 --- a/Mathlib/Algebra/Algebra/Tower.lean +++ b/Mathlib/Algebra/Algebra/Tower.lean @@ -376,12 +376,12 @@ section Ring namespace Algebra -variable [CommSemiring R] [Semiring A] [Semiring S] [Algebra R A] -variable [AddCommGroup M] [SMul R S] [Module R M] [Module S M] [Module A M] -variable [IsScalarTower R A M] [IsScalarTower R S M] [SMulCommClass S R M] [SMulCommClass A S M] +variable [CommSemiring R] [Semiring A] [Semiring B] [Algebra R A] [Algebra R B] +variable [AddCommGroup M] [Module R M] [Module A M] [Module B M] +variable [IsScalarTower R A M] [IsScalarTower R B M] [SMulCommClass A B M] theorem lsmul_injective [NoZeroSMulDivisors A M] {x : A} (hx : x ≠ 0) : - Function.Injective (lsmul R S M x) := + Function.Injective (lsmul R B M x) := smul_right_injective M hx #align algebra.lsmul_injective Algebra.lsmul_injective From 416ee1d2a690fcdc3ca922da0d43d274c2211fb0 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 14:17:49 +0000 Subject: [PATCH 28/37] feat(LinearAlgebra/BilinearForm/TensorProduct): base change of bilinear forms --- .../BilinearForm/TensorProduct.lean | 30 ++++++++++--------- 1 file changed, 16 insertions(+), 14 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index c454f7c03fc789..0144854154b334 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -5,6 +5,7 @@ Authors: Eric Wieser -/ import Mathlib.LinearAlgebra.BilinearForm import Mathlib.LinearAlgebra.TensorProduct +import Mathlib.LinearAlgebra.TensorProduct.Tower #align_import linear_algebra.bilinear_form.tensor_product from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9" @@ -23,31 +24,32 @@ import Mathlib.LinearAlgebra.TensorProduct universe u v w -variable {ι : Type _} {R : Type _} {M₁ M₂ : Type _} +variable {ι : Type _} {R A : Type _} {M₁ M₂ : Type _} open TensorProduct namespace BilinForm section CommSemiring - -variable [CommSemiring R] - -variable [AddCommMonoid M₁] [AddCommMonoid M₂] - -variable [Module R M₁] [Module R M₂] +variables [CommSemiring R] [CommSemiring A] +variables [AddCommMonoid M₁] [AddCommMonoid M₂] +variables [Algebra R A] [Module R M₁] [Module A M₁] +variables [SMulCommClass R A M₁] [SMulCommClass A R M₁] [SMulCommClass R A A] [IsScalarTower R A M₁] +variables [Module R M₂] /-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. -/ -def tensorDistrib : BilinForm R M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm R (M₁ ⊗[R] M₂) := - ((TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ - (TensorProduct.lift.equiv R _ _ _).symm ≪≫ₗ LinearMap.toBilin).toLinearMap ∘ₗ - TensorProduct.dualDistrib R _ _ ∘ₗ - (TensorProduct.congr (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) +def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm A (M₁ ⊗[R] M₂) := + ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).dualMap + ≪≫ₗ (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) A).symm + ≪≫ₗ LinearMap.toBilin).toLinearMap + ∘ₗ TensorProduct.AlgebraTensorModule.dualDistrib R _ _ + ∘ₗ (TensorProduct.AlgebraTensorModule.congr + (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _)).toLinearMap #align bilin_form.tensor_distrib BilinForm.tensorDistrib @[simp] -theorem tensorDistrib_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) +theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : tensorDistrib (R := R) (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂' := rfl @@ -55,7 +57,7 @@ theorem tensorDistrib_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) ( /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ @[reducible] -protected def tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) : BilinForm R (M₁ ⊗[R] M₂) := +protected def tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : BilinForm A (M₁ ⊗[R] M₂) := tensorDistrib (R := R) (B₁ ⊗ₜ[R] B₂) #align bilin_form.tmul BilinForm.tmul From 290e8df4384852f4600f210c34492024bc695e86 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 14:25:58 +0000 Subject: [PATCH 29/37] fix --- .../BilinearForm/TensorProduct.lean | 21 ++++++++++--------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 0144854154b334..6635687e094c96 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -31,27 +31,28 @@ open TensorProduct namespace BilinForm section CommSemiring -variables [CommSemiring R] [CommSemiring A] -variables [AddCommMonoid M₁] [AddCommMonoid M₂] -variables [Algebra R A] [Module R M₁] [Module A M₁] -variables [SMulCommClass R A M₁] [SMulCommClass A R M₁] [SMulCommClass R A A] [IsScalarTower R A M₁] -variables [Module R M₂] +variable [CommSemiring R] [CommSemiring A] +variable [AddCommMonoid M₁] [AddCommMonoid M₂] +variable [Algebra R A] [Module R M₁] [Module A M₁] +variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [SMulCommClass R A A] [IsScalarTower R A M₁] +variable [Module R M₂] /-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. -/ -def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[R] BilinForm A (M₁ ⊗[R] M₂) := +def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).dualMap ≪≫ₗ (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) A).symm ≪≫ₗ LinearMap.toBilin).toLinearMap - ∘ₗ TensorProduct.AlgebraTensorModule.dualDistrib R _ _ + ∘ₗ sorry -- TensorProduct.AlgebraTensorModule.dualDistrib R _ _ ∘ₗ (TensorProduct.AlgebraTensorModule.congr - (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _) + (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv A _ _ _) (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _)).toLinearMap #align bilin_form.tensor_distrib BilinForm.tensorDistrib @[simp] theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : - tensorDistrib (R := R) (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂' := + tensorDistrib (A := A) (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + = B₁ m₁ m₁' * algebraMap R A (B₂ m₂ m₂') := rfl #align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmul @@ -91,7 +92,7 @@ noncomputable def tensorDistribEquiv : @[simp] theorem tensorDistribEquiv_apply (B : BilinForm R M₁ ⊗ BilinForm R M₂) : - tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) B = tensorDistrib (R := R) B := + tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) B = tensorDistrib (A := R) B := rfl #align bilin_form.tensor_distrib_equiv_apply BilinForm.tensorDistribEquiv_apply From 7511f856734c24268d461096bb02787c8266cacb Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 15:21:13 +0000 Subject: [PATCH 30/37] almost done --- .../BilinearForm/TensorProduct.lean | 7 ++- Mathlib/LinearAlgebra/Dual.lean | 26 ++++++++- Mathlib/RingTheory/TensorProduct.lean | 55 +++++++++++-------- 3 files changed, 61 insertions(+), 27 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 6635687e094c96..c3ae9d6c03447a 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -37,12 +37,15 @@ variable [Algebra R A] [Module R M₁] [Module A M₁] variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [SMulCommClass R A A] [IsScalarTower R A M₁] variable [Module R M₂] -/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. -/ +/-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. + +Note this is heterobasic; the bilinear form on the left can take values in a larger ring than +the one on the right. -/ def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).dualMap ≪≫ₗ (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) A).symm ≪≫ₗ LinearMap.toBilin).toLinearMap - ∘ₗ sorry -- TensorProduct.AlgebraTensorModule.dualDistrib R _ _ + ∘ₗ TensorProduct.AlgebraTensorModule.dualDistrib R _ _ ∘ₗ (TensorProduct.AlgebraTensorModule.congr (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv A _ _ _) (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _)).toLinearMap diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index 5466aa6d915f3d..1d9902510416d2 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -8,6 +8,7 @@ import Mathlib.LinearAlgebra.Projection import Mathlib.LinearAlgebra.SesquilinearForm import Mathlib.RingTheory.Finiteness import Mathlib.LinearAlgebra.FreeModule.Finite.Basic +import Mathlib.RingTheory.TensorProduct #align_import linear_algebra.dual from "leanprover-community/mathlib"@"b1c017582e9f18d8494e5c18602a8cb4a6f843ac" @@ -94,9 +95,9 @@ noncomputable section namespace Module -- Porting note: max u v universe issues so name and specific below -universe u v v' v'' w u₁ u₂ +universe u uA v v' v'' w u₁ u₂ -variable (R : Type u) (M : Type v) +variable (R : Type u) (A : Type uA) (M : Type v) variable [CommSemiring R] [AddCommMonoid M] [Module R M] @@ -1571,7 +1572,7 @@ end VectorSpace namespace TensorProduct -variable (R : Type _) (M : Type _) (N : Type _) +variable (R A : Type _) (M : Type _) (N : Type _) variable {ι κ : Type _} @@ -1613,6 +1614,25 @@ theorem dualDistrib_apply (f : Dual R M) (g : Dual R N) (m : M) (n : N) : end +namespace AlgebraTensorModule +set_option autoImplicit false +variable [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] + +variable [Module R M] [Module A M] [Module R N] [IsScalarTower R A M] + +/-- Heterobasic version of `TensorProduct.dualDistrib` -/ +def dualDistrib : Dual A M ⊗[R] Dual R N →ₗ[A] Dual A (M ⊗[R] N) := + compRight (Algebra.TensorProduct.rid R A A) ∘ₗ homTensorHomMap R A A M N A R + +variable {R M N} + +@[simp] +theorem dualDistrib_apply (f : Dual A M) (g : Dual R N) (m : M) (n : N) : + dualDistrib R A M N (f ⊗ₜ g) (m ⊗ₜ n) = f m * algebraMap _ _ (g n) := + rfl + +end AlgebraTensorModule + variable {R M N} variable [CommRing R] [AddCommGroup M] [AddCommGroup N] diff --git a/Mathlib/RingTheory/TensorProduct.lean b/Mathlib/RingTheory/TensorProduct.lean index 4c318d9bbb67b4..5f3943a13a468e 100644 --- a/Mathlib/RingTheory/TensorProduct.lean +++ b/Mathlib/RingTheory/TensorProduct.lean @@ -31,7 +31,7 @@ In this file we: -/ -universe u v₁ v₂ v₃ v₄ +universe u uS v₁ v₂ v₃ v₄ open scoped TensorProduct @@ -468,24 +468,24 @@ section Monoidal section -variable {R : Type u} [CommSemiring R] +variable {R : Type u} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] -variable {A : Type v₁} [Semiring A] [Algebra R A] +variable {A : Type v₁} [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] variable {B : Type v₂} [Semiring B] [Algebra R B] -variable {C : Type v₃} [Semiring C] [Algebra R C] +variable {C : Type v₃} [Semiring C] [Algebra R C] [Algebra S C] variable {D : Type v₄} [Semiring D] [Algebra R D] /-- Build an algebra morphism from a linear map out of a tensor product, and evidence of multiplicativity on pure tensors. -/ -def algHomOfLinearMapTensorProduct (f : A ⊗[R] B →ₗ[R] C) +def algHomOfLinearMapTensorProduct (f : A ⊗[R] B →ₗ[S] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂)) - (w₂ : ∀ r, f ((algebraMap R A) r ⊗ₜ[R] 1) = (algebraMap R C) r) : A ⊗[R] B →ₐ[R] C := + (w₂ : ∀ r, f ((algebraMap S A) r ⊗ₜ[R] 1) = (algebraMap S C) r) : A ⊗[R] B →ₐ[S] C := { f with - map_one' := by rw [← (algebraMap R C).map_one, ← w₂, (algebraMap R A).map_one]; rfl + map_one' := by rw [← (algebraMap S C).map_one, ← w₂, (algebraMap S A).map_one]; rfl map_zero' := by simp only; rw [LinearMap.toFun_eq_coe, map_zero] map_mul' := fun x y => by simp only @@ -506,22 +506,22 @@ def algHomOfLinearMapTensorProduct (f : A ⊗[R] B →ₗ[R] C) @[simp] theorem algHomOfLinearMapTensorProduct_apply (f w₁ w₂ x) : - (algHomOfLinearMapTensorProduct f w₁ w₂ : A ⊗[R] B →ₐ[R] C) x = f x := + (algHomOfLinearMapTensorProduct f w₁ w₂ : A ⊗[R] B →ₐ[S] C) x = f x := rfl #align algebra.tensor_product.alg_hom_of_linear_map_tensor_product_apply Algebra.TensorProduct.algHomOfLinearMapTensorProduct_apply /-- Build an algebra equivalence from a linear equivalence out of a tensor product, and evidence of multiplicativity on pure tensors. -/ -def algEquivOfLinearEquivTensorProduct (f : A ⊗[R] B ≃ₗ[R] C) +def algEquivOfLinearEquivTensorProduct (f : A ⊗[R] B ≃ₗ[S] C) (w₁ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), f ((a₁ * a₂) ⊗ₜ (b₁ * b₂)) = f (a₁ ⊗ₜ b₁) * f (a₂ ⊗ₜ b₂)) - (w₂ : ∀ r, f ((algebraMap R A) r ⊗ₜ[R] 1) = (algebraMap R C) r) : A ⊗[R] B ≃ₐ[R] C := - { algHomOfLinearMapTensorProduct (f : A ⊗[R] B →ₗ[R] C) w₁ w₂, f with } + (w₂ : ∀ r, f ((algebraMap S A) r ⊗ₜ[R] 1) = (algebraMap S C) r) : A ⊗[R] B ≃ₐ[S] C := + { algHomOfLinearMapTensorProduct (f : A ⊗[R] B →ₗ[S] C) w₁ w₂, f with } #align algebra.tensor_product.alg_equiv_of_linear_equiv_tensor_product Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct @[simp] theorem algEquivOfLinearEquivTensorProduct_apply (f w₁ w₂ x) : - (algEquivOfLinearEquivTensorProduct f w₁ w₂ : A ⊗[R] B ≃ₐ[R] C) x = f x := + (algEquivOfLinearEquivTensorProduct f w₁ w₂ : A ⊗[R] B ≃ₐ[S] C) x = f x := rfl #align algebra.tensor_product.alg_equiv_of_linear_equiv_tensor_product_apply Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct_apply @@ -561,9 +561,9 @@ theorem algEquivOfLinearEquivTripleTensorProduct_apply (f w₁ w₂ x) : end -variable {R : Type u} [CommSemiring R] +variable {R : Type u} {S : Type uS} [CommSemiring R] [CommSemiring S] [Algebra R S] -variable {A : Type v₁} [Semiring A] [Algebra R A] +variable {A : Type v₁} [Semiring A] [Algebra R A] [Algebra S A] [IsScalarTower R S A] variable {B : Type v₂} [Semiring B] [Algebra R B] @@ -590,19 +590,30 @@ theorem lid_tmul (r : R) (a : A) : (TensorProduct.lid R A : R ⊗ A → A) (r simp [TensorProduct.lid] #align algebra.tensor_product.lid_tmul Algebra.TensorProduct.lid_tmul +variable (S) + /-- The base ring is a right identity for the tensor product of algebra, up to algebra isomorphism. + +Note that if `A` is commutative this can be instantiated with `S = A`. -/ -protected nonrec def rid : A ⊗[R] R ≃ₐ[R] A := - algEquivOfLinearEquivTensorProduct (TensorProduct.rid R A) (by - simp [mul_smul] - simp_rw [← mul_smul, mul_comm] - simp) - (by simp [Algebra.smul_def]) +protected nonrec def rid : A ⊗[R] R ≃ₐ[S] A := + let act : R →ₗ[R] A →ₗ[S] A := + (Algebra.lsmul (A := A) S Aᵐᵒᵖ A).toLinearMap.flip.restrictScalars R ∘ₗ Algebra.linearMap R A + let lin : A ⊗[R] R ≃ₗ[S] A := LinearEquiv.ofLinear + (AlgebraTensorModule.lift <| LinearMap.flip <| act) + ((AlgebraTensorModule.mk R A A R).flip 1) + (LinearMap.ext <| fun x => show x * algebraMap R A 1 = x by simp) + (AlgebraTensorModule.ext <| fun x y => show (x * algebraMap R A y) ⊗ₜ[R] 1 = x ⊗ₜ[R] y + by rw [←Algebra.commutes, ←_root_.Algebra.smul_def, smul_tmul, smul_eq_mul, mul_one]) + algEquivOfLinearEquivTensorProduct lin + (fun a₁ a₂ r₁ r₂ => by + show a₁ * a₂ * algebraMap R A (r₁ * r₂) = a₁ * algebraMap R A r₁ * (a₂ * algebraMap R A r₂) + simp_rw [←Algebra.commutes, ←Algebra.smul_def, smul_mul_smul]) + (fun s => show algebraMap S A s * algebraMap R A 1 = algebraMap S A s by simp) #align algebra.tensor_product.rid Algebra.TensorProduct.rid @[simp] -theorem rid_tmul (r : R) (a : A) : (TensorProduct.rid R A : A ⊗ R → A) (a ⊗ₜ r) = r • a := by - simp [TensorProduct.rid] +theorem rid_tmul (r : R) (a : A) : TensorProduct.rid R S A (a ⊗ₜ r) = a * algebraMap _ _ r := rfl #align algebra.tensor_product.rid_tmul Algebra.TensorProduct.rid_tmul section From 1fc8e3096e6125ca2108d1f7053d63254be4f0a2 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 15:35:58 +0000 Subject: [PATCH 31/37] times out --- .../BilinearForm/TensorProduct.lean | 23 +++++++++++++++---- 1 file changed, 18 insertions(+), 5 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index c3ae9d6c03447a..569282fb44aa52 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -22,9 +22,9 @@ import Mathlib.LinearAlgebra.TensorProduct.Tower -/ -universe u v w +universe u v w uι uR uA uM₁ uM₂ -variable {ι : Type _} {R A : Type _} {M₁ M₂ : Type _} +variable {ι : Type _} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} open TensorProduct @@ -34,7 +34,7 @@ section CommSemiring variable [CommSemiring R] [CommSemiring A] variable [AddCommMonoid M₁] [AddCommMonoid M₂] variable [Algebra R A] [Module R M₁] [Module A M₁] -variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [SMulCommClass R A A] [IsScalarTower R A M₁] +variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁] variable [Module R M₂] /-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. @@ -45,7 +45,7 @@ def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).dualMap ≪≫ₗ (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) A).symm ≪≫ₗ LinearMap.toBilin).toLinearMap - ∘ₗ TensorProduct.AlgebraTensorModule.dualDistrib R _ _ + ∘ₗ TensorProduct.AlgebraTensorModule.dualDistrib R _ _ _ ∘ₗ (TensorProduct.AlgebraTensorModule.congr (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv A _ _ _) (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _)).toLinearMap @@ -62,9 +62,22 @@ theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) ( /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ @[reducible] protected def tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : BilinForm A (M₁ ⊗[R] M₂) := - tensorDistrib (R := R) (B₁ ⊗ₜ[R] B₂) + tensorDistrib (A := A) (B₁ ⊗ₜ[R] B₂) #align bilin_form.tmul BilinForm.tmul +/-- The base change of a bilinear form -/ +protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) := by + let why := BilinForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.toBilin <| LinearMap.mul A A) B + exact why -- `exact why` fails! + +@[simp] +theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : M₂) + (a' : A) (m₂' : M₂) : + tensorDistrib (A := A) (B₁ ⊗ₜ B₂) (a ⊗ₜ m₂) (a' ⊗ₜ m₂') + = (a * a') * algebraMap R A (B₂ m₂ m₂') := + rfl +#align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmulₓ + end CommSemiring section CommRing From 0a9471ade69dacbbda78aa9892432be4fd799472 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 2 Aug 2023 15:40:46 +0000 Subject: [PATCH 32/37] golf --- .../LinearAlgebra/BilinearForm/TensorProduct.lean | 13 +++++-------- 1 file changed, 5 insertions(+), 8 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 569282fb44aa52..9d95c190b2a889 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -57,7 +57,7 @@ theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) ( tensorDistrib (A := A) (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * algebraMap R A (B₂ m₂ m₂') := rfl -#align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmul +#align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmulₓ /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ @[reducible] @@ -65,18 +65,15 @@ protected def tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : BilinFo tensorDistrib (A := A) (B₁ ⊗ₜ[R] B₂) #align bilin_form.tmul BilinForm.tmul -/-- The base change of a bilinear form -/ -protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) := by - let why := BilinForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.toBilin <| LinearMap.mul A A) B - exact why -- `exact why` fails! +/-- The base change of a bilinear form. -/ +protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) := + BilinForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.toBilin <| LinearMap.mul A A) B @[simp] theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) : - tensorDistrib (A := A) (B₁ ⊗ₜ B₂) (a ⊗ₜ m₂) (a' ⊗ₜ m₂') - = (a * a') * algebraMap R A (B₂ m₂ m₂') := + B₂.baseChange (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (a * a') * algebraMap R A (B₂ m₂ m₂') := rfl -#align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmulₓ end CommSemiring From 0b52e3b9564228acd0c7fc880b906317fdc87352 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 7 Aug 2023 21:33:03 +0000 Subject: [PATCH 33/37] fix --- Mathlib/LinearAlgebra/Dual.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index bdc5fd63e08ea2..b94f5968582d7a 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -1621,7 +1621,7 @@ variable {R M N} @[simp] theorem dualDistrib_apply (f : Dual A M) (g : Dual R N) (m : M) (n : N) : - dualDistrib R A M N (f ⊗ₜ g) (m ⊗ₜ n) = f m * algebraMap _ _ (g n) := + dualDistrib R A M N (f ⊗ₜ g) (m ⊗ₜ n) = g n • f m := rfl end AlgebraTensorModule From d4ca2d13646ca40a4c85cedc29036befb4080c34 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 7 Aug 2023 21:51:11 +0000 Subject: [PATCH 34/37] fix --- .../BilinearForm/TensorProduct.lean | 26 ++++++++++++++++--- 1 file changed, 23 insertions(+), 3 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 9d95c190b2a889..d62d2d10179b54 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -51,11 +51,13 @@ def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm (BilinForm.toLin ≪≫ₗ TensorProduct.lift.equiv R _ _ _)).toLinearMap #align bilin_form.tensor_distrib BilinForm.tensorDistrib +-- TODO: make the RHS `MulOpposite.op (B₂ m₂ m₂') • B₁ m₁ m₁'` so that this has a nicer defeq for +-- `R = A` of `B₁ m₁ m₁' * B₂ m₂ m₂'`, as it did before the generalization in #6306. @[simp] theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : tensorDistrib (A := A) (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') - = B₁ m₁ m₁' * algebraMap R A (B₂ m₂ m₂') := + = B₂ m₂ m₂' • B₁ m₁ m₁' := rfl #align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmulₓ @@ -72,7 +74,7 @@ protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) := @[simp] theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) : - B₂.baseChange (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (a * a') * algebraMap R A (B₂ m₂ m₂') := + B₂.baseChange (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') := rfl end CommSemiring @@ -103,10 +105,28 @@ noncomputable def tensorDistribEquiv : (TensorProduct.lift.equiv R _ _ _).symm ≪≫ₗ LinearMap.toBilin #align bilin_form.tensor_distrib_equiv BilinForm.tensorDistribEquiv + +@[simp] +theorem tensorDistribEquiv_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) + (m₁' : M₁) (m₂' : M₂) : + tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) (B₁ ⊗ₜ[R] B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + = B₁ m₁ m₁' * B₂ m₂ m₂' := + rfl + +variable (R M₁ M₂) in +-- TODO: make this `rfl` +@[simp] +theorem tensorDistribEquiv_toLinearMap : + (tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib (A := R) := by + ext B₁ B₂ : 3 + apply toLin.injective + ext + exact mul_comm _ _ + @[simp] theorem tensorDistribEquiv_apply (B : BilinForm R M₁ ⊗ BilinForm R M₂) : tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) B = tensorDistrib (A := R) B := - rfl + FunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B #align bilin_form.tensor_distrib_equiv_apply BilinForm.tensorDistribEquiv_apply end CommRing From 03915542bc7c2df9dd29dab72be8fa66df1497e0 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 9 Aug 2023 14:11:59 +0100 Subject: [PATCH 35/37] Update TensorProduct.lean --- Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index d62d2d10179b54..5ed9820ea40255 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -105,8 +105,8 @@ noncomputable def tensorDistribEquiv : (TensorProduct.lift.equiv R _ _ _).symm ≪≫ₗ LinearMap.toBilin #align bilin_form.tensor_distrib_equiv BilinForm.tensorDistribEquiv - -@[simp] +-- this is a dsimp lemma +@[simp, nolint simpNF] theorem tensorDistribEquiv_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) (B₁ ⊗ₜ[R] B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') From 6a10f7e0ea4443314d699f82ab483bd9d6da8750 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Mon, 14 Aug 2023 23:08:42 +0000 Subject: [PATCH 36/37] fix errors --- .../LinearAlgebra/BilinearForm/TensorProduct.lean | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index 13ce8a2c3c5d09..be769d09356533 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -69,12 +69,14 @@ protected def tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : BilinFo attribute [ext] TensorProduct.ext in /-- A tensor product of symmetric bilinear forms is symmetric. -/ -lemma IsSymm.tmul {B₁ : BilinForm R M₁} {B₂ : BilinForm R M₂} +lemma IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂} (hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul B₂).IsSymm := by rw [isSymm_iff_flip R] apply toLin.injective ext x₁ x₂ y₁ y₂ - exact (congr_arg₂ (HMul.hMul) (hB₁ x₁ y₁) (hB₂ x₂ y₂)).symm + exact (congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁)).symm + +variable (A) /-- The base change of a bilinear form. -/ protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) := @@ -83,9 +85,13 @@ protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) := @[simp] theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : M₂) (a' : A) (m₂' : M₂) : - B₂.baseChange (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') := + B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') := rfl +/-- The base change of a symmetric bilinear form is symmetric. -/ +lemma IsSymm.baseChange {B₂ : BilinForm R M₂} (hB₂ : B₂.IsSymm) : (B₂.baseChange A).IsSymm := + IsSymm.tmul mul_comm hB₂ + end CommSemiring section CommRing From 17f4289c368de6cf17a88861ded9a141ce89daa9 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Thu, 17 Aug 2023 12:52:13 +0000 Subject: [PATCH 37/37] review comments --- .../BilinearForm/TensorProduct.lean | 20 ++++++++++--------- Mathlib/LinearAlgebra/Dual.lean | 1 - 2 files changed, 11 insertions(+), 10 deletions(-) diff --git a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean index be769d09356533..71fd73cfcb637e 100644 --- a/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean +++ b/Mathlib/LinearAlgebra/BilinearForm/TensorProduct.lean @@ -37,10 +37,11 @@ variable [Algebra R A] [Module R M₁] [Module A M₁] variable [SMulCommClass R A M₁] [SMulCommClass A R M₁] [IsScalarTower R A M₁] variable [Module R M₂] +variable (R A) in /-- The tensor product of two bilinear forms injects into bilinear forms on tensor products. -Note this is heterobasic; the bilinear form on the left can take values in a larger ring than -the one on the right. -/ +Note this is heterobasic; the bilinear form on the left can take values in an (commutative) algebra +over the ring in which the right bilinear form is valued. -/ def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm A (M₁ ⊗[R] M₂) := ((TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R A M₁ M₂ M₁ M₂).dualMap ≪≫ₗ (TensorProduct.lift.equiv A (M₁ ⊗[R] M₂) (M₁ ⊗[R] M₂) A).symm @@ -56,7 +57,7 @@ def tensorDistrib : BilinForm A M₁ ⊗[R] BilinForm R M₂ →ₗ[A] BilinForm @[simp] theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : - tensorDistrib (A := A) (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + tensorDistrib R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₂ m₂ m₂' • B₁ m₁ m₁' := rfl #align bilin_form.tensor_distrib_tmul BilinForm.tensorDistrib_tmulₓ @@ -64,7 +65,7 @@ theorem tensorDistrib_tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) ( /-- The tensor product of two bilinear forms, a shorthand for dot notation. -/ @[reducible] protected def tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : BilinForm A (M₁ ⊗[R] M₂) := - tensorDistrib (A := A) (B₁ ⊗ₜ[R] B₂) + tensorDistrib R A (B₁ ⊗ₜ[R] B₂) #align bilin_form.tmul BilinForm.tmul attribute [ext] TensorProduct.ext in @@ -76,8 +77,7 @@ lemma IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂} ext x₁ x₂ y₁ y₂ exact (congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁)).symm -variable (A) - +variable (A) in /-- The base change of a bilinear form. -/ protected def baseChange (B : BilinForm R M₂) : BilinForm A (A ⊗[R] M₂) := BilinForm.tmul (R := R) (A := A) (M₁ := A) (M₂ := M₂) (LinearMap.toBilin <| LinearMap.mul A A) B @@ -88,6 +88,7 @@ theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : M₂) B₂.baseChange A (a ⊗ₜ m₂) (a' ⊗ₜ m₂') = (B₂ m₂ m₂') • (a * a') := rfl +variable (A) in /-- The base change of a symmetric bilinear form is symmetric. -/ lemma IsSymm.baseChange {B₂ : BilinForm R M₂} (hB₂ : B₂.IsSymm) : (B₂.baseChange A).IsSymm := IsSymm.tmul mul_comm hB₂ @@ -108,6 +109,7 @@ variable [Module.Free R M₂] [Module.Finite R M₂] variable [Nontrivial R] +variable (R) in /-- `tensorDistrib` as an equivalence. -/ noncomputable def tensorDistribEquiv : BilinForm R M₁ ⊗[R] BilinForm R M₂ ≃ₗ[R] BilinForm R (M₁ ⊗[R] M₂) := @@ -124,7 +126,7 @@ noncomputable def tensorDistribEquiv : @[simp, nolint simpNF] theorem tensorDistribEquiv_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂) (m₁' : M₁) (m₂' : M₂) : - tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) (B₁ ⊗ₜ[R] B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') + tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) (B₁ ⊗ₜ[R] B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂') = B₁ m₁ m₁' * B₂ m₂ m₂' := rfl @@ -132,7 +134,7 @@ variable (R M₁ M₂) in -- TODO: make this `rfl` @[simp] theorem tensorDistribEquiv_toLinearMap : - (tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib (A := R) := by + (tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib R R := by ext B₁ B₂ : 3 apply toLin.injective ext @@ -140,7 +142,7 @@ theorem tensorDistribEquiv_toLinearMap : @[simp] theorem tensorDistribEquiv_apply (B : BilinForm R M₁ ⊗ BilinForm R M₂) : - tensorDistribEquiv (R := R) (M₁ := M₁) (M₂ := M₂) B = tensorDistrib (A := R) B := + tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) B = tensorDistrib R R B := FunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B #align bilin_form.tensor_distrib_equiv_apply BilinForm.tensorDistribEquiv_apply diff --git a/Mathlib/LinearAlgebra/Dual.lean b/Mathlib/LinearAlgebra/Dual.lean index 9022db855a1b41..a17beaf3ee1bd4 100644 --- a/Mathlib/LinearAlgebra/Dual.lean +++ b/Mathlib/LinearAlgebra/Dual.lean @@ -1610,7 +1610,6 @@ theorem dualDistrib_apply (f : Dual R M) (g : Dual R N) (m : M) (n : N) : end namespace AlgebraTensorModule -set_option autoImplicit false variable [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M] [AddCommMonoid N] variable [Module R M] [Module A M] [Module R N] [IsScalarTower R A M]