refactor(linear_algebra/exterior_algebra): redefine `exterior_algebra…

…` as `clifford_algebra 0` (#14819)

The motivation here is to avoid having to duplicate API between these two types, else we end up having to repeat every definition that works on `clifford_algebra Q` on `exterior_algebra` for the case when `Q = 0`. This also:
* Removes `as_exterior : clifford_algebra (0 : quadratic_form R M) ≃ₐ[R] exterior_algebra R M` as the two types are reducibly defeq.
* Removes support for working with exterior algebras over semirings; while it is entirely possible to generalize `clifford_algebra` to semirings to make this removal unnecessary, it creates difficulties with elaboration, and the support for semirings was without mathematical motivation in the first place. This is in line with a [vote on Zulip](https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Exterior.20algebras.20over.20semiring/near/286660821).

The consequences are:
* A bunch of redundant code can be removed
* `x.reverse` and `x.involute` should now work on `x : exterior_algebra R M`.
* Future API will extend effortlessly from one to the other

src/linear_algebra/clifford_algebra/basic.lean

@@ -6,7 +6,6 @@ Authors: Eric Wieser, Utensil Song
 
 import algebra.ring_quot
 import linear_algebra.tensor_algebra.basic
-import linear_algebra.exterior_algebra.basic
 import linear_algebra.quadratic_form.isometry
 
 /-!
@@ -195,26 +194,6 @@ begin
   exact alg_hom.congr_fun of_id a,
 end
 
-/-- A Clifford algebra with a zero quadratic form is isomorphic to an `exterior_algebra` -/
-def as_exterior : clifford_algebra (0 : quadratic_form R M) ≃ₐ[R] exterior_algebra R M :=
-alg_equiv.of_alg_hom
-  (clifford_algebra.lift 0 ⟨(exterior_algebra.ι R),
-    by simp only [forall_const, ring_hom.map_zero,
-                  exterior_algebra.ι_sq_zero, quadratic_form.zero_apply]⟩)
-  (exterior_algebra.lift R ⟨(ι (0 : quadratic_form R M)),
-    by simp only [forall_const, ring_hom.map_zero,
-                  quadratic_form.zero_apply, ι_sq_scalar]⟩)
-  (exterior_algebra.hom_ext $ linear_map.ext $
-    by simp only [alg_hom.comp_to_linear_map, linear_map.coe_comp,
-                  function.comp_app, alg_hom.to_linear_map_apply,
-                  exterior_algebra.lift_ι_apply, clifford_algebra.lift_ι_apply,
-                  alg_hom.to_linear_map_id, linear_map.id_comp, eq_self_iff_true, forall_const])
-  (clifford_algebra.hom_ext $ linear_map.ext $
-    by simp only [alg_hom.comp_to_linear_map, linear_map.coe_comp,
-                  function.comp_app, alg_hom.to_linear_map_apply,
-                  clifford_algebra.lift_ι_apply, exterior_algebra.lift_ι_apply,
-                  alg_hom.to_linear_map_id, linear_map.id_comp, eq_self_iff_true, forall_const])
-
 /-- The symmetric product of vectors is a scalar -/
 lemma ι_mul_ι_add_swap (a b : M) :
   ι Q a * ι Q b + ι Q b * ι Q a = algebra_map R _ (quadratic_form.polar Q a b) :=

src/linear_algebra/exterior_algebra/basic.lean

@@ -5,7 +5,7 @@ Authors: Zhangir Azerbayev, Adam Topaz, Eric Wieser
 -/
 
 import algebra.ring_quot
-import linear_algebra.tensor_algebra.basic
+import linear_algebra.clifford_algebra.basic
 import linear_algebra.alternating
 import group_theory.perm.sign
 
@@ -38,58 +38,36 @@ of the exterior algebra.
 
 ## Implementation details
 
-The exterior algebra of `M` is constructed as a quotient of the tensor algebra, as follows.
-1. We define a relation `exterior_algebra.rel R M` on `tensor_algebra R M`.
-   This is the smallest relation which identifies squares of elements of `M` with `0`.
-2. The exterior algebra is the quotient of the tensor algebra by this relation.
-
+The exterior algebra of `M` is constructed as simply `clifford_algebra (0 : quadratic_form R M)`,
+as this avoids us having to duplicate API.
 -/
 
 universes u1 u2 u3
 
-variables (R : Type u1) [comm_semiring R]
-variables (M : Type u2) [add_comm_monoid M] [module R M]
-
-namespace exterior_algebra
-open tensor_algebra
-
-/-- `rel` relates each `ι m * ι m`, for `m : M`, with `0`.
-
-The exterior algebra of `M` is defined as the quotient modulo this relation.
--/
-inductive rel : tensor_algebra R M → tensor_algebra R M → Prop
-| of (m : M) : rel ((ι R m) * (ι R m)) 0
-
-end exterior_algebra
+variables (R : Type u1) [comm_ring R]
+variables (M : Type u2) [add_comm_group M] [module R M]
 
 /--
 The exterior algebra of an `R`-module `M`.
 -/
-@[derive [inhabited, semiring, algebra R]]
-def exterior_algebra := ring_quot (exterior_algebra.rel R M)
+@[reducible]
+def exterior_algebra := clifford_algebra (0 : quadratic_form R M)
 
 namespace exterior_algebra
 
 variables {M}
 
-instance {S : Type u3} [comm_ring S] [module S M] : ring (exterior_algebra S M) :=
-ring_quot.ring (exterior_algebra.rel S M)
-
 /--
 The canonical linear map `M →ₗ[R] exterior_algebra R M`.
 -/
-def ι : M →ₗ[R] exterior_algebra R M :=
-(ring_quot.mk_alg_hom R _).to_linear_map.comp (tensor_algebra.ι R)
-
+@[reducible] def ι : M →ₗ[R] exterior_algebra R M := by exact clifford_algebra.ι _
 
 variables {R}
 
 /-- As well as being linear, `ι m` squares to zero -/
 @[simp]
 theorem ι_sq_zero (m : M) : (ι R m) * (ι R m) = 0 :=
-begin
-  erw [←alg_hom.map_mul, ring_quot.mk_alg_hom_rel R (rel.of m), alg_hom.map_zero _],
-end
+(clifford_algebra.ι_sq_scalar _ m).trans $ map_zero _
 
 variables {A : Type*} [semiring A] [algebra R A]
 
@@ -107,65 +85,39 @@ from `exterior_algebra R M` to `A`.
 -/
 @[simps symm_apply]
 def lift : {f : M →ₗ[R] A // ∀ m, f m * f m = 0} ≃ (exterior_algebra R M →ₐ[R] A) :=
-{ to_fun := λ f,
-  ring_quot.lift_alg_hom R ⟨tensor_algebra.lift R (f : M →ₗ[R] A),
-    λ x y (h : rel R M x y), by
-    { induction h,
-      rw [alg_hom.map_zero, alg_hom.map_mul, tensor_algebra.lift_ι_apply, f.prop] }⟩,
-  inv_fun := λ F, ⟨F.to_linear_map.comp (ι R), λ m, by rw [
-    linear_map.comp_apply, alg_hom.to_linear_map_apply, comp_ι_sq_zero]⟩,
-  left_inv := λ f, by { ext, simp [ι] },
-  right_inv := λ F, by { ext, simp [ι] } }
+equiv.trans (equiv.subtype_equiv (equiv.refl _) $ by simp) $ clifford_algebra.lift _
 
 @[simp]
 theorem ι_comp_lift (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = 0) :
   (lift R ⟨f, cond⟩).to_linear_map.comp (ι R) = f :=
-(subtype.mk_eq_mk.mp $ (lift R).symm_apply_apply ⟨f, cond⟩)
+clifford_algebra.ι_comp_lift f _
 
 @[simp]
 theorem lift_ι_apply (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = 0) (x) :
   lift R ⟨f, cond⟩ (ι R x) = f x :=
-(linear_map.ext_iff.mp $ ι_comp_lift R f cond) x
+clifford_algebra.lift_ι_apply f _ x
 
 @[simp]
 theorem lift_unique (f : M →ₗ[R] A) (cond : ∀ m, f m * f m = 0)
   (g : exterior_algebra R M →ₐ[R] A) : g.to_linear_map.comp (ι R) = f ↔ g = lift R ⟨f, cond⟩ :=
-begin
-  convert (lift R).symm_apply_eq,
-  rw lift_symm_apply,
-  simp only,
-end
-
-attribute [irreducible] ι lift
--- Marking `exterior_algebra` irreducible makes our `ring` instances inaccessible.
--- https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/algebra.2Esemiring_to_ring.20breaks.20semimodule.20typeclass.20lookup/near/212580241
--- For now, we avoid this by not marking it irreducible.
+clifford_algebra.lift_unique f _ _
 
 variables {R M}
 
 @[simp]
 theorem lift_comp_ι (g : exterior_algebra R M →ₐ[R] A) :
   lift R ⟨g.to_linear_map.comp (ι R), comp_ι_sq_zero _⟩ = g :=
-begin
-  convert (lift R).apply_symm_apply g,
-  rw lift_symm_apply,
-  refl,
-end
+clifford_algebra.lift_comp_ι g
 
 /-- See note [partially-applied ext lemmas]. -/
 @[ext]
 theorem hom_ext {f g : exterior_algebra R M →ₐ[R] A}
   (h : f.to_linear_map.comp (ι R) = g.to_linear_map.comp (ι R)) : f = g :=
-begin
-  apply (lift R).symm.injective,
-  rw [lift_symm_apply, lift_symm_apply],
-  simp only [h],
-end
+clifford_algebra.hom_ext h
 
 /-- If `C` holds for the `algebra_map` of `r : R` into `exterior_algebra R M`, the `ι` of `x : M`,
 and is preserved under addition and muliplication, then it holds for all of `exterior_algebra R M`.
 -/
--- This proof closely follows `tensor_algebra.induction`
 @[elab_as_eliminator]
 lemma induction {C : exterior_algebra R M → Prop}
   (h_grade0 : ∀ r, C (algebra_map R (exterior_algebra R M) r))
@@ -174,24 +126,7 @@ lemma induction {C : exterior_algebra R M → Prop}
   (h_add : ∀ a b, C a → C b → C (a + b))
   (a : exterior_algebra R M) :
   C a :=
-begin
-  -- the arguments are enough to construct a subalgebra, and a mapping into it from M
-  let s : subalgebra R (exterior_algebra R M) :=
-  { carrier := C,
-    mul_mem' := h_mul,
-    add_mem' := h_add,
-    algebra_map_mem' := h_grade0, },
-  let of : { f : M →ₗ[R] s // ∀ m, f m * f m = 0 } :=
-  ⟨(ι R).cod_restrict s.to_submodule h_grade1,
-    λ m, subtype.eq $ ι_sq_zero m ⟩,
-  -- the mapping through the subalgebra is the identity
-  have of_id : alg_hom.id R (exterior_algebra R M) = s.val.comp (lift R of),
-  { ext,
-    simp [of], },
-  -- finding a proof is finding an element of the subalgebra
-  convert subtype.prop (lift R of a),
-  exact alg_hom.congr_fun of_id a,
-end
+clifford_algebra.induction h_grade0 h_grade1 h_mul h_add a
 
 /-- The left-inverse of `algebra_map`. -/
 def algebra_map_inv : exterior_algebra R M →ₐ[R] R :=
@@ -334,7 +269,7 @@ variables {R M}
 /-- The canonical image of the `tensor_algebra` in the `exterior_algebra`, which maps
 `tensor_algebra.ι R x` to `exterior_algebra.ι R x`. -/
 def to_exterior : tensor_algebra R M →ₐ[R] exterior_algebra R M :=
-tensor_algebra.lift R (exterior_algebra.ι R)
+tensor_algebra.lift R (exterior_algebra.ι R : M →ₗ[R] exterior_algebra R M)
 
 @[simp] lemma to_exterior_ι (m : M) : (tensor_algebra.ι R m).to_exterior = exterior_algebra.ι R m :=
 by simp [to_exterior]

src/linear_algebra/exterior_algebra/grading.lean

@@ -16,7 +16,7 @@ The main result is `exterior_algebra.graded_algebra`, which says that the exteri
 -/
 
 namespace exterior_algebra
-variables {R M : Type*} [comm_semiring R] [add_comm_monoid M] [module R M]
+variables {R M : Type*} [comm_ring R] [add_comm_group M] [module R M]
 variables (R M)
 
 open_locale direct_sum

test/free_algebra.lean

@@ -31,7 +31,7 @@ end free
 
 section exterior
 
-variables [comm_ring S] [add_comm_monoid M] [module S M]
+variables [comm_ring S] [add_comm_group M] [module S M]
 
 example : (1 : exterior_algebra S M) - (1 : exterior_algebra S M) = 0 := by rw sub_self