feat(algebra/*): Add ring instances to clifford_algebra and exterior_…

…algebra (#4916)

To do this, this removes the `irreducible` attributes.

These attributes were present to try and "insulate" the quotient / generator based definitions, and force downstream proofs to use the universal property.

Unfortunately, this irreducibility created massive headaches in typeclass resolution, and the tradeoff for neatness vs usability just isn't worth it.

If someone wants to add back the `irreducible` attributes in future, they now have test-cases that force them not to break the `ring` instances when doing so.

src/algebra/free_algebra.lean

@@ -265,7 +265,10 @@ At this stage we set the basic definitions as `@[irreducible]`, so from this poi
 
 Of course, one still has the option to locally make these definitions `semireducible` if so desired, and Lean is still willing in some circumstances to do unification based on the underlying definition.
 -/
-attribute [irreducible] free_algebra ι lift
+attribute [irreducible] ι lift
+-- Marking `free_algebra` irreducible makes `ring` instances inaccessible on quotients.
+-- 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.
 
 @[simp]
 theorem lift_comp_ι (g : free_algebra R X →ₐ[R] A) :

src/algebra/lie/universal_enveloping.lean

@@ -53,13 +53,11 @@ inductive rel : tensor_algebra R L → tensor_algebra R L → Prop
 end universal_enveloping_algebra
 
 /-- The universal enveloping algebra of a Lie algebra. -/
-@[derive [inhabited, semiring, algebra R]]
+@[derive [inhabited, ring, algebra R]]
 def universal_enveloping_algebra := ring_quot (universal_enveloping_algebra.rel R L)
 
 namespace universal_enveloping_algebra
 
-instance : ring (universal_enveloping_algebra R L) := algebra.semiring_to_ring R
-
 /-- The quotient map from the tensor algebra to the universal enveloping algebra as a morphism of
 associative algebras. -/
 def mk_alg_hom : tensor_algebra R L →ₐ[R] universal_enveloping_algebra R L :=

src/algebra/ring_quot.lean

@@ -280,6 +280,6 @@ by { ext, simp, }
 
 end algebra
 
-attribute [irreducible] ring_quot mk_ring_hom mk_alg_hom lift lift_alg_hom
+attribute [irreducible] mk_ring_hom mk_alg_hom lift lift_alg_hom
 
 end ring_quot

src/linear_algebra/clifford_algebra.lean

@@ -66,7 +66,7 @@ end clifford_algebra
 /--
 The Clifford algebra of an `R`-module `M` equipped with a quadratic_form `Q`.
 -/
-@[derive [inhabited, semiring, algebra R]]
+@[derive [inhabited, ring, algebra R]]
 def clifford_algebra := ring_quot (clifford_algebra.rel Q)
 
 namespace clifford_algebra

src/linear_algebra/exterior_algebra.lean

@@ -65,6 +65,11 @@ namespace exterior_algebra
 
 variables {M}
 
+-- typeclass resolution times out here, so we give it a hand
+instance {S : Type*} [comm_ring S] [semimodule S M] : ring (exterior_algebra S M) :=
+let i : ring (tensor_algebra S M) := infer_instance in
+@ring_quot.ring (tensor_algebra S M) i (exterior_algebra.rel S M)
+
 /--
 The canonical linear map `M →ₗ[R] exterior_algebra R M`.
 -/
@@ -115,7 +120,10 @@ begin
   refl,
 end
 
-attribute [irreducible] exterior_algebra ι lift
+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.
 
 variables {R M}
 

src/linear_algebra/tensor_algebra.lean

@@ -61,7 +61,7 @@ def tensor_algebra := ring_quot (tensor_algebra.rel R M)
 namespace tensor_algebra
 
 instance {S : Type*} [comm_ring S] [semimodule S M] : ring (tensor_algebra S M) :=
-ring_quot.ring _
+ring_quot.ring (rel S M)
 
 variables {M}
 /--
@@ -103,7 +103,10 @@ begin
   refl,
 end
 
-attribute [irreducible] tensor_algebra ι lift
+-- Marking `tensor_algebra` irreducible makes `ring` instances inaccessible on quotients.
+-- 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.
+attribute [irreducible] ι lift
 
 @[simp]
 theorem lift_comp_ι {A : Type*} [semiring A] [algebra R A] (g : tensor_algebra R M →ₐ[R] A) :

test/free_algebra.lean

@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+
+import linear_algebra.exterior_algebra
+import linear_algebra.clifford_algebra
+
+/-!
+Tests that the ring instances for `free_algebra` and derived quotient types actually work.
+
+There is some discussion about this in
+https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/algebra.2Esemiring_to_ring.20breaks.20semimodule.20typeclass.20lookup/near/212580241
+
+In essence, the use of `attribute [irreducible] the_type` was breaking instance resolution on that
+type.
+-/
+
+variables {S : Type*} {M : Type*}
+
+
+section free
+
+variables [comm_ring S]
+
+example : (1 : free_algebra S M) - (1 : free_algebra S M) = 0 := by rw sub_self
+
+end free
+
+
+section exterior
+
+variables [comm_ring S] [add_comm_monoid M] [semimodule S M]
+
+example : (1 : exterior_algebra S M) - (1 : exterior_algebra S M) = 0 := by rw sub_self
+
+end exterior
+
+
+section clifford
+
+variables [comm_ring S] [add_comm_group M] [semimodule S M] (Q : quadratic_form S M)
+
+example : (1 : clifford_algebra Q) - (1 : clifford_algebra Q) = 0 := by rw sub_self
+
+end clifford