This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 298
/
contraction.lean
54 lines (38 loc) · 1.78 KB
/
contraction.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
/-
Copyright (c) 2020 Oliver Nash. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Oliver Nash
-/
import linear_algebra.dual
/-!
# Contractions
Given modules $M, N$ over a commutative ring $R$, this file defines the natural linear maps:
$M^* \otimes M \to R$, $M \otimes M^* \to R$, and $M^* \otimes N → Hom(M, N)$, as well as proving
some basic properties of these maps.
## Tags
contraction, dual module, tensor product
-/
universes u v
section contraction
open tensor_product
open_locale tensor_product
variables (R : Type u) (M N : Type v)
variables [comm_ring R] [add_comm_group M] [add_comm_group N] [module R M] [module R N]
/-- The natural left-handed pairing between a module and its dual. -/
def contract_left : (module.dual R M) ⊗ M →ₗ[R] R := (uncurry _ _ _ _).to_fun linear_map.id
/-- The natural right-handed pairing between a module and its dual. -/
def contract_right : M ⊗ (module.dual R M) →ₗ[R] R :=
(uncurry _ _ _ _).to_fun (linear_map.flip linear_map.id)
/-- The natural map associating a linear map to the tensor product of two modules. -/
def dual_tensor_hom : (module.dual R M) ⊗ N →ₗ M →ₗ N :=
let M' := module.dual R M in
(uncurry R M' N (M →ₗ[R] N) : _ → M' ⊗ N →ₗ M →ₗ N) linear_map.smul_rightₗ
variables {R M N}
@[simp] lemma contract_left_apply (f : module.dual R M) (m : M) :
contract_left R M (f ⊗ₜ m) = f m := by apply uncurry_apply
@[simp] lemma contract_right_apply (f : module.dual R M) (m : M) :
contract_right R M (m ⊗ₜ f) = f m := by apply uncurry_apply
@[simp] lemma dual_tensor_hom_apply (f : module.dual R M) (m : M) (n : N) :
dual_tensor_hom R M N (f ⊗ₜ n) m = (f m) • n :=
by { dunfold dual_tensor_hom, rw uncurry_apply, refl, }
end contraction