-
Notifications
You must be signed in to change notification settings - Fork 259
/
TensorProduct.lean
146 lines (115 loc) · 5.75 KB
/
TensorProduct.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
/-
Copyright (c) 2023 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser
-/
import Mathlib.LinearAlgebra.Dual
import Mathlib.LinearAlgebra.TensorProduct.Tower
#align_import linear_algebra.bilinear_form.tensor_product from "leanprover-community/mathlib"@"f0c8bf9245297a541f468be517f1bde6195105e9"
/-!
# The bilinear form on a tensor product
## Main definitions
* `LinearMap.BilinForm.tensorDistrib (B₁ ⊗ₜ B₂)`: the bilinear form on `M₁ ⊗ M₂` constructed by
applying `B₁` on `M₁` and `B₂` on `M₂`.
* `LinearMap.BilinForm.tensorDistribEquiv`: `BilinForm.tensorDistrib` as an equivalence on finite
free modules.
-/
suppress_compilation
universe u v w uι uR uA uM₁ uM₂
variable {ι : Type uι} {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂}
open TensorProduct
namespace LinearMap
namespace BilinForm
open LinearMap (BilinForm)
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₁] [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 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).toLinearMap
∘ₗ TensorProduct.AlgebraTensorModule.dualDistrib R _ _ _
∘ₗ (TensorProduct.AlgebraTensorModule.congr
(TensorProduct.lift.equiv A M₁ M₁ A)
(TensorProduct.lift.equiv R _ _ _)).toLinearMap
#align bilin_form.tensor_distrib LinearMap.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 R A (B₁ ⊗ₜ B₂) (m₁ ⊗ₜ m₂) (m₁' ⊗ₜ m₂')
= B₂ m₂ m₂' • B₁ m₁ m₁' :=
rfl
#align bilin_form.tensor_distrib_tmul LinearMap.BilinForm.tensorDistrib_tmulₓ
/-- The tensor product of two bilinear forms, a shorthand for dot notation. -/
protected abbrev tmul (B₁ : BilinForm A M₁) (B₂ : BilinForm R M₂) : BilinForm A (M₁ ⊗[R] M₂) :=
tensorDistrib R A (B₁ ⊗ₜ[R] B₂)
#align bilin_form.tmul LinearMap.BilinForm.tmul
attribute [local ext] TensorProduct.ext in
/-- A tensor product of symmetric bilinear forms is symmetric. -/
lemma _root_.LinearMap.IsSymm.tmul {B₁ : BilinForm A M₁} {B₂ : BilinForm R M₂}
(hB₁ : B₁.IsSymm) (hB₂ : B₂.IsSymm) : (B₁.tmul B₂).IsSymm := by
rw [LinearMap.isSymm_iff_eq_flip]
ext x₁ x₂ y₁ y₂
exact congr_arg₂ (HSMul.hSMul) (hB₂ x₂ y₂) (hB₁ x₁ y₁)
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.mul A A) B
@[simp]
theorem baseChange_tmul (B₂ : BilinForm R M₂) (a : A) (m₂ : 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₂
end CommSemiring
section CommRing
variable [CommRing R]
variable [AddCommGroup M₁] [AddCommGroup M₂]
variable [Module R M₁] [Module R M₂]
variable [Module.Free R M₁] [Module.Finite R M₁]
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₂) :=
-- the same `LinearEquiv`s as from `tensorDistrib`,
-- but with the inner linear map also as an equiv
TensorProduct.congr (TensorProduct.lift.equiv R _ _ _) (TensorProduct.lift.equiv R _ _ _) ≪≫ₗ
TensorProduct.dualDistribEquiv R (M₁ ⊗ M₁) (M₂ ⊗ M₂) ≪≫ₗ
(TensorProduct.tensorTensorTensorComm R _ _ _ _).dualMap ≪≫ₗ
(TensorProduct.lift.equiv R _ _ _).symm
#align bilin_form.tensor_distrib_equiv LinearMap.BilinForm.tensorDistribEquiv
@[simp]
theorem tensorDistribEquiv_tmul (B₁ : BilinForm R M₁) (B₂ : BilinForm R M₂) (m₁ : M₁) (m₂ : M₂)
(m₁' : M₁) (m₂' : M₂) :
tensorDistribEquiv 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 (M₁ := M₁) (M₂ := M₂)).toLinearMap = tensorDistrib R R := by
ext B₁ B₂ : 3
ext
exact mul_comm _ _
@[simp]
theorem tensorDistribEquiv_apply (B : BilinForm R M₁ ⊗ BilinForm R M₂) :
tensorDistribEquiv R (M₁ := M₁) (M₂ := M₂) B = tensorDistrib R R B :=
DFunLike.congr_fun (tensorDistribEquiv_toLinearMap R M₁ M₂) B
#align bilin_form.tensor_distrib_equiv_apply LinearMap.BilinForm.tensorDistribEquiv_apply
end CommRing
end BilinForm
end LinearMap