[Merged by Bors] - feat(algebra/ring_quot): quotients of noncommutative rings

src/algebra/group/hom.lean

@@ -81,6 +81,10 @@ lemma to_fun_eq_coe (f : M →* N) : f.to_fun = f := rfl
 @[simp, to_additive]
 lemma coe_mk (f : M → N) (h1 hmul) : ⇑(monoid_hom.mk f h1 hmul) = f := rfl
 
+@[to_additive]
+theorem congr_fun {f g : M →* N} (h : f = g) (x : M) : f x = g x :=
+congr_arg (λ h : M →* N, h x) h
+
 @[to_additive]
 lemma coe_inj ⦃f g : M →* N⦄ (h : (f : M → N) = g) : f = g :=
 by cases f; cases g; cases h; refl

src/algebra/ring/basic.lean

@@ -231,6 +231,9 @@ lemma to_fun_eq_coe (f : α →+* β) : f.to_fun = f := rfl
 
 variables (f : α →+* β) {x y : α} {rα rβ}
 
+theorem congr_fun {f g : α →+* β} (h : f = g) (x : α) : f x = g x :=
+congr_arg (λ h : α →+* β, h x) h
+
 theorem coe_inj ⦃f g : α →+* β⦄ (h : (f : α → β) = g) : f = g :=
 by cases f; cases g; cases h; refl
 

src/algebra/ring_quot.lean

