feat(linear_algebra/contraction): define contraction maps between a module 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>

Author: 3 people

src/group_theory/group_action.lean

@@ -28,6 +28,9 @@ theorem mul_smul (a₁ a₂ : α) (b : β) : (a₁ * a₂) • b = a₁ • a₂
 
 lemma smul_smul (a₁ a₂ : α) (b : β) : a₁ • a₂ • b = (a₁ * a₂) • b := (mul_smul _ _ _).symm
 
+lemma smul_comm {α : Type u} {β : Type v} [comm_monoid α] [mul_action α β] (a₁ a₂ : α) (b : β) :
+  a₁ • a₂ • b = a₂ • a₁ • b := by rw [←mul_smul, ←mul_smul, mul_comm]
+
 variable (α)
 @[simp] theorem one_smul (b : β) : (1 : α) • b = b := mul_action.one_smul α _
 

src/linear_algebra/basic.lean

@@ -302,6 +302,20 @@ rfl
 theorem comp_smul (g : M₂ →ₗ[R] M₃) (a : R) : g.comp (a • f) = a • (g.comp f) :=
 ext $ assume b, by rw [comp_apply, smul_apply, g.map_smul]; refl
 
+/--
+The family of linear maps `M₂ → M` parameterised by `f ∈ M₂ → R`, `x ∈ M`, is linear in `f`, `x`.
+-/
+def smul_rightₗ : (M₂ →ₗ[R] R) →ₗ[R] M →ₗ[R] M₂ →ₗ[R] M :=
+{ to_fun := λ f, {
+    to_fun := linear_map.smul_right f,
+    add    := λ m m', by { ext, apply smul_add, },
+    smul   := λ c m, by { ext, apply smul_comm, } },
+  add    := λ f f', by { ext, apply add_smul, },
+  smul   := λ c f, by { ext, apply mul_smul, } }
+
+@[simp] lemma smul_rightₗ_apply (f : M₂ →ₗ[R] R) (x : M) (c : M₂) :
+  (smul_rightₗ : (M₂ →ₗ R) →ₗ M →ₗ M₂ →ₗ M) f x c = (f c) • x := rfl
+
 end comm_ring
 end linear_map
 

src/linear_algebra/contraction.lean

@@ -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