feat(linear_algebra/{exterior,tensor}_algebra): Prove that ι is inj…

…ective (#5712)

This strategy can't be used on `clifford_algebra`, and the obvious guess of trying to define a `less_triv_sq_quadratic_form_ext` leads to a non-associative multiplication; so for now, we just handle these two cases.



Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

src/linear_algebra/exterior_algebra.lean

@@ -162,6 +162,15 @@ 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)
+
 @[simp]
 lemma ι_add_mul_swap (x y : M) : ι R x * ι R y + ι R y * ι R x = 0 :=
 calc _ = ι R (x + y) * ι R (x + y) : by simp [mul_add, add_mul]

src/linear_algebra/tensor_algebra.lean

@@ -5,6 +5,7 @@ Author: Adam Topaz.
 -/
 import algebra.free_algebra
 import algebra.ring_quot
+import algebra.triv_sq_zero_ext
 
 /-!
 # Tensor Algebras
@@ -121,4 +122,13 @@ 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)
+
 end tensor_algebra