From eaa358a61641316ddafb4b903b0ddb0b9ebb6a5b Mon Sep 17 00:00:00 2001 From: Buster Copley Date: Fri, 27 Oct 2023 15:47:54 +0000 Subject: [PATCH] feat: Nontrivial instances for ExteriorAlgebra, CliffordAlgebra (#7985) Using methods suggested by @eric-wieser [Zulip discussion](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Nontrivial.20algebras) --- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean | 4 ++++ Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean | 4 ++++ 2 files changed, 8 insertions(+) diff --git a/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean b/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean index d354eca2d3092..5ce702ad50ec2 100644 --- a/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean +++ b/Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean @@ -399,4 +399,8 @@ def equivExterior [Invertible (2 : R)] : CliffordAlgebra Q ≃ₗ[R] ExteriorAlg changeFormEquiv changeForm.associated_neg_proof #align clifford_algebra.equiv_exterior CliffordAlgebra.equivExterior +/-- A `CliffordAlgebra` over a nontrivial ring is nontrivial, in characteristic not two. -/ +instance [Nontrivial R] [Invertible (2 : R)] : + Nontrivial (CliffordAlgebra Q) := (equivExterior Q).symm.injective.nontrivial + end CliffordAlgebra diff --git a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean index f126bfc12a2ab..224094e5a2c73 100644 --- a/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean +++ b/Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean @@ -333,6 +333,10 @@ theorem ιMulti_succ_curryLeft {n : ℕ} (m : M) : rfl #align exterior_algebra.ι_multi_succ_curry_left ExteriorAlgebra.ιMulti_succ_curryLeft +/-- An `ExteriorAlgebra` over a nontrivial ring is nontrivial. -/ +instance [Nontrivial R] : Nontrivial (ExteriorAlgebra R M) := + (algebraMap_leftInverse M).injective.nontrivial + end ExteriorAlgebra namespace TensorAlgebra