@@ -0,0 +1,274 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import ring_theory.ideal.basic
+import ring_theory.algebra
+
+/-!
+# Quotients of non-commutative rings
+
+Unfortunately, ideals have only been developed in the commutative case,
+and it's not immediately clear how one should formalise ideals in the non-commutative case.
+
+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!
+
+Since everything runs in parallel for quotients of `R`-algebras, we do that case at the same time.
+-/
+
+universes u₁ u₂ u₃ u₄
+
+variables {R : Type u₁} [semiring R]
+variables (S : Type u₂) [comm_semiring S]
+variables {A : Type u₃} [semiring A] [algebra S A]
+
+namespace ring_quot
+
+/--
+The quotient by the transitive closure of this relation is the quotient
+by the ideal generated by `r`.
+-/
+inductive rel (r : R → R → Prop) : R → R → Prop
+| of {x y : R} (h : r x y) : rel x y
+| add {a b c} : rel a b → rel (a + c) (b + c)
+| mul_left {a b c} : rel a b → rel (a * c) (b * c)
+| mul_right {a b c} : rel a b → rel (c * a) (c * b)
+
+end ring_quot
+
+/-- The quotient of a ring by an arbitrary relation. -/
+def ring_quot (r : R → R → Prop) := quot (ring_quot.rel r)
+
+namespace ring_quot
+
+instance (r : R → R → Prop) : semiring (ring_quot r) :=
+{ add           := quot.map₂ (+)
+    (λ c a b h, by { rw [add_comm c a, add_comm c b], exact rel.add h, })
+    (λ _ _ _, rel.add),
+  add_assoc     := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, change quot.mk _ _ = _, rw add_assoc, refl, },
+  zero          := quot.mk _ 0,
+  zero_add      := by { rintros ⟨⟩, change quot.mk _ _ = _, rw zero_add, },
+  add_zero      := by { rintros ⟨⟩, change quot.mk _ _ = _, rw add_zero, },
+  zero_mul      := by { rintros ⟨⟩, change quot.mk _ _ = _, rw zero_mul, },
+  mul_zero      := by { rintros ⟨⟩, change quot.mk _ _ = _, rw mul_zero, },
+  add_comm      := by { rintros ⟨⟩ ⟨⟩, change quot.mk _ _ = _, rw add_comm, refl, },
+  mul           := quot.map₂ (*) (λ _ _ _, rel.mul_right) (λ _ _ _, rel.mul_left),
+  mul_assoc     := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, change quot.mk _ _ = _, rw mul_assoc, refl, },
+  one           := quot.mk _ 1,
+  one_mul       := by { rintros ⟨⟩, change quot.mk _ _ = _, rw one_mul, },
+  mul_one       := by { rintros ⟨⟩, change quot.mk _ _ = _, rw mul_one, },
+  left_distrib  := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, change quot.mk _ _ = _, rw left_distrib, refl, },
+  right_distrib := by { rintros ⟨⟩ ⟨⟩ ⟨⟩, change quot.mk _ _ = _, rw right_distrib, refl, }, }
+
+instance {R : Type u₁} [ring R] (r : R → R → Prop) : ring (ring_quot r) :=
+{ neg           := quot.map (λ a, -a)
+    (λ a b h, by simp only [neg_eq_neg_one_mul a, neg_eq_neg_one_mul b, rel.mul_right h]),
+  add_left_neg  := by { rintros ⟨⟩, change quot.mk _ _ = _, rw add_left_neg, refl, },
+  .. (ring_quot.semiring r) }
+
+instance {R : Type u₁} [comm_semiring R] (r : R → R → Prop) : comm_semiring (ring_quot r) :=
+{ mul_comm := by { rintros ⟨⟩ ⟨⟩, change quot.mk _ _ = _, rw mul_comm, refl, }
+  .. (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 a, (quot.mk _ (r • 1)) * a,
+  to_fun    := λ r, quot.mk _ (r • 1),
+  map_one'  := by { rw one_smul, refl, },
+  map_mul'  := λ r s, by { change _ = quot.mk _ _, simp [mul_smul], },
+  map_zero' := by { rw zero_smul, refl, },
+  map_add'  := λ r s, by { change _ = quot.mk _ _, rw add_smul, },
+  commutes' := λ r, by { rintros ⟨a⟩, change quot.mk _ _ = quot.mk _ _, simp, },
+  smul_def' := λ r u, rfl, }
+
+instance (r : R → R → Prop) : inhabited (ring_quot r) := ⟨0⟩
+
+/--
+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, }
+
+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)
+
+lemma mk_ring_hom_surjective (r : R → R → Prop) : function.surjective (mk_ring_hom r) :=
+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)
+  (w : f.comp (mk_ring_hom r) = g.comp (mk_ring_hom r)) : f = g :=
+begin
+  ext,
+  rcases mk_ring_hom_surjective r x with ⟨x, rfl⟩,
+  exact (congr_arg (λ h : R →+* T, h x) w), -- TODO should we have `ring_hom.congr` for this?
+end
+
+variables  {T : Type u₄} [semiring T]
+
+/--
+Any ring homomorphism `f : R →+* T` which respects a relation `r : R → R → Prop`
+factors through a morphism `ring_quot r →+* T`.
+-/
+def lift (f : R →+* T) {r : R → R → Prop} (w : ∀ {x y}, r x y → f x = f y) :
+  ring_quot r →+* T :=
+{ to_fun := quot.lift f
+  begin
+    rintros _ _ r,
+    induction r with a b r a b c r r' a b c r r' a b c r r',
+    { exact w r, },
+    { simp [r'], },
+    { simp [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, }, }
+
+@[simp]
+lemma lift_mk_ring_hom (f : R →+* T) {r : R → R → Prop} (w : ∀ {x y}, r x y → f x = f y) :
+  (lift f @w).comp (mk_ring_hom r) = f :=
+by { ext, simp, refl, }
+
+lemma lift_unique (f : R →+* T) {r : R → R → Prop} (w : ∀ {x y}, r x y → f x = f y)
+  (g : ring_quot r →+* T) (h : g.comp (mk_ring_hom r) = f) : g = lift f @w :=
+by { ext, simp [h], }
+
+lemma eq_lift_comp_mk_ring_hom {r : R → R → Prop} (f : ring_quot r →+* T) :
+  f = lift (f.comp (mk_ring_hom r)) (λ x y h, by { dsimp, rw mk_ring_hom_rel h, }) :=
+by { ext, simp, }
+
+section comm_ring
+/-!
+We now verify that in the case of a commutative ring, the `ring_quot` construction
+agrees with the quotient by the appropriate ideal.
+-/
+
+variables {B : Type u₁} [comm_ring B]
+
+/-- The universal ring homomorphism from `ring_quot r` to `(ideal.of_rel r).quotient`. -/
+def ring_quot_to_ideal_quotient (r : B → B → Prop) :
+  ring_quot r →+* (ideal.of_rel r).quotient :=
+lift
+  (ideal.quotient.mk (ideal.of_rel r))
+  (λ x y h, quot.sound (submodule.mem_Inf.mpr (λ p w, w ⟨x, y, h, rfl⟩)))
+
+@[simp] lemma ring_quot_to_ideal_quotient_apply (r : B → B → Prop) (x : B) :
+  ring_quot_to_ideal_quotient r (mk_ring_hom r x) = ideal.quotient.mk _ x := rfl
+
+/-- The universal ring homomorphism from `(ideal.of_rel r).quotient` to `ring_quot r`. -/
+def ideal_quotient_to_ring_quot (r : B → B → Prop) :
+  (ideal.of_rel r).quotient →+* ring_quot r :=
+ideal.quotient.lift (ideal.of_rel r) (mk_ring_hom r)
+begin
+  intros x h,
+  apply submodule.span_induction h,
+  { rintros - ⟨a,b,h,rfl⟩,
+    rw [ring_hom.map_sub, mk_ring_hom_rel h, sub_self], },
+  { simp, },
+  { intros a b ha hb, simp [ha, hb], },
+  { intros a x hx, simp [hx], },
+end
+
+@[simp] lemma ideal_quotient_to_ring_quot_apply (r : B → B → Prop) (x : B) :
+  ideal_quotient_to_ring_quot r (ideal.quotient.mk _ x) = mk_ring_hom r x := rfl
+
+/--
+The ring equivalence between `ring_quot r` and `(ideal.of_rel r).quotient`
+-/
+def ring_quot_equiv_ideal_quotient (r : B → B → Prop) :
+  ring_quot r ≃+* (ideal.of_rel r).quotient :=
+ring_equiv.of_hom_inv (ring_quot_to_ideal_quotient r) (ideal_quotient_to_ring_quot r)
+  (by { ext, simp, }) (by { ext ⟨x⟩, simp, })
+
+end comm_ring
+
+section algebra
+
+/--
+The quotient map from an `S`-algebra to its quotient, as a homomorphism of `S`-algebras.
+-/
+def mk_alg_hom (s : A → A → Prop) : A →ₐ[S] ring_quot s :=
+{ commutes' := λ r, show quot.mk _ _ = quot.mk _ _, by rw [algebra.smul_def'', mul_one],
+  ..mk_ring_hom s }
+
+@[simp]
+lemma mk_alg_hom_coe (s : A → A → Prop) : (mk_alg_hom S s : A →+* ring_quot s) = mk_ring_hom s :=
+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)
+
+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, }
+
+variables {B : Type u₄} [semiring B] [algebra S B]
+
+@[ext]
+lemma ring_quot_ext' {s : A → A → Prop}
+  (f g : ring_quot s →ₐ[S] B) (w : f.comp (mk_alg_hom S s) = g.comp (mk_alg_hom S s)) : f = g :=
+begin
+  ext,
+  rcases mk_alg_hom_surjective S s x with ⟨x, rfl⟩,
+  exact (congr_arg (λ h : A →ₐ[S] B, h x) w), -- TODO should we have `alg_hom.congr` for this?
+end
+
+/--
+Any `S`-algebra homomorphism `f : A →ₐ[S] B` which respects a relation `s : A → A → Prop`
+factors through a morphism `ring_quot s →ₐ[S]  B`.
+-/
+def lift_alg_hom (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ {x y}, s x y → f x = f y) :
+  ring_quot s →ₐ[S] B :=
+{ to_fun := quot.lift f
+  begin
+    rintros _ _ r,
+    induction r with a b r a b c r r' a b c r r' a b c r r',
+    { exact w r, },
+    { simp [r'], },
+    { simp [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], },
+    exact quot.lift_beta f @w (x • 1),
+  end, }
+
+@[simp]
+lemma lift_alg_hom_mk_alg_hom (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ {x y}, s x y → f x = f y) :
+  (lift_alg_hom S f @w).comp (mk_alg_hom S s) = f :=
+by { ext, simp, refl, }
+
+lemma lift_alg_hom_unique (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ {x y}, s x y → f x = f y)
+  (g : ring_quot s →ₐ[S] B) (h : g.comp (mk_alg_hom S s) = f) : g = lift_alg_hom S f @w :=
+by { ext, simp [h], }
+
+lemma eq_lift_alg_hom_comp_mk_alg_hom {s : A → A → Prop} (f : ring_quot s →ₐ[S] B) :
+  f = lift_alg_hom S (f.comp (mk_alg_hom S s)) (λ x y h, by { dsimp, erw mk_alg_hom_rel S h, }) :=
+by { ext, simp, }
+
+end algebra
+
+attribute [irreducible] ring_quot mk_ring_hom mk_alg_hom lift lift_alg_hom
+
+end ring_quot

src/data/equiv/ring.lean

@@ -199,6 +199,25 @@ equiv.symm_apply_apply (e.to_equiv)
 lemma to_ring_hom_trans (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
   (e₁.trans e₂).to_ring_hom = e₂.to_ring_hom.comp e₁.to_ring_hom := rfl
 
+/--
+Construct an equivalence of rings from homomorphisms in both directions, which are inverses.
+-/
+def of_hom_inv (hom : R →+* S) (inv : S →+* R)
+  (hom_inv_id : inv.comp hom = ring_hom.id R) (inv_hom_id : hom.comp inv = ring_hom.id S) :
+  R ≃+* S :=
+{ inv_fun := inv,
+  left_inv := λ x, ring_hom.congr_fun hom_inv_id x,
+  right_inv := λ x, ring_hom.congr_fun inv_hom_id x,
+  ..hom }
+
+@[simp]
+lemma of_hom_inv_apply (hom : R →+* S) (inv : S →+* R) (hom_inv_id inv_hom_id) (r : R) :
+  (of_hom_inv hom inv hom_inv_id inv_hom_id) r = hom r := rfl
+
+@[simp]
+lemma of_hom_inv_symm_apply (hom : R →+* S) (inv : S →+* R) (hom_inv_id inv_hom_id) (s : S) :
+  (of_hom_inv hom inv hom_inv_id inv_hom_id).symm s = inv s := rfl
+
 end semiring_hom
 
 end ring_equiv

src/linear_algebra/basic.lean

@@ -536,6 +536,9 @@ lemma bot_ne_top [nontrivial M] : (⊥ : submodule R M) ≠ ⊤ :=
 by rw [infi, Inf_coe]; ext a; simp; exact
 ⟨λ h i, h _ i rfl, λ h i x e, e ▸ h _⟩
 
+@[simp] lemma mem_Inf {S : set (submodule R M)} {x : M} : x ∈ Inf S ↔ ∀ p ∈ S, x ∈ p :=
+set.mem_bInter_iff
+
 @[simp] theorem mem_infi {ι} (p : ι → submodule R M) :
   x ∈ (⨅ i, p i) ↔ ∀ i, x ∈ p i :=
 by rw [← mem_coe, infi_coe, mem_Inter]; refl

src/ring_theory/ideal/basic.lean

@@ -18,7 +18,9 @@ This file defines `ideal R`, the type of ideals over a commutative ring `R`.
 
 ## TODO
 
-Support one-sided ideals, and ideals over non-commutative rings
+Support one-sided ideals, and ideals over non-commutative rings.
+
+See `algebra.ring_quot` for quotients of non-commutative rings.
 -/
 
 universes u v w
@@ -151,6 +153,12 @@ end
 lemma span_singleton_mul_left_unit {a : α} (h2 : is_unit a) (x : α) :
   span ({a * x} : set α) = span {x} := by rw [mul_comm, span_singleton_mul_right_unit h2]
 
+/--
+The ideal generated by an arbitrary binary relation.
+-/
+def of_rel (r : α → α → Prop) : ideal α :=
+submodule.span α { x | ∃ (a b) (h : r a b), x = a - b }
+
 /-- An ideal `P` of a ring `R` is prime if `P ≠ R` and `xy ∈ P → x ∈ P ∨ y ∈ P` -/
 @[class] def is_prime (I : ideal α) : Prop :=
 I ≠ ⊤ ∧ ∀ {x y : α}, x * y ∈ I → x ∈ I ∨ y ∈ I

src/topology/instances/real_vector_space.lean

@@ -22,7 +22,7 @@ namespace add_monoid_hom
 /-- A continuous additive map between two vector spaces over `ℝ` is `ℝ`-linear. -/
 lemma map_real_smul (f : E →+ F) (hf : continuous f) (c : ℝ) (x : E) :
   f (c • x) = c • f x :=
-suffices (λ c : ℝ, f (c • x)) = λ c : ℝ, c • f x, from congr_fun this c,
+suffices (λ c : ℝ, f (c • x)) = λ c : ℝ, c • f x, from _root_.congr_fun this c,
 dense_embedding_of_rat.dense.equalizer
   (hf.comp $ continuous_id.smul continuous_const)
   (continuous_id.smul continuous_const)