feat(linear_algebra/{exterior,tensor,free}_algebra): provide left-inv…

…erses for `algebra_map` and `ι` (#5722)

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

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

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

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 :=

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