feat(linear_algebra/clifford_algebra/equivs): There is a clifford alg…

…ebra isomorphic to the dual numbers (#10730)

This adds a brief file on the dual numbers, and then shows that they are equivalent to the clifford algebra with `Q = (0 : quadratic_form R R)`.

src/algebra/dual_number.lean

@@ -0,0 +1,99 @@
+/-
+Copyright (c) 2021 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+
+import algebra.triv_sq_zero_ext
+
+/-!
+# Dual numbers
+
+The dual numbers over `R` are of the form `a + bε`, where `a` and `b` are typically elements of a
+commutative ring `R`, and `ε` is a symbol satisfying `ε^2 = 0`. They are a special case of
+`triv_sq_zero_ext R M` with `M = R`.
+
+## Notation
+
+In the `dual_number` locale:
+
+* `R[ε]` is a shorthand for `dual_number R`
+* `ε` is a shorthand for `dual_number.eps`
+
+## Main definitions
+
+* `dual_number`
+* `dual_number.eps`
+* `dual_number.lift`
+
+## Implementation notes
+
+Rather than duplicating the API of `triv_sq_zero_ext`, this file reuses the functions there.
+
+## References
+
+* https://en.wikipedia.org/wiki/Dual_number
+-/
+
+variables {R : Type*}
+
+/-- The type of dual numbers, numbers of the form $a + bε$ where $ε^2 = 0$.-/
+abbreviation dual_number (R : Type*) : Type* := triv_sq_zero_ext R R
+
+/-- The unit element $ε$ that squares to zero. -/
+def dual_number.eps [has_zero R] [has_one R] : dual_number R := triv_sq_zero_ext.inr 1
+
+localized "notation `ε` := dual_number.eps" in dual_number
+localized "postfix `[ε]`:1025 := dual_number" in dual_number
+
+open_locale dual_number
+
+namespace dual_number
+
+open triv_sq_zero_ext
+
+@[simp] lemma fst_eps [has_zero R] [has_one R] : fst ε = (0 : R) := fst_inr _ _
+@[simp] lemma snd_eps [has_zero R] [has_one R] : snd ε = (1 : R) := snd_inr _ _
+
+/-- A version of `triv_sq_zero_ext.snd_mul` with `*` instead of `•`. -/
+@[simp] lemma snd_mul [semiring R] (x y : R[ε]) : snd (x * y) = fst x * snd y + fst y * snd x :=
+snd_mul _ _
+
+@[simp] lemma eps_mul_eps [semiring R] : (ε * ε : R[ε]) = 0 := inr_mul_inr _ _ _
+
+@[simp] lemma inr_eq_smul_eps [mul_zero_one_class R] (r : R) : inr r = (r • ε : R[ε]) :=
+ext (mul_zero r).symm (mul_one r).symm
+
+/-- For two algebra morphisms out of `R[ε]` to agree, it suffices for them to agree on `ε`. -/
+@[ext] lemma alg_hom_ext {A} [comm_semiring R] [semiring A] [algebra R A]
+  ⦃f g : R[ε] →ₐ[R] A⦄ (h : f ε = g ε) : f = g :=
+alg_hom_ext' $ linear_map.ext_ring $ h
+
+variables {A : Type*} [comm_semiring R] [semiring A] [algebra R A]
+
+/-- A universal property of the dual numbers, providing a unique `R[ε] →ₐ[R] A` for every element
+of `A` which squares to `0`.
+
+This isomorphism is named to match the very similar `complex.lift`. -/
+@[simps {attrs := []}]
+def lift : {e : A // e * e = 0} ≃ (R[ε] →ₐ[R] A) :=
+equiv.trans
+  (show {e : A // e * e = 0} ≃ {f : R →ₗ[R] A // ∀ x y, f x * f y = 0}, from
+    (linear_map.ring_lmap_equiv_self R ℕ A).symm.to_equiv.subtype_equiv $ λ a, begin
+      dsimp,
+      simp_rw smul_mul_smul,
+      refine ⟨λ h x y, h.symm ▸ smul_zero _, λ h, by simpa using h 1 1⟩,
+    end)
+  triv_sq_zero_ext.lift
+
+/- When applied to `ε`, `dual_number.lift` produces the element of `A` that squares to 0. -/
+@[simp]
+lemma lift_apply_eps (e : {e : A // e * e = 0}) : lift e (ε : R[ε]) = e :=
+(triv_sq_zero_ext.lift_aux_apply_inr _ _ _).trans $ one_smul _ _
+
+/- Lifting `dual_number.eps` itself gives the identity. -/
+@[simp]
+lemma lift_eps : lift ⟨ε, by exact eps_mul_eps⟩ = alg_hom.id R R[ε] :=
+alg_hom_ext $ lift_apply_eps _
+
+end dual_number

src/linear_algebra/clifford_algebra/equivs.lean

@@ -6,6 +6,7 @@ Authors: Eric Wieser
 import algebra.quaternion_basis
 import data.complex.module
 import linear_algebra.clifford_algebra.conjugation
+import algebra.dual_number
 import linear_algebra.quadratic_form.prod
 
 /-!
@@ -48,6 +49,11 @@ and vice-versa:
 * `clifford_algebra_quaternion.to_quaternion_involute_reverse`
 * `clifford_algebra_quaternion.of_quaternion_conj`
 
+## Dual numbers
+
+* `clifford_algebra_dual_number.equiv`: `R[ε]` is is equivalent as an `R`-algebra to a clifford
+  algebra over `R` where `Q = 0`.
+
 -/
 
 open clifford_algebra
@@ -343,3 +349,34 @@ clifford_algebra_quaternion.equiv.injective $
 attribute [protected] Q
 
 end clifford_algebra_quaternion
+
+/-! ### The clifford algebra isomorphic to the dual numbers -/
+namespace clifford_algebra_dual_number
+
+open_locale dual_number
+open dual_number triv_sq_zero_ext
+
+variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]
+
+lemma ι_mul_ι (r₁ r₂) : ι (0 : quadratic_form R R) r₁ * ι (0 : quadratic_form R R) r₂ = 0 :=
+by rw [←mul_one r₁, ←mul_one r₂, ←smul_eq_mul R, ←smul_eq_mul R, linear_map.map_smul,
+       linear_map.map_smul, smul_mul_smul, ι_sq_scalar, quadratic_form.zero_apply,
+       ring_hom.map_zero, smul_zero]
+
+/-- The clifford algebra over a 1-dimensional vector space with 0 quadratic form is isomorphic to
+the dual numbers. -/
+protected def equiv : clifford_algebra (0 : quadratic_form R R) ≃ₐ[R] R[ε] :=
+alg_equiv.of_alg_hom
+  (clifford_algebra.lift (0 : quadratic_form R R) ⟨inr_hom R _, λ m, inr_mul_inr _ m m⟩)
+  (dual_number.lift ⟨ι _ (1 : R), ι_mul_ι (1 : R) 1⟩)
+  (by { ext x : 1, dsimp, rw [lift_apply_eps, subtype.coe_mk, lift_ι_apply, inr_hom_apply, eps] })
+  (by { ext : 2, dsimp, rw [lift_ι_apply, inr_hom_apply, ←eps, lift_apply_eps, subtype.coe_mk] })
+
+@[simp] lemma equiv_ι (r : R) : clifford_algebra_dual_number.equiv (ι _ r) = r • ε :=
+(lift_ι_apply _ _ r).trans (inr_eq_smul_eps _)
+
+@[simp] lemma equiv_symm_eps :
+  clifford_algebra_dual_number.equiv.symm (eps : R[ε]) = ι (0 : quadratic_form R R) 1 :=
+dual_number.lift_apply_eps _
+
+end clifford_algebra_dual_number