From 3b8cfdc905c663f3d99acac325c7dff1a0ce744c Mon Sep 17 00:00:00 2001
From: Eric Wieser <wieser.eric@gmail.com>
Date: Thu, 14 Jan 2021 19:06:16 +0000
Subject: [PATCH] =?UTF-8?q?feat(linear=5Falgebra/{exterior,tensor,free}=5F?=
 =?UTF-8?q?algebra):=20provide=20left-inverses=20for=20`algebra=5Fmap`=20a?=
 =?UTF-8?q?nd=20`=CE=B9`=20(#5722)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The strategy used for `algebra_map` here can't be used on `clifford_algebra` as the zero map does not satisfy `f m * f m = Q m`.
---
 src/algebra/free_algebra.lean            |  8 ++++++++
 src/algebra/triv_sq_zero_ext.lean        |  7 +++++++
 src/linear_algebra/exterior_algebra.lean | 26 ++++++++++++++++--------
 src/linear_algebra/tensor_algebra.lean   | 25 +++++++++++++++--------
 4 files changed, 50 insertions(+), 16 deletions(-)

diff --git a/src/algebra/free_algebra.lean b/src/algebra/free_algebra.lean
index f4af376ed9a3d..0ca3d00a82aea 100644
--- a/src/algebra/free_algebra.lean
+++ b/src/algebra/free_algebra.lean
@@ -326,6 +326,14 @@ equiv_monoid_algebra_free_monoid.to_equiv.nontrivial
 section
 open_locale classical
 
+/-- The left-inverse of `algebra_map`. -/
+def algebra_map_inv : free_algebra R X →ₐ[R] R :=
+lift R (0 : X → R)
+
+lemma algebra_map_left_inverse :
+  function.left_inverse algebra_map_inv (algebra_map R $ free_algebra R X) :=
+λ x, by simp [algebra_map_inv]
+
 -- this proof is copied from the approach in `free_abelian_group.of_injective`
 lemma ι_injective [nontrivial R] : function.injective (ι R : X → free_algebra R X) :=
 λ x y hoxy, classical.by_contradiction $ assume hxy : x ≠ y,
diff --git a/src/algebra/triv_sq_zero_ext.lean b/src/algebra/triv_sq_zero_ext.lean
index df973b9a6dc03..f4756853d9b78 100644
--- a/src/algebra/triv_sq_zero_ext.lean
+++ b/src/algebra/triv_sq_zero_ext.lean
@@ -270,6 +270,13 @@ def fst_hom [comm_semiring R] [add_comm_monoid M] [semimodule R M] : tsze R M 
   map_add' := fst_add R M,
   commutes' := fst_inl }
 
+/-- The canonical `R`-module projection `triv_sq_zero_ext R M → M`. -/
+@[simps apply]
+def snd_hom [semiring R] [add_comm_monoid M] [semimodule R M] : tsze R M →ₗ[R] M :=
+{ to_fun := snd,
+  map_add' := snd_add R M,
+  map_smul' := snd_smul R M}
+
 end algebra
 
 end triv_sq_zero_ext
diff --git a/src/linear_algebra/exterior_algebra.lean b/src/linear_algebra/exterior_algebra.lean
index 2213994692fcf..a028bf7e81eb6 100644
--- a/src/linear_algebra/exterior_algebra.lean
+++ b/src/linear_algebra/exterior_algebra.lean
@@ -162,14 +162,24 @@ begin
   simp only [h],
 end
 
-lemma ι_injective : function.injective (ι R : M → exterior_algebra R M) :=
--- This is essentially the same proof as `tensor_algebra.ι_injective`
-λ x y hxy,
-  let f : exterior_algebra R M →ₐ[R] triv_sq_zero_ext R M := lift R
-    ⟨triv_sq_zero_ext.inr_hom R M, λ m, triv_sq_zero_ext.inr_mul_inr R _ m m⟩ in
-  have hfxx : f (ι R x) = triv_sq_zero_ext.inr x := lift_ι_apply _ _ _ _,
-  have hfyy : f (ι R y) = triv_sq_zero_ext.inr y := lift_ι_apply _ _ _ _,
-  triv_sq_zero_ext.inr_injective $ hfxx.symm.trans ((f.congr_arg hxy).trans hfyy)
+/-- The left-inverse of `algebra_map`. -/
+def algebra_map_inv : exterior_algebra R M →ₐ[R] R :=
+exterior_algebra.lift R ⟨(0 : M →ₗ[R] R), λ m, by simp⟩
+
+lemma algebra_map_left_inverse :
+  function.left_inverse algebra_map_inv (algebra_map R $ exterior_algebra R M) :=
+λ x, by simp [algebra_map_inv]
+
+/-- The left-inverse of `ι`.
+
+As an implementation detail, we implement this using `triv_sq_zero_ext` which has a suitable
+algebra structure. -/
+def ι_inv : exterior_algebra R M →ₗ[R] M :=
+(triv_sq_zero_ext.snd_hom R M).comp
+  (lift R ⟨triv_sq_zero_ext.inr_hom R M, λ m, triv_sq_zero_ext.inr_mul_inr R _ m m⟩).to_linear_map
+
+lemma ι_left_inverse : function.left_inverse ι_inv (ι R : M → exterior_algebra R M) :=
+λ x, by simp [ι_inv]
 
 @[simp]
 lemma ι_add_mul_swap (x y : M) : ι R x * ι R y + ι R y * ι R x = 0 :=
diff --git a/src/linear_algebra/tensor_algebra.lean b/src/linear_algebra/tensor_algebra.lean
index 044a09e408a06..70a4b42ce15a9 100644
--- a/src/linear_algebra/tensor_algebra.lean
+++ b/src/linear_algebra/tensor_algebra.lean
@@ -122,13 +122,22 @@ begin
   exact (lift R).symm.injective w,
 end
 
-lemma ι_injective : function.injective (ι R : M → tensor_algebra R M) :=
--- `triv_sq_zero_ext` has a suitable algebra structure and existing proof of injectivity, which
--- we can transfer
-λ x y hxy,
-  let f : tensor_algebra R M →ₐ[R] triv_sq_zero_ext R M := lift R (triv_sq_zero_ext.inr_hom R M) in
-  have hfxx : f (ι R x) = triv_sq_zero_ext.inr x := lift_ι_apply _ _,
-  have hfyy : f (ι R y) = triv_sq_zero_ext.inr y := lift_ι_apply _ _,
-  triv_sq_zero_ext.inr_injective $ hfxx.symm.trans ((f.congr_arg hxy).trans hfyy)
+/-- The left-inverse of `algebra_map`. -/
+def algebra_map_inv : tensor_algebra R M →ₐ[R] R :=
+lift R (0 : M →ₗ[R] R)
+
+lemma algebra_map_left_inverse :
+  function.left_inverse algebra_map_inv (algebra_map R $ tensor_algebra R M) :=
+λ x, by simp [algebra_map_inv]
+
+/-- The left-inverse of `ι`.
+
+As an implementation detail, we implement this using `triv_sq_zero_ext` which has a suitable
+algebra structure. -/
+def ι_inv : tensor_algebra R M →ₗ[R] M :=
+(triv_sq_zero_ext.snd_hom R M).comp (lift R (triv_sq_zero_ext.inr_hom R M)).to_linear_map
+
+lemma ι_left_inverse : function.left_inverse ι_inv (ι R : M → tensor_algebra R M) :=
+λ x, by simp [ι_inv]
 
 end tensor_algebra