feat(linear_algebra/{clifford,exterior,tensor,free}_algebra): provide…

… canonical images from larger algebras into smaller ones (#5745)

This adds:

* `free_algebra.to_tensor`
* `tensor_algebra.to_exterior`
* `tensor_algebra.to_clifford`

Providing the injection in the other direction is more challenging, so is left as future work.

src/linear_algebra/clifford_algebra.lean

@@ -165,3 +165,17 @@ alg_equiv.of_alg_hom
   (by { ext, simp, })
 
 end clifford_algebra
+
+namespace tensor_algebra
+
+variables {Q}
+
+/-- The canonical image of the `tensor_algebra` in the `clifford_algebra`, which maps
+`tensor_algebra.ι R x` to `clifford_algebra.ι Q x`. -/
+def to_clifford : tensor_algebra R M →ₐ[R] clifford_algebra Q :=
+tensor_algebra.lift R (clifford_algebra.ι Q)
+
+@[simp] lemma to_clifford_ι (m : M) : (tensor_algebra.ι R m).to_clifford = clifford_algebra.ι Q m :=
+by simp [to_clifford]
+
+end tensor_algebra

src/linear_algebra/exterior_algebra.lean

@@ -236,3 +236,17 @@ lemma ι_multi_apply {n : ℕ} (v : fin n → M) :
   ι_multi R n v = (list.of_fn $ λ i, ι R (v i)).prod := rfl
 
 end exterior_algebra
+
+namespace tensor_algebra
+
+variables {R M}
+
+/-- The canonical image of the `tensor_algebra` in the `exterior_algebra`, which maps
+`tensor_algebra.ι R x` to `exterior_algebra.ι R x`. -/
+def to_exterior : tensor_algebra R M →ₐ[R] exterior_algebra R M :=
+tensor_algebra.lift R (exterior_algebra.ι R)
+
+@[simp] lemma to_exterior_ι (m : M) : (tensor_algebra.ι R m).to_exterior = exterior_algebra.ι R m :=
+by simp [to_exterior]
+
+end tensor_algebra

src/linear_algebra/tensor_algebra.lean

@@ -141,3 +141,17 @@ lemma ι_left_inverse : function.left_inverse ι_inv (ι R : M → tensor_algebr
 λ x, by simp [ι_inv]
 
 end tensor_algebra
+
+namespace free_algebra
+
+variables {R M}
+
+/-- The canonical image of the `free_algebra` in the `tensor_algebra`, which maps
+`free_algebra.ι R x` to `tensor_algebra.ι R x`. -/
+def to_tensor : free_algebra R M →ₐ[R] tensor_algebra R M :=
+free_algebra.lift R (tensor_algebra.ι R)
+
+@[simp] lemma to_tensor_ι (m : M) : (free_algebra.ι R m).to_tensor = tensor_algebra.ι R m :=
+by simp [to_tensor]
+
+end free_algebra