Skip to content

Commit 1157b75

Browse files
eric-wieserkim-em
eric-wieser
authored and
kim-em
committed
chore: split RingTheory/TensorProduct (#6187)
There is a reasonably-sized section on modules over two rings before we actual reach tensor products of rings. The motivation for splitting here is to make room for the results in #6035. The declarations are copied without modification, the module docstring has been adapted.
1 parent cefb357 commit 1157b75

4 files changed

Lines changed: 208 additions & 191 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2236,6 +2236,7 @@ import Mathlib.LinearAlgebra.TensorAlgebra.ToTensorPower
22362236
import Mathlib.LinearAlgebra.TensorPower
22372237
import Mathlib.LinearAlgebra.TensorProduct
22382238
import Mathlib.LinearAlgebra.TensorProduct.Matrix
2239+
import Mathlib.LinearAlgebra.TensorProduct.Tower
22392240
import Mathlib.LinearAlgebra.TensorProductBasis
22402241
import Mathlib.LinearAlgebra.Trace
22412242
import Mathlib.LinearAlgebra.UnitaryGroup

‎Mathlib/Algebra/Lie/Weights.lean‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ import Mathlib.Algebra.Lie.Character
99
import Mathlib.Algebra.Lie.Engel
1010
import Mathlib.Algebra.Lie.CartanSubalgebra
1111
import Mathlib.LinearAlgebra.Eigenspace.Basic
12-
import Mathlib.RingTheory.TensorProduct
12+
import Mathlib.LinearAlgebra.TensorProduct.Tower
1313

1414
#align_import algebra.lie.weights from "leanprover-community/mathlib"@"6b0169218d01f2837d79ea2784882009a0da1aa1"
1515

‎Mathlib/LinearAlgebra/TensorProduct/Tower.lean‎

Lines changed: 205 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,205 @@
1+
/-
2+
Copyright (c) 2020 Scott Morrison. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Scott Morrison, Johan Commelin
5+
-/
6+
import Mathlib.LinearAlgebra.TensorProduct
7+
import Mathlib.Algebra.Algebra.Tower
8+
9+
#align_import ring_theory.tensor_product from "leanprover-community/mathlib"@"88fcdc3da43943f5b01925deddaa5bf0c0e85e4e"
10+
11+
/-!
12+
# The `A`-module structure on `M ⊗[R] N`
13+
14+
When `M` is both an `R`-module and an `A`-module, and `Algebra R A`, then many of the morphisms
15+
preserve the actions by `A`.
16+
17+
This file provides more general versions of the definitions already in
18+
`LinearAlgebra/TensorProduct`.
19+
20+
## Main definitions
21+
22+
* `TensorProduct.AlgebraTensorModule.curry`
23+
* `TensorProduct.AlgebraTensorModule.uncurry`
24+
* `TensorProduct.AlgebraTensorModule.lcurry`
25+
* `TensorProduct.AlgebraTensorModule.lift`
26+
* `TensorProduct.AlgebraTensorModule.lift.equiv`
27+
* `TensorProduct.AlgebraTensorModule.mk`
28+
* `TensorProduct.AlgebraTensorModule.assoc`
29+
30+
## Implementation notes
31+
32+
We could thus consider replacing the less general definitions with these ones. If we do this, we
33+
probably should still implement the less general ones as abbreviations to the more general ones with
34+
fewer type arguments.
35+
-/
36+
37+
namespace TensorProduct
38+
39+
namespace AlgebraTensorModule
40+
41+
variable {R A M N P : Type _}
42+
43+
open LinearMap
44+
open Algebra (lsmul)
45+
46+
section Semiring
47+
48+
variable [CommSemiring R] [Semiring A] [Algebra R A]
49+
50+
variable [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M]
51+
52+
variable [AddCommMonoid N] [Module R N]
53+
54+
variable [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P]
55+
56+
theorem smul_eq_lsmul_rTensor (a : A) (x : M ⊗[R] N) : a • x = (lsmul R M a).rTensor N x :=
57+
rfl
58+
#align tensor_product.algebra_tensor_module.smul_eq_lsmul_rtensor TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor
59+
60+
/-- Heterobasic version of `TensorProduct.curry`:
61+
62+
Given a linear map `M ⊗[R] N →[A] P`, compose it with the canonical
63+
bilinear map `M →[A] N →[R] M ⊗[R] N` to form a bilinear map `M →[A] N →[R] P`. -/
64+
@[simps]
65+
nonrec def curry (f : M ⊗[R] N →ₗ[A] P) : M →ₗ[A] N →ₗ[R] P :=
66+
{ curry (f.restrictScalars R) with
67+
toFun := curry (f.restrictScalars R)
68+
map_smul' := fun c x => LinearMap.ext fun y => f.map_smul c (x ⊗ₜ y) }
69+
#align tensor_product.algebra_tensor_module.curry TensorProduct.AlgebraTensorModule.curry
70+
#align tensor_product.algebra_tensor_module.curry_apply TensorProduct.AlgebraTensorModule.curry_apply
71+
72+
theorem restrictScalars_curry (f : M ⊗[R] N →ₗ[A] P) :
73+
restrictScalars R (curry f) = TensorProduct.curry (f.restrictScalars R) :=
74+
rfl
75+
#align tensor_product.algebra_tensor_module.restrict_scalars_curry TensorProduct.AlgebraTensorModule.restrictScalars_curry
76+
77+
/-- Just as `TensorProduct.ext` is marked `ext` instead of `TensorProduct.ext'`, this is
78+
a better `ext` lemma than `TensorProduct.AlgebraTensorModule.ext` below.
79+
80+
See note [partially-applied ext lemmas]. -/
81+
@[ext high]
82+
nonrec theorem curry_injective : Function.Injective (curry : (M ⊗ N →ₗ[A] P) → M →ₗ[A] N →ₗ[R] P) :=
83+
fun _ _ h =>
84+
LinearMap.restrictScalars_injective R <|
85+
curry_injective <| (congr_arg (LinearMap.restrictScalars R) h : _)
86+
#align tensor_product.algebra_tensor_module.curry_injective TensorProduct.AlgebraTensorModule.curry_injective
87+
88+
theorem ext {g h : M ⊗[R] N →ₗ[A] P} (H : ∀ x y, g (x ⊗ₜ y) = h (x ⊗ₜ y)) : g = h :=
89+
curry_injective <| LinearMap.ext₂ H
90+
#align tensor_product.algebra_tensor_module.ext TensorProduct.AlgebraTensorModule.ext
91+
92+
end Semiring
93+
94+
section CommSemiring
95+
96+
variable [CommSemiring R] [CommSemiring A] [Algebra R A]
97+
98+
variable [AddCommMonoid M] [Module R M] [Module A M] [IsScalarTower R A M]
99+
100+
variable [AddCommMonoid N] [Module R N]
101+
102+
variable [AddCommMonoid P] [Module R P] [Module A P] [IsScalarTower R A P]
103+
104+
/-- Heterobasic version of `TensorProduct.lift`:
105+
106+
Constructing a linear map `M ⊗[R] N →[A] P` given a bilinear map `M →[A] N →[R] P` with the
107+
property that its composition with the canonical bilinear map `M →[A] N →[R] M ⊗[R] N` is
108+
the given bilinear map `M →[A] N →[R] P`. -/
109+
nonrec def lift (f : M →ₗ[A] N →ₗ[R] P) : M ⊗[R] N →ₗ[A] P :=
110+
{ lift (f.restrictScalars R) with
111+
map_smul' := fun c =>
112+
show
113+
∀ x : M ⊗[R] N,
114+
(lift (f.restrictScalars R)).comp (lsmul R _ c) x =
115+
(lsmul R _ c).comp (lift (f.restrictScalars R)) x
116+
from
117+
ext_iff.1 <|
118+
TensorProduct.ext' fun x y => by
119+
simp only [comp_apply, Algebra.lsmul_coe, smul_tmul', lift.tmul,
120+
coe_restrictScalars, f.map_smul, smul_apply] }
121+
#align tensor_product.algebra_tensor_module.lift TensorProduct.AlgebraTensorModule.lift
122+
123+
-- Porting note: autogenerated lemma unfolded to `liftAux`
124+
@[simp]
125+
theorem lift_apply (f : M →ₗ[A] N →ₗ[R] P) (a : M ⊗[R] N) :
126+
AlgebraTensorModule.lift f a = TensorProduct.lift (LinearMap.restrictScalars R f) a :=
127+
rfl
128+
129+
@[simp]
130+
theorem lift_tmul (f : M →ₗ[A] N →ₗ[R] P) (x : M) (y : N) : lift f (x ⊗ₜ y) = f x y :=
131+
rfl
132+
#align tensor_product.algebra_tensor_module.lift_tmul TensorProduct.AlgebraTensorModule.lift_tmul
133+
134+
variable (R A M N P)
135+
136+
/-- Heterobasic version of `TensorProduct.uncurry`:
137+
138+
Linearly constructing a linear map `M ⊗[R] N →[A] P` given a bilinear map `M →[A] N →[R] P`
139+
with the property that its composition with the canonical bilinear map `M →[A] N →[R] M ⊗[R] N` is
140+
the given bilinear map `M →[A] N →[R] P`. -/
141+
@[simps]
142+
def uncurry : (M →ₗ[A] N →ₗ[R] P) →ₗ[A] M ⊗[R] N →ₗ[A] P where
143+
toFun := lift
144+
map_add' _ _ := ext fun x y => by simp only [lift_tmul, add_apply]
145+
map_smul' _ _ := ext fun x y => by simp only [lift_tmul, smul_apply, RingHom.id_apply]
146+
#align tensor_product.algebra_tensor_module.uncurry TensorProduct.AlgebraTensorModule.uncurry
147+
148+
/-- Heterobasic version of `TensorProduct.lcurry`:
149+
150+
Given a linear map `M ⊗[R] N →[A] P`, compose it with the canonical
151+
bilinear map `M →[A] N →[R] M ⊗[R] N` to form a bilinear map `M →[A] N →[R] P`. -/
152+
@[simps]
153+
def lcurry : (M ⊗[R] N →ₗ[A] P) →ₗ[A] M →ₗ[A] N →ₗ[R] P where
154+
toFun := curry
155+
map_add' _ _ := rfl
156+
map_smul' _ _ := rfl
157+
#align tensor_product.algebra_tensor_module.lcurry TensorProduct.AlgebraTensorModule.lcurry
158+
159+
/-- Heterobasic version of `TensorProduct.lift.equiv`:
160+
161+
A linear equivalence constructing a linear map `M ⊗[R] N →[A] P` given a
162+
bilinear map `M →[A] N →[R] P` with the property that its composition with the
163+
canonical bilinear map `M →[A] N →[R] M ⊗[R] N` is the given bilinear map `M →[A] N →[R] P`. -/
164+
def lift.equiv : (M →ₗ[A] N →ₗ[R] P) ≃ₗ[A] M ⊗[R] N →ₗ[A] P :=
165+
LinearEquiv.ofLinear (uncurry R A M N P) (lcurry R A M N P)
166+
(LinearMap.ext fun _ => ext fun x y => lift_tmul _ x y)
167+
(LinearMap.ext fun f => LinearMap.ext fun x => LinearMap.ext fun y => lift_tmul f x y)
168+
#align tensor_product.algebra_tensor_module.lift.equiv TensorProduct.AlgebraTensorModule.lift.equiv
169+
170+
/-- Heterobasic version of `TensorProduct.mk`:
171+
172+
The canonical bilinear map `M →[A] N →[R] M ⊗[R] N`. -/
173+
@[simps! apply]
174+
nonrec def mk : M →ₗ[A] N →ₗ[R] M ⊗[R] N :=
175+
{ mk R M N with map_smul' := fun _ _ => rfl }
176+
#align tensor_product.algebra_tensor_module.mk TensorProduct.AlgebraTensorModule.mk
177+
#align tensor_product.algebra_tensor_module.mk_apply TensorProduct.AlgebraTensorModule.mk_apply
178+
179+
attribute [local ext high] TensorProduct.ext
180+
181+
/-- Heterobasic version of `TensorProduct.assoc`:
182+
183+
Linear equivalence between `(M ⊗[A] N) ⊗[R] P` and `M ⊗[A] (N ⊗[R] P)`. -/
184+
def assoc : (M ⊗[A] P) ⊗[R] N ≃ₗ[A] M ⊗[A] P ⊗[R] N :=
185+
LinearEquiv.ofLinear
186+
(lift <|
187+
TensorProduct.uncurry A _ _ _ <| comp (lcurry R A _ _ _) <| TensorProduct.mk A M (P ⊗[R] N))
188+
(TensorProduct.uncurry A _ _ _ <|
189+
comp (uncurry R A _ _ _) <| by
190+
apply TensorProduct.curry
191+
exact mk R A _ _)
192+
(by
193+
ext
194+
rfl)
195+
(by
196+
ext
197+
-- porting note: was `simp only [...]`
198+
rfl)
199+
#align tensor_product.algebra_tensor_module.assoc TensorProduct.AlgebraTensorModule.assoc
200+
201+
end CommSemiring
202+
203+
end AlgebraTensorModule
204+
205+
end TensorProduct

0 commit comments

Comments
 (0)