-
Notifications
You must be signed in to change notification settings - Fork 299
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat(linear_algebra/contraction): define contraction maps between a m…
…odule and its dual (#1973) * feat(linear_algebra/contraction): define contraction maps between a module and its dual * Implicit carrier types for smul_comm * Add comment with license and file description * Build on top of extant linear_map.smul_right * Feedback from code review Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
- Loading branch information
1 parent
4299a80
commit b373dae
Showing
3 changed files
with
72 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,55 @@ | ||
/- | ||
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.tensor_product | ||
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 | ||
|
||
set_option class.instance_max_depth 42 | ||
|
||
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.id.flip | ||
|
||
/-- 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 |