refactor(algebra/ring_quot.lean): make ring_quot irreducible (#7120)

The quotient of a ring by an equivalence relation which is compatible with the operations is still a ring. This is used to define several objects such as tensor algebras, exterior algebras, and so on, but the details of the construction are irrelevant. This PR makes `ring_quot` irreducible to keep the complexity down.

src/algebra/ring_quot.lean

@@ -15,8 +15,8 @@ and it's not immediately clear how one should formalise ideals in the non-commut
 In this file, we directly define the quotient of a semiring by any relation,
 by building a bigger relation that represents the ideal generated by that relation.
 
-We prove the universal properties of the quotient,
-and recommend avoiding relying on the actual definition!
+We prove the universal properties of the quotient, and recommend avoiding relying on the actual
+definition, which is made irreducible for this purpose.
 
 Since everything runs in parallel for quotients of `R`-algebras, we do that case at the same time.
 -/
@@ -61,74 +61,114 @@ by simp only [algebra.smul_def, rel.mul_right h]
 end ring_quot
 
 /-- The quotient of a ring by an arbitrary relation. -/
-def ring_quot (r : R → R → Prop) := quot (ring_quot.rel r)
+structure ring_quot (r : R → R → Prop) :=
+(to_quot : quot (ring_quot.rel r))
 
 namespace ring_quot
 
+variable (r : R → R → Prop)
+
+@[irreducible] private def zero : ring_quot r := ⟨quot.mk _ 0⟩
+@[irreducible] private def one : ring_quot r := ⟨quot.mk _ 1⟩
+@[irreducible] private def add : ring_quot r → ring_quot r → ring_quot r
+| ⟨a⟩ ⟨b⟩ := ⟨quot.map₂ (+) rel.add_right rel.add_left a b⟩
+@[irreducible] private def mul : ring_quot r → ring_quot r → ring_quot r
+| ⟨a⟩ ⟨b⟩ := ⟨quot.map₂ (*) rel.mul_right rel.mul_left a b⟩
+@[irreducible] private def neg {R : Type u₁} [ring R] (r : R → R → Prop) : ring_quot r → ring_quot r
+| ⟨a⟩:= ⟨quot.map (λ a, -a) rel.neg a⟩
+@[irreducible] private def sub {R : Type u₁} [ring R] (r : R → R → Prop) :
+  ring_quot r → ring_quot r → ring_quot r
+| ⟨a⟩ ⟨b⟩ := ⟨quot.map₂ has_sub.sub rel.sub_right rel.sub_left a b⟩
+@[irreducible] private def smul [algebra S R] (n : S) : ring_quot r → ring_quot r
+| ⟨a⟩ := ⟨quot.map (λ a, n • a) (rel.smul n) a⟩
+
+instance : has_zero (ring_quot r) := ⟨zero r⟩
+instance : has_one (ring_quot r) := ⟨one r⟩
+instance : has_add (ring_quot r) := ⟨add r⟩
+instance : has_mul (ring_quot r) := ⟨mul r⟩
+instance {R : Type u₁} [ring R] (r : R → R → Prop) : has_neg (ring_quot r) := ⟨neg r⟩
+instance {R : Type u₁} [ring R] (r : R → R → Prop) : has_sub (ring_quot r) := ⟨sub r⟩
+instance [algebra S R] : has_scalar S (ring_quot r) := ⟨smul r⟩
+
+lemma zero_quot : (⟨quot.mk _ 0⟩ : ring_quot r) = 0 := show _ = zero r, by rw zero
+lemma one_quot : (⟨quot.mk _ 1⟩ : ring_quot r) = 1 := show _ = one r, by rw one
+lemma add_quot {a b} : (⟨quot.mk _ a⟩ + ⟨quot.mk _ b⟩ : ring_quot r) = ⟨quot.mk _ (a + b)⟩ :=
+by { show add r _ _ = _, rw add, refl }
+lemma mul_quot {a b} : (⟨quot.mk _ a⟩ * ⟨quot.mk _ b⟩ : ring_quot r) = ⟨quot.mk _ (a * b)⟩ :=
+by { show mul r _ _ = _, rw mul, refl }
+lemma neg_quot {R : Type u₁} [ring R] (r : R → R → Prop) {a} :
+  (-⟨quot.mk _ a⟩ : ring_quot r) = ⟨quot.mk _ (-a)⟩ :=
+by { show neg r _ = _, rw neg, refl }
+lemma sub_quot {R : Type u₁} [ring R] (r : R → R → Prop) {a b} :
+  (⟨quot.mk _ a⟩ - ⟨ quot.mk _ b⟩ : ring_quot r) = ⟨quot.mk _ (a - b)⟩ :=
+by { show sub r _ _ = _, rw sub, refl }
+lemma smul_quot [algebra S R] {n : S} {a : R} :
+  (n • ⟨quot.mk _ a⟩ : ring_quot r) = ⟨quot.mk _ (n • a)⟩ :=
+by { show smul r _ _ = _, rw smul, refl }
+
 instance (r : R → R → Prop) : semiring (ring_quot r) :=
-{ add           := quot.map₂ (+) rel.add_right rel.add_left,
-  add_assoc     := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (add_assoc _ _ _), },
-  zero          := quot.mk _ 0,
-  zero_add      := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (zero_add _), },
-  add_zero      := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (add_zero _), },
-  zero_mul      := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (zero_mul _), },
-  mul_zero      := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (mul_zero _), },
-  add_comm      := by { rintros ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (add_comm _ _), },
-  mul           := quot.map₂ (*) rel.mul_right rel.mul_left,
-  mul_assoc     := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (mul_assoc _ _ _), },
-  one           := quot.mk _ 1,
-  one_mul       := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (one_mul _), },
-  mul_one       := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (mul_one _), },
-  left_distrib  := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (left_distrib _ _ _), },
-  right_distrib := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (right_distrib _ _ _), },
-  nsmul         := λ n, quot.map ((•) n) (rel.smul n),
-  nsmul_zero'   := by { rintro ⟨⟩, exact congr_arg (quot.mk _) (zero_nsmul _) },
-  nsmul_succ'   := by { rintros n ⟨⟩, refine congr_arg (quot.mk _) _,
-                        simp only [nat.succ_eq_one_add, add_smul, one_smul] } }
+{ add           := (+),
+  mul           := (*),
+  zero          := 0,
+  one           := 1,
+  add_assoc     := by { rintros ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩, simp [add_quot, add_assoc] },
+  zero_add      := by { rintros ⟨⟨⟩⟩, simp [add_quot, ← zero_quot] },
+  add_zero      := by { rintros ⟨⟨⟩⟩, simp [add_quot, ← zero_quot], },
+  zero_mul      := by { rintros ⟨⟨⟩⟩, simp [mul_quot, ← zero_quot], },
+  mul_zero      := by { rintros ⟨⟨⟩⟩, simp [mul_quot, ← zero_quot], },
+  add_comm      := by { rintros ⟨⟨⟩⟩ ⟨⟨⟩⟩, simp [add_quot, add_comm], },
+  mul_assoc     := by { rintros ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩, simp [mul_quot, mul_assoc] },
+  one_mul       := by { rintros ⟨⟨⟩⟩, simp [mul_quot, ← one_quot] },
+  mul_one       := by { rintros ⟨⟨⟩⟩, simp [mul_quot, ← one_quot] },
+  left_distrib  := by { rintros ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩, simp [mul_quot, add_quot, left_distrib] },
+  right_distrib := by { rintros ⟨⟨⟩⟩ ⟨⟨⟩⟩ ⟨⟨⟩⟩, simp [mul_quot, add_quot, right_distrib] },
+  nsmul         := (•),
+  nsmul_zero'   := by { rintros ⟨⟨⟩⟩, simp [smul_quot, ← zero_quot] },
+  nsmul_succ'   := by { rintros n ⟨⟨⟩⟩, simp [smul_quot, add_quot, add_mul, add_comm] } }
 
 instance {R : Type u₁} [ring R] (r : R → R → Prop) : ring (ring_quot r) :=
-{ neg            := quot.map (λ a, -a) rel.neg,
-  add_left_neg   := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (add_left_neg _), },
-  sub            := quot.map₂ (has_sub.sub) rel.sub_right rel.sub_left,
-  sub_eq_add_neg := by { rintros ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (sub_eq_add_neg _ _), },
+{ neg           := has_neg.neg,
+  add_left_neg  := by { rintros ⟨⟨⟩⟩, simp [neg_quot, add_quot, ← zero_quot], },
+  sub            := has_sub.sub,
+  sub_eq_add_neg := by { rintros ⟨⟨⟩⟩ ⟨⟨⟩⟩, simp [neg_quot, sub_quot, add_quot, sub_eq_add_neg] },
   .. (ring_quot.semiring r) }
 
 instance {R : Type u₁} [comm_semiring R] (r : R → R → Prop) : comm_semiring (ring_quot r) :=
-{ mul_comm := by { rintros ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (mul_comm _ _), }
+{ mul_comm := by { rintros ⟨⟨⟩⟩ ⟨⟨⟩⟩, simp [mul_quot, mul_comm], }
   .. (ring_quot.semiring r) }
 
 instance {R : Type u₁} [comm_ring R] (r : R → R → Prop) : comm_ring (ring_quot r) :=
 { .. (ring_quot.comm_semiring r),
   .. (ring_quot.ring r) }
 
-instance (s : A → A → Prop) : algebra S (ring_quot s) :=
-{ smul      := λ r, quot.map ((•) r) (rel.smul r),
-  to_fun    := λ r, quot.mk _ (algebra_map S A r),
-  map_one'  := congr_arg (quot.mk _) (ring_hom.map_one _),
-  map_mul'  := λ r s, congr_arg (quot.mk _) (ring_hom.map_mul _ _ _),
-  map_zero' := congr_arg (quot.mk _) (ring_hom.map_zero _),
-  map_add'  := λ r s, congr_arg (quot.mk _) (ring_hom.map_add _ _ _),
-  commutes' := λ r, by { rintro ⟨a⟩, exact congr_arg (quot.mk _) (algebra.commutes _ _) },
-  smul_def' := λ r, by { rintro ⟨a⟩, exact congr_arg (quot.mk _) (algebra.smul_def _ _) }, }
-
 instance (r : R → R → Prop) : inhabited (ring_quot r) := ⟨0⟩
 
+instance [algebra S R] (r : R → R → Prop) : algebra S (ring_quot r) :=
+{ smul      := (•),
+  to_fun    := λ r, ⟨quot.mk _ (algebra_map S R r)⟩,
+  map_one'  := by simp [← one_quot],
+  map_mul'  := by simp [mul_quot],
+  map_zero' := by simp [← zero_quot],
+  map_add'  := by simp [add_quot],
+  commutes' := λ r, by { rintro ⟨⟨a⟩⟩, simp [algebra.commutes, mul_quot] },
+  smul_def' := λ r, by { rintro ⟨⟨a⟩⟩, simp [smul_quot, algebra.smul_def, mul_quot], }, }
+
 /--
 The quotient map from a ring to its quotient, as a homomorphism of rings.
 -/
 def mk_ring_hom (r : R → R → Prop) : R →+* ring_quot r :=
-{ to_fun := quot.mk _,
-  map_one'  := rfl,
-  map_mul'  := λ a b, rfl,
-  map_zero' := rfl,
-  map_add'  := λ a b, rfl, }
+{ to_fun := λ x, ⟨quot.mk _ x⟩,
+  map_one'  := by simp [← one_quot],
+  map_mul'  := by simp [mul_quot],
+  map_zero' := by simp [← zero_quot],
+  map_add'  := by simp [add_quot], }
 
 lemma mk_ring_hom_rel {r : R → R → Prop} {x y : R} (w : r x y) :
   mk_ring_hom r x = mk_ring_hom r y :=
-quot.sound (rel.of w)
+by simp [mk_ring_hom, quot.sound (rel.of w)]
 
 lemma mk_ring_hom_surjective (r : R → R → Prop) : function.surjective (mk_ring_hom r) :=
-by { dsimp [mk_ring_hom], rintro ⟨⟩, simp, }
+by { dsimp [mk_ring_hom], rintro ⟨⟨⟩⟩, simp, }
 
 @[ext]
 lemma ring_quot_ext {T : Type u₄} [semiring T] {r : R → R → Prop} (f g : ring_quot r →+* T)
@@ -148,19 +188,19 @@ factors uniquely through a morphism `ring_quot r →+* T`.
 def lift {r : R → R → Prop} :
   {f : R →+* T // ∀ ⦃x y⦄, r x y → f x = f y} ≃ (ring_quot r →+* T) :=
 { to_fun := λ f', let f := (f' : R →+* T) in
-  { to_fun := quot.lift f
+  { to_fun := λ x, quot.lift f
     begin
       rintros _ _ r,
       induction r,
       case of : _ _ r { exact f'.prop r, },
       case add_left : _ _ _ _ r' { simp [r'], },
       case mul_left : _ _ _ _ r' { simp [r'], },
       case mul_right : _ _ _ _ r' { simp [r'], },
-    end,
-    map_zero' := f.map_zero,
-    map_add' := by { rintros ⟨x⟩ ⟨y⟩, exact f.map_add x y, },
-    map_one' := f.map_one,
-    map_mul' := by { rintros ⟨x⟩ ⟨y⟩, exact f.map_mul x y, }, },
+    end x.to_quot,
+    map_zero' := by simp [← zero_quot, f.map_zero],
+    map_add' := by { rintros ⟨⟨x⟩⟩ ⟨⟨y⟩⟩, simp [add_quot, f.map_add x y], },
+    map_one' := by simp [← one_quot, f.map_one],
+    map_mul' := by { rintros ⟨⟨x⟩⟩ ⟨⟨y⟩⟩, simp [mul_quot, f.map_mul x y] }, },
   inv_fun := λ F, ⟨F.comp (mk_ring_hom r), λ x y h, by { dsimp, rw mk_ring_hom_rel h, }⟩,
   left_inv := λ f, by { ext, simp, refl },
   right_inv := λ F, by { ext, simp, refl } }
@@ -225,20 +265,38 @@ ring_equiv.of_hom_inv (ring_quot_to_ideal_quotient r) (ideal_quotient_to_ring_qu
 
 end comm_ring
 
+section star_ring
+
+variables [star_ring R] (r) (hr : ∀ a b, r a b → r (star a) (star b))
+include hr
+
+theorem rel.star ⦃a b : R⦄ (h : rel r a b) :
+  rel r (star a) (star b) :=
+begin
+  induction h,
+  { exact rel.of (hr _ _ h_h) },
+  { rw [star_add, star_add], exact rel.add_left h_ih, },
+  { rw [star_mul, star_mul], exact rel.mul_right h_ih, },
+  { rw [star_mul, star_mul], exact rel.mul_left h_ih, },
+end
+
+@[irreducible] private def star' : ring_quot r → ring_quot r
+| ⟨a⟩ := ⟨quot.map (_root_.star : R → R) (rel.star r hr) a⟩
+
+lemma star'_quot (hr : ∀ a b, r a b → r (star a) (star b)) {a} :
+  (star' r hr ⟨quot.mk _ a⟩ : ring_quot r) = ⟨quot.mk _ (star a)⟩ :=
+by { show star' r _ _ = _, rw star', refl }
+
 /-- Transfer a star_ring instance through a quotient, if the quotient is invariant to `star` -/
 def star_ring {R : Type u₁} [semiring R] [star_ring R] (r : R → R → Prop)
-  (hr : ∀ {a b}, r a b → r (star a) (star b)) :
+  (hr : ∀ a b, r a b → r (star a) (star b)) :
   star_ring (ring_quot r) :=
-{ star := quot.map star $ λ a b h, begin
-    induction h,
-    { exact rel.of (hr h_h) },
-    { rw [star_add, star_add], exact rel.add_left h_ih, },
-    { rw [star_mul, star_mul], exact rel.mul_right h_ih, },
-    { rw [star_mul, star_mul], exact rel.mul_left h_ih, },
-  end,
-  star_involutive := by { rintros ⟨⟩, exact congr_arg (quot.mk _) (star_star _), },
-  star_mul := by { rintros ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (star_mul _ _), },
-  star_add := by { rintros ⟨⟩ ⟨⟩, exact congr_arg (quot.mk _) (star_add _ _), } }
+{ star := star' r hr,
+  star_involutive := by { rintros ⟨⟨⟩⟩, simp [star'_quot], },
+  star_mul := by { rintros ⟨⟨⟩⟩ ⟨⟨⟩⟩, simp [star'_quot, mul_quot, star_mul], },
+  star_add := by { rintros ⟨⟨⟩⟩ ⟨⟨⟩⟩, simp [star'_quot, add_quot, star_add], } }
+
+end star_ring
 
 section algebra
 
@@ -257,10 +315,10 @@ rfl
 
 lemma mk_alg_hom_rel {s : A → A → Prop} {x y : A} (w : s x y) :
   mk_alg_hom S s x = mk_alg_hom S s y :=
-quot.sound (rel.of w)
+by simp [mk_alg_hom, mk_ring_hom, quot.sound (rel.of w)]
 
 lemma mk_alg_hom_surjective (s : A → A → Prop) : function.surjective (mk_alg_hom S s) :=
-by { dsimp [mk_alg_hom], rintro ⟨a⟩, use a, refl, }
+by { dsimp [mk_alg_hom], rintro ⟨⟨a⟩⟩, use a, refl, }
 
 variables {B : Type u₄} [semiring B] [algebra S B]
 
@@ -280,26 +338,20 @@ factors uniquely through a morphism `ring_quot s →ₐ[S]  B`.
 def lift_alg_hom {s : A → A → Prop} :
   { f : A →ₐ[S] B // ∀ ⦃x y⦄, s x y → f x = f y} ≃ (ring_quot s →ₐ[S] B) :=
 { to_fun := λ f', let f := (f' : A →ₐ[S] B) in
-  { to_fun := quot.lift f
+  { to_fun := λ x, quot.lift f
     begin
       rintros _ _ r,
       induction r,
       case of : _ _ r { exact f'.prop r, },
       case add_left : _ _ _ _ r' { simp [r'], },
       case mul_left : _ _ _ _ r' { simp [r'], },
       case mul_right : _ _ _ _ r' { simp [r'], },
-    end,
-    map_zero' := f.map_zero,
-    map_add' := by { rintros ⟨x⟩ ⟨y⟩, exact f.map_add x y, },
-    map_one' := f.map_one,
-    map_mul' := by { rintros ⟨x⟩ ⟨y⟩, exact f.map_mul x y, },
-    commutes' :=
-    begin
-      rintros x,
-      conv_rhs { rw [algebra.algebra_map_eq_smul_one, ←f.map_one, ←f.map_smul], },
-      rw algebra.algebra_map_eq_smul_one,
-      exact quot.lift_mk f f'.prop (x • 1),
-    end, },
+    end x.to_quot,
+    map_zero' := by simp [← zero_quot, f.map_zero],
+    map_add' := by { rintros ⟨⟨x⟩⟩ ⟨⟨y⟩⟩, simp [add_quot, f.map_add x y] },
+    map_one' := by simp [← one_quot, f.map_one],
+    map_mul' := by { rintros ⟨⟨x⟩⟩ ⟨⟨y⟩⟩, simp [mul_quot, f.map_mul x y], },
+    commutes' := by { rintros x, simp [← one_quot, smul_quot, algebra.algebra_map_eq_smul_one] } },
   inv_fun := λ F, ⟨F.comp (mk_alg_hom S s), λ _ _ h, by { dsimp, erw mk_alg_hom_rel S h }⟩,
   left_inv := λ f, by { ext, simp, refl },
   right_inv := λ F, by { ext, simp, refl } }

src/linear_algebra/clifford_algebra/conjugation.lean

@@ -71,7 +71,7 @@ by simp [reverse]
 by simp [reverse]
 
 @[simp] lemma reverse.map_one : reverse (1 : clifford_algebra Q) = 1 :=
-reverse.commutes 1
+by convert reverse.commutes (1 : R); simp
 
 @[simp] lemma reverse.map_mul (a b : clifford_algebra Q) :
   reverse (a * b) = reverse b * reverse a :=