refactor: introduce Ideal.IsTwoSided class for quotients of noncommutative rings

Mathlib/Algebra/Algebra/Operations.lean

@@ -313,9 +313,16 @@ protected theorem pow_zero : M ^ 0 = 1 := rfl
 
 protected theorem pow_succ {n : ℕ} : M ^ (n + 1) = M ^ n * M := rfl
 
+protected theorem pow_add {m n : ℕ} (h : n ≠ 0) : M ^ (m + n) = M ^ m * M ^ n :=
+  npowRec_add m n h _ M.one_mul
+
 protected theorem pow_one : M ^ 1 = M := by
   rw [Submodule.pow_succ, Submodule.pow_zero, Submodule.one_mul]
 
+/-- `Submodule.pow_succ` with the right hand side commuted. -/
+protected theorem pow_succ' {n : ℕ} (h : n ≠ 0) : M ^ (n + 1) = M * M ^ n := by
+  rw [add_comm, M.pow_add h, Submodule.pow_one]
+
 theorem pow_toAddSubmonoid {n : ℕ} (h : n ≠ 0) : (M ^ n).toAddSubmonoid = M.toAddSubmonoid ^ n := by
   induction n with
   | zero => exact (h rfl).elim

Mathlib/Algebra/GroupWithZero/Basic.lean

@@ -185,6 +185,15 @@ lemma sq_eq_zero_iff : a ^ 2 = 0 ↔ a = 0 := pow_eq_zero_iff two_ne_zero
 @[simp] lemma pow_eq_zero_iff' [Nontrivial M₀] : a ^ n = 0 ↔ a = 0 ∧ n ≠ 0 := by
   obtain rfl | hn := eq_or_ne n 0 <;> simp [*]
 
+theorem exists_right_inv_of_exists_left_inv {α} [MonoidWithZero α]
+    (h : ∀ a : α, a ≠ 0 → ∃ b : α, b * a = 1) {a : α} (ha : a ≠ 0) : ∃ b : α, a * b = 1 := by
+  obtain _ | _ := subsingleton_or_nontrivial α
+  · exact ⟨a, Subsingleton.elim _ _⟩
+  obtain ⟨b, hb⟩ := h a ha
+  obtain ⟨c, hc⟩ := h b (left_ne_zero_of_mul <| hb.trans_ne one_ne_zero)
+  refine ⟨b, ?_⟩
+  conv_lhs => rw [← one_mul (a * b), ← hc, mul_assoc, ← mul_assoc b, hb, one_mul, hc]
+
 end MonoidWithZero
 
 section CancelMonoidWithZero

Mathlib/Algebra/Module/LinearMap/Defs.lean

@@ -453,6 +453,8 @@ def _root_.RingHom.toSemilinearMap (f : R →+* S) : R →ₛₗ[f] S :=
   { f with
     map_smul' := f.map_mul }
 
+@[simp] theorem _root_.RingHom.coe_toSemilinearMap (f : R →+* S) : ⇑f.toSemilinearMap = f := rfl
+
 section
 
 variable [Semiring R₁] [Semiring R₂] [Semiring R₃]

Mathlib/Algebra/Module/Torsion.lean

@@ -143,10 +143,11 @@ open nonZeroDivisors
 
 section Defs
 
-variable (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M]
-
 namespace Submodule
 
+variable (R M : Type*) [CommSemiring R] [AddCommMonoid M] [Module R M]
+
+-- TODO: generalize to `Submodule S M` with `SMulCommClass R S M`.
 /-- The `a`-torsion submodule for `a` in `R`, containing all elements `x` of `M` such that
   `a • x = 0`. -/
 @[simps!]
@@ -190,6 +191,8 @@ end Submodule
 
 namespace Module
 
+variable (R M : Type*) [Semiring R] [AddCommMonoid M] [Module R M]
+
 /-- An `a`-torsion module is a module where every element is `a`-torsion. -/
 abbrev IsTorsionBy (a : R) :=
   ∀ ⦃x : M⦄, a • x = 0
@@ -207,9 +210,18 @@ abbrev IsTorsion' (S : Type*) [SMul S M] :=
 abbrev IsTorsion :=
   ∀ ⦃x : M⦄, ∃ a : R⁰, a • x = 0
 
-theorem isTorsionBySet_annihilator : IsTorsionBySet R M (Module.annihilator R M) :=
+theorem isTorsionBySet_annihilator : IsTorsionBySet R M (annihilator R M) :=
   fun _ r ↦ Module.mem_annihilator.mp r.2 _
 
+theorem isTorsionBy_iff_mem_annihilator {a : R} :
+    IsTorsionBy R M a ↔ a ∈ annihilator R M := by
+  rw [IsTorsionBy, mem_annihilator]
+
+theorem isTorsionBySet_iff_subset_annihilator {s : Set R} :
+    IsTorsionBySet R M s ↔ s ⊆ annihilator R M := by
+  simp_rw [IsTorsionBySet, Set.subset_def, SetLike.mem_coe, mem_annihilator]
+  rw [forall_comm, SetCoe.forall]
+
 end Module
 
 end Defs
@@ -223,10 +235,10 @@ variable {R M : Type*}
 
 section
 
-variable [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (a : R)
-
 namespace Submodule
 
+variable [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (a : R)
+
 @[simp]
 theorem smul_torsionBy (x : torsionBy R M a) : a • x = 0 :=
   Subtype.ext x.prop
@@ -291,13 +303,32 @@ open Submodule
 
 namespace Module
 
+variable [Semiring R] [AddCommMonoid M] [Module R M] (s : Set R) (a : R)
+
+theorem isTorsionBySet_of_subset {s t : Set R} (h : s ⊆ t)
+    (ht : IsTorsionBySet R M t) : IsTorsionBySet R M s :=
+  fun m r ↦ @ht m ⟨r, h r.2⟩
+
 @[simp]
 theorem isTorsionBySet_singleton_iff : IsTorsionBySet R M {a} ↔ IsTorsionBy R M a := by
   refine ⟨fun h x => @h _ ⟨_, Set.mem_singleton _⟩, fun h x => ?_⟩
   rintro ⟨b, rfl : b = a⟩; exact @h _
 
+theorem isTorsionBySet_iff_is_torsion_by_span :
+    IsTorsionBySet R M s ↔ IsTorsionBySet R M (Ideal.span s) := by
+  simpa only [isTorsionBySet_iff_subset_annihilator] using Ideal.span_le.symm
+
+theorem isTorsionBySet_span_singleton_iff : IsTorsionBySet R M (R ∙ a) ↔ IsTorsionBy R M a :=
+  (isTorsionBySet_iff_is_torsion_by_span _).symm.trans <| isTorsionBySet_singleton_iff _
+
+end Module
+
+namespace Module
+
+variable [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (a : R)
+
 theorem isTorsionBySet_iff_torsionBySet_eq_top :
-    IsTorsionBySet R M s ↔ Submodule.torsionBySet R M s = ⊤ :=
+    IsTorsionBySet R M s ↔ torsionBySet R M s = ⊤ :=
   ⟨fun h => eq_top_iff.mpr fun _ _ => (mem_torsionBySet_iff _ _).mpr <| @h _, fun h x => by
     rw [← mem_torsionBySet_iff, h]
     trivial⟩
@@ -307,14 +338,6 @@ theorem isTorsionBy_iff_torsionBy_eq_top : IsTorsionBy R M a ↔ torsionBy R M a
   rw [← torsionBySet_singleton_eq, ← isTorsionBySet_singleton_iff,
     isTorsionBySet_iff_torsionBySet_eq_top]
 
-theorem isTorsionBySet_iff_is_torsion_by_span :
-    IsTorsionBySet R M s ↔ IsTorsionBySet R M (Ideal.span s) := by
-  rw [isTorsionBySet_iff_torsionBySet_eq_top, isTorsionBySet_iff_torsionBySet_eq_top,
-    torsionBySet_eq_torsionBySet_span]
-
-theorem isTorsionBySet_span_singleton_iff : IsTorsionBySet R M (R ∙ a) ↔ IsTorsionBy R M a :=
-  (isTorsionBySet_iff_is_torsion_by_span _).symm.trans <| isTorsionBySet_singleton_iff _
-
 theorem isTorsionBySet_iff_subseteq_ker_lsmul :
     IsTorsionBySet R M s ↔ s ⊆ LinearMap.ker (LinearMap.lsmul R M) where
   mp h r hr := LinearMap.mem_ker.mpr <| LinearMap.ext fun x => @h x ⟨r, hr⟩
@@ -330,6 +353,8 @@ namespace Submodule
 
 open Module
 
+variable [CommSemiring R] [AddCommMonoid M] [Module R M] (s : Set R) (a : R)
+
 theorem torsionBySet_isTorsionBySet : IsTorsionBySet R (torsionBySet R M s) s :=
   fun ⟨_, hx⟩ a => Subtype.ext <| (mem_torsionBySet_iff _ _).mp hx a
 
@@ -434,10 +459,9 @@ end
 
 section NeedsGroup
 
-variable [CommRing R] [AddCommGroup M] [Module R M]
-
 namespace Submodule
 
+variable [CommRing R] [AddCommGroup M] [Module R M]
 variable {ι : Type*} [DecidableEq ι] {S : Finset ι}
 
 /-- If the `p i` are pairwise coprime, a `⨅ i, p i`-torsion module is the internal direct sum of
@@ -469,43 +493,54 @@ end Submodule
 
 namespace Module
 
+variable [Ring R] [AddCommGroup M] [Module R M]
 variable {I : Ideal R} {r : R}
 
 /-- can't be an instance because `hM` can't be inferred -/
 def IsTorsionBySet.hasSMul (hM : IsTorsionBySet R M I) : SMul (R ⧸ I) M where
-  smul b x := I.liftQ (LinearMap.lsmul R M)
-                ((isTorsionBySet_iff_subseteq_ker_lsmul _).mp hM) b x
+  smul b := QuotientAddGroup.lift I.toAddSubgroup (smulAddHom R M)
+    (by rwa [isTorsionBySet_iff_subset_annihilator] at hM) b
 
 /-- can't be an instance because `hM` can't be inferred -/
 abbrev IsTorsionBy.hasSMul (hM : IsTorsionBy R M r) : SMul (R ⧸ Ideal.span {r}) M :=
   ((isTorsionBySet_span_singleton_iff r).mpr hM).hasSMul
 
 @[simp]
-theorem IsTorsionBySet.mk_smul (hM : IsTorsionBySet R M I) (b : R) (x : M) :
+theorem IsTorsionBySet.mk_smul [I.IsTwoSided] (hM : IsTorsionBySet R M I) (b : R) (x : M) :
     haveI := hM.hasSMul
     Ideal.Quotient.mk I b • x = b • x :=
   rfl
 
 @[simp]
-theorem IsTorsionBy.mk_smul (hM : IsTorsionBy R M r) (b : R) (x : M) :
+theorem IsTorsionBy.mk_smul [(Ideal.span {r}).IsTwoSided] (hM : IsTorsionBy R M r) (b : R) (x : M) :
     haveI := hM.hasSMul
     Ideal.Quotient.mk (Ideal.span {r}) b • x = b • x :=
   rfl
 
 /-- An `(R ⧸ I)`-module is an `R`-module which `IsTorsionBySet R M I`. -/
-def IsTorsionBySet.module (hM : IsTorsionBySet R M I) : Module (R ⧸ I) M :=
+def IsTorsionBySet.module [I.IsTwoSided] (hM : IsTorsionBySet R M I) : Module (R ⧸ I) M :=
   letI := hM.hasSMul; I.mkQ_surjective.moduleLeft _ (IsTorsionBySet.mk_smul hM)
 
-instance IsTorsionBySet.isScalarTower (hM : IsTorsionBySet R M I)
+instance IsTorsionBySet.isScalarTower [I.IsTwoSided] (hM : IsTorsionBySet R M I)
     {S : Type*} [SMul S R] [SMul S M] [IsScalarTower S R M] [IsScalarTower S R R] :
     @IsScalarTower S (R ⧸ I) M _ (IsTorsionBySet.module hM).toSMul _ :=
   -- Porting note: still needed to be fed the Module R / I M instance
   @IsScalarTower.mk S (R ⧸ I) M _ (IsTorsionBySet.module hM).toSMul _
     (fun b d x => Quotient.inductionOn' d fun c => (smul_assoc b c x : _))
 
+/-- If a `R`-module `M` is annihilated by a two-sided ideal `I`, then the identity is a semilinear
+map from the `R`-module `M` to the `R ⧸ I`-module `M`. -/
+def IsTorsionBySet.semilinearMap [I.IsTwoSided] (hM : IsTorsionBySet R M I) :
+    let _ := hM.module; M →ₛₗ[Ideal.Quotient.mk I] M :=
+  let _ := hM.module
+  { toFun := id
+    map_add' := fun _ _ ↦ rfl
+    map_smul' := fun _ _ ↦ rfl }
+
 /-- An `(R ⧸ Ideal.span {r})`-module is an `R`-module for which `IsTorsionBy R M r`. -/
-abbrev IsTorsionBy.module (hM : IsTorsionBy R M r) : Module (R ⧸ Ideal.span {r}) M :=
-  ((isTorsionBySet_span_singleton_iff r).mpr hM).module
+abbrev IsTorsionBy.module [h : (Ideal.span {r}).IsTwoSided] (hM : IsTorsionBy R M r) :
+    Module (R ⧸ Ideal.span {r}) M := by
+  rw [Ideal.span] at h; exact ((isTorsionBySet_span_singleton_iff r).mpr hM).module
 
 /-- Any module is also a module over the quotient of the ring by the annihilator.
 Not an instance because it causes synthesis failures / timeouts. -/
@@ -540,34 +575,44 @@ lemma isTorsionBySet_quotient_set_smul :
   (isTorsionBySet_quotient_iff _ _).mpr fun _ _ h =>
     mem_set_smul_of_mem_mem h mem_top
 
-lemma isTorsionBy_quotient_element_smul :
-    IsTorsionBy R (M⧸r • (⊤ : Submodule R M)) r :=
-  (isTorsionBy_quotient_iff _ _).mpr (smul_mem_pointwise_smul · r ⊤ ⟨⟩)
-
 lemma isTorsionBySet_quotient_ideal_smul :
     IsTorsionBySet R (M⧸I • (⊤ : Submodule R M)) I :=
   (isTorsionBySet_quotient_iff _ _).mpr fun _ _ h => smul_mem_smul h ⟨⟩
 
-instance : Module (R ⧸ Ideal.span s) (M ⧸ s • (⊤ : Submodule R M)) :=
-  ((isTorsionBySet_iff_is_torsion_by_span s).mp
-    (isTorsionBySet_quotient_set_smul M s)).module
-
-instance : Module (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M)) :=
+instance [I.IsTwoSided] : Module (R ⧸ I) (M ⧸ I • (⊤ : Submodule R M)) :=
   (isTorsionBySet_quotient_ideal_smul M I).module
 
-instance : Module (R ⧸ Ideal.span {r}) (M ⧸ r • (⊤ : Submodule R M)) :=
-  (isTorsionBy_quotient_element_smul M r).module
-
-lemma Quotient.mk_smul_mk (r : R) (m : M) :
+lemma Quotient.mk_smul_mk [I.IsTwoSided] (r : R) (m : M) :
     Ideal.Quotient.mk I r •
       Submodule.Quotient.mk (p := (I • ⊤ : Submodule R M)) m =
       Submodule.Quotient.mk (p := (I • ⊤ : Submodule R M)) (r • m) :=
   rfl
 
 end Module
 
+namespace Module
+
+variable (M) [CommRing R] [AddCommGroup M] [Module R M] (s : Set R) (r : R)
+
+open Pointwise
+
+lemma isTorsionBy_quotient_element_smul :
+    IsTorsionBy R (M⧸r • (⊤ : Submodule R M)) r :=
+  (isTorsionBy_quotient_iff _ _).mpr (Submodule.smul_mem_pointwise_smul · r ⊤ ⟨⟩)
+
+instance : Module (R ⧸ Ideal.span s) (M ⧸ s • (⊤ : Submodule R M)) :=
+  ((isTorsionBySet_iff_is_torsion_by_span s).mp
+    (isTorsionBySet_quotient_set_smul M s)).module
+
+instance : Module (R ⧸ Ideal.span {r}) (M ⧸ r • (⊤ : Submodule R M)) :=
+  (isTorsionBy_quotient_element_smul M r).module
+
+end Module
+
 namespace Submodule
 
+variable [CommRing R] [AddCommGroup M] [Module R M]
+
 instance (I : Ideal R) : Module (R ⧸ I) (torsionBySet R M I) :=
   -- Porting note: times out without the (R := R)
   Module.IsTorsionBySet.module <| torsionBySet_isTorsionBySet (R := R) I

Mathlib/Algebra/RingQuot.lean

@@ -9,10 +9,7 @@ import Mathlib.RingTheory.Ideal.Quotient.Defs
 import Mathlib.RingTheory.Ideal.Span
 
 /-!
-# Quotients of non-commutative rings
-
-Unfortunately, ideals have only been developed in the commutative case as `Ideal`,
-and it's not immediately clear how one should formalise ideals in the non-commutative case.
+# Quotients of semirings
 
 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.

Mathlib/LinearAlgebra/Quotient/Defs.lean

@@ -107,6 +107,10 @@ theorem mk_sub : (mk (x - y) : M ⧸ p) = mk x - mk y :=
 
 protected nonrec lemma «forall» {P : M ⧸ p → Prop} : (∀ a, P a) ↔ ∀ a, P (mk a) := Quotient.forall
 
+theorem subsingleton_iff : Subsingleton (M ⧸ p) ↔ ∀ x : M, x ∈ p := by
+  rw [subsingleton_iff_forall_eq 0, Submodule.Quotient.forall]
+  simp_rw [Submodule.Quotient.mk_eq_zero]
+
 section SMul
 
 variable {S : Type*} [SMul S R] [SMul S M] [IsScalarTower S R M] (P : Submodule R M)

Mathlib/NumberTheory/Padics/RingHoms.lean

@@ -289,9 +289,9 @@ theorem ker_toZMod : RingHom.ker (toZMod : ℤ_[p] →+* ZMod p) = maximalIdeal
     · apply sub_zmodRepr_mem
 
 /-- The equivalence between the residue field of the `p`-adic integers and `ℤ/pℤ` -/
-def residueField : IsLocalRing.ResidueField ℤ_[p] ≃+* ZMod p := by
-  exact_mod_cast (@PadicInt.ker_toZMod p _) ▸ RingHom.quotientKerEquivOfSurjective
-    (ZMod.ringHom_surjective PadicInt.toZMod)
+def residueField : IsLocalRing.ResidueField ℤ_[p] ≃+* ZMod p :=
+  (Ideal.quotEquivOfEq PadicInt.ker_toZMod.symm).trans <|
+    RingHom.quotientKerEquivOfSurjective (ZMod.ringHom_surjective PadicInt.toZMod)
 
 /-- `appr n x` gives a value `v : ℕ` such that `x` and `↑v : ℤ_p` are congruent mod `p^n`.
 See `appr_spec`. -/

Mathlib/RingTheory/AdicCompletion/Algebra.lean

@@ -184,7 +184,7 @@ theorem evalₐ_mkₐ (n : ℕ) (x : AdicCauchySequence I R) :
 theorem Ideal.mk_eq_mk {m n : ℕ} (hmn : m ≤ n) (r : AdicCauchySequence I R) :
     Ideal.Quotient.mk (I ^ m) (r.val n) = Ideal.Quotient.mk (I ^ m) (r.val m) := by
   have h : I ^ m = I ^ m • ⊤ := by simp
-  rw [h, ← Ideal.Quotient.mk_eq_mk, ← Ideal.Quotient.mk_eq_mk]
+  rw [← Ideal.Quotient.mk_eq_mk, ← Ideal.Quotient.mk_eq_mk, h]
   exact (r.property hmn).symm
 
 theorem smul_mk {m n : ℕ} (hmn : m ≤ n) (r : AdicCauchySequence I R)

Mathlib/RingTheory/Ideal/Basic.lean

@@ -56,6 +56,9 @@ def pi : Ideal (ι → α) where
 theorem mem_pi (x : ι → α) : x ∈ I.pi ι ↔ ∀ i, x i ∈ I :=
   Iff.rfl
 
+instance (priority := low) [I.IsTwoSided] : (I.pi ι).IsTwoSided :=
+  ⟨fun _b hb i ↦ mul_mem_right _ _ (hb i)⟩
+
 end Pi
 
 end Ideal