feat(Algebra/Ring/Subring): drop associativity condition for Subrings (#36735)

cf. Item 4 in #7987.

Author: yhx-12243

Counterexamples/DimensionPolynomial.lean

@@ -78,7 +78,8 @@ theorem ringKrullDim_polynomial_A_eq_three : ringKrullDim (A k)[X] = 3 := by
         (PowerSeries.constantCoeff.comp (A k).subtype).rangeRestrict
     exact fun _ ⟨⟨_, ⟨u, _⟩⟩, _⟩ ↦ ⟨u, ⟨by simp, by simp_all⟩⟩
   have h_phi : RatFunc.C.comp φ = PowerSeries.constantCoeff.comp (A k).subtype := RingHom.ext
-    fun x ↦ by simp [φ, ← Subring.coe_equivMapOfInjective_apply (hf := RatFunc.C_injective)]
+    fun x ↦ by simp [φ, ← Subring.coe_equivMapOfInjective_apply
+      (S := RatFunc k) (hf := RatFunc.C_injective)]
   let f : (A k)[X] →+* (RatFunc k)⟦X⟧ := eval₂RingHom (A k).subtype (PowerSeries.C RatFunc.X)
   let Q : PrimeSpectrum (A k)[X] := ⟨RingHom.ker f, RingHom.ker_isPrime f⟩
   let g : (A k)[X] →+* k[X] := mapRingHom φ

Mathlib/Algebra/Ring/InjSurj.lean

@@ -56,7 +56,7 @@ protected abbrev distrib [Distrib R] (add : ∀ x y, f (x + y) = f x + f y)
 
 /-- A type endowed with `-` and `*` has distributive negation, if it admits an injective map that
 preserves `-` and `*` to a type which has distributive negation. -/
--- -- See note [reducible non-instances]
+-- See note [reducible non-instances]
 protected abbrev hasDistribNeg (f : S → R) (hf : Injective f) [Mul R] [HasDistribNeg R]
     (neg : ∀ a, f (-a) = -f a)
     (mul : ∀ a b, f (a * b) = f a * f b) : HasDistribNeg S :=
@@ -215,7 +215,14 @@ protected abbrev nonUnitalCommSemiring [NonUnitalCommSemiring R] (f : S → R)
   toNonUnitalSemiring := hf.nonUnitalSemiring f zero add mul nsmul
   __ := hf.commSemigroup f mul
 
--- `NonAssocCommSemiring` currently doesn't exist
+/-- Pullback a `NonAssocCommSemiring` instance along an injective function. -/
+-- See note [reducible non-instances]
+protected abbrev nonAssocCommSemiring [NonAssocCommSemiring R] (f : S → R)
+    (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
+    (mul : ∀ x y, f (x * y) = f x * f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
+    (natCast : ∀ n : ℕ, f n = n) : NonAssocCommSemiring S where
+  toNonAssocSemiring := hf.nonAssocSemiring f zero one add mul nsmul natCast
+  __ := hf.commMagma f mul
 
 /-- Pullback a `CommSemiring` instance along an injective function. -/
 -- See note [reducible non-instances]
@@ -238,7 +245,7 @@ protected abbrev nonUnitalNonAssocCommRing [NonUnitalNonAssocCommRing R] (f : S
   __ := hf.nonUnitalNonAssocCommSemiring f zero add mul nsmul
 
 /-- Pullback a `NonUnitalCommRing` instance along an injective function. -/
--- -- See note [reducible non-instances]
+-- See note [reducible non-instances]
 protected abbrev nonUnitalCommRing [NonUnitalCommRing R] (f : S → R)
     (hf : Injective f) (zero : f 0 = 0) (add : ∀ x y, f (x + y) = f x + f y)
     (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
@@ -247,8 +254,19 @@ protected abbrev nonUnitalCommRing [NonUnitalCommRing R] (f : S → R)
   toNonUnitalRing := hf.nonUnitalRing f zero add mul neg sub nsmul zsmul
   __ := hf.nonUnitalNonAssocCommRing f zero add mul neg sub nsmul zsmul
 
+/-- Pullback a `NonAssocCommRing` instance along an injective function. -/
+-- See note [reducible non-instances]
+protected abbrev nonAssocCommRing [NonAssocCommRing R] (f : S → R)
+    (hf : Injective f) (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
+    (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
+    (sub : ∀ x y, f (x - y) = f x - f y) (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
+    (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
+    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : NonAssocCommRing S where
+  toNonAssocRing := hf.nonAssocRing f zero one add mul neg sub nsmul zsmul natCast intCast
+  __ := hf.nonUnitalNonAssocCommRing f zero add mul neg sub nsmul zsmul
+
 /-- Pullback a `CommRing` instance along an injective function. -/
--- -- See note [reducible non-instances]
+-- See note [reducible non-instances]
 protected abbrev commRing [CommRing R]
     (zero : f 0 = 0) (one : f 1 = 1) (add : ∀ x y, f (x + y) = f x + f y)
     (mul : ∀ x y, f (x * y) = f x * f y) (neg : ∀ x, f (-x) = -f x)
@@ -438,6 +456,15 @@ protected abbrev nonUnitalCommSemiring [NonUnitalCommSemiring R] (zero : f 0 = 0
   toNonUnitalSemiring := hf.nonUnitalSemiring f zero add mul nsmul
   __ := hf.commSemigroup f mul
 
+/-- Pushforward a `NonAssocCommSemiring` instance along a surjective function. -/
+-- See note [reducible non-instances]
+protected abbrev nonAssocCommSemiring [NonAssocCommSemiring R] (zero : f 0 = 0) (one : f 1 = 1)
+    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x)
+    (natCast : ∀ n : ℕ, f n = n) : NonAssocCommSemiring S where
+  toNonAssocSemiring := hf.nonAssocSemiring f zero one add mul nsmul natCast
+  __ := hf.commMagma f mul
+
 /-- Pushforward a `CommSemiring` instance along a surjective function. -/
 -- See note [reducible non-instances]
 protected abbrev commSemiring [CommSemiring R] (zero : f 0 = 0) (one : f 1 = 1)
@@ -467,6 +494,16 @@ protected abbrev nonUnitalCommRing [NonUnitalCommRing R] (zero : f 0 = 0)
   toNonUnitalRing := hf.nonUnitalRing f zero add mul neg sub nsmul zsmul
   __ := hf.nonUnitalNonAssocCommRing f zero add mul neg sub nsmul zsmul
 
+/-- Pushforward a `NonAssocCommRing` instance along a surjective function. -/
+-- See note [reducible non-instances]
+protected abbrev nonAssocCommRing [NonAssocCommRing R] (zero : f 0 = 0) (one : f 1 = 1)
+    (add : ∀ x y, f (x + y) = f x + f y) (mul : ∀ x y, f (x * y) = f x * f y)
+    (neg : ∀ x, f (-x) = -f x) (sub : ∀ x y, f (x - y) = f x - f y)
+    (nsmul : ∀ (n : ℕ) (x), f (n • x) = n • f x) (zsmul : ∀ (n : ℤ) (x), f (n • x) = n • f x)
+    (natCast : ∀ n : ℕ, f n = n) (intCast : ∀ n : ℤ, f n = n) : NonAssocCommRing S where
+  toNonAssocRing := hf.nonAssocRing f zero one add mul neg sub nsmul zsmul natCast intCast
+  __ := hf.nonAssocCommSemiring f zero one add mul nsmul natCast
+
 /-- Pushforward a `CommRing` instance along a surjective function. -/
 -- See note [reducible non-instances]
 protected abbrev commRing [CommRing R] (zero : f 0 = 0) (one : f 1 = 1)

Mathlib/Algebra/Ring/Subring/Basic.lean

@@ -66,9 +66,9 @@ assert_not_exists IsOrderedRing
 
 universe u v w
 
-variable {R : Type u} {S : Type v} {T : Type w} [Ring R]
+variable {R : Type u} {S : Type v} {T : Type w} [NonAssocRing R]
 
-variable [Ring S] [Ring T]
+variable [NonAssocRing S] [NonAssocRing T]
 
 namespace Subring
 variable {s t : Subring R}
@@ -115,8 +115,8 @@ namespace Subring
 variable (s : Subring R)
 
 /-- Product of a list of elements in a subring is in the subring. -/
-protected theorem list_prod_mem {l : List R} : (∀ x ∈ l, x ∈ s) → l.prod ∈ s :=
-  list_prod_mem
+protected theorem list_prod_mem {R} [Ring R] (s : Subring R) {l : List R} :
+    (∀ x ∈ l, x ∈ s) → l.prod ∈ s := list_prod_mem
 
 /-- Sum of a list of elements in a subring is in the subring. -/
 protected theorem list_sum_mem {l : List R} : (∀ x ∈ l, x ∈ s) → l.sum ∈ s :=
@@ -174,17 +174,17 @@ theorem coe_top : ((⊤ : Subring R) : Set R) = Set.univ :=
 def topEquiv : (⊤ : Subring R) ≃+* R :=
   Subsemiring.topEquiv
 
-instance {R : Type*} [Ring R] [Fintype R] : Fintype (⊤ : Subring R) :=
+instance {R : Type*} [NonAssocRing R] [Fintype R] : Fintype (⊤ : Subring R) :=
   (inferInstance : Fintype (⊤ : Set R))
 
-theorem card_top (R) [Ring R] [Fintype R] : Fintype.card (⊤ : Subring R) = Fintype.card R :=
+theorem card_top (R) [NonAssocRing R] [Fintype R] : Fintype.card (⊤ : Subring R) = Fintype.card R :=
   Fintype.card_congr topEquiv.toEquiv
 
 /-! ## comap -/
 
 
 /-- The preimage of a subring along a ring homomorphism is a subring. -/
-def comap {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (s : Subring S) : Subring R :=
+def comap (f : R →+* S) (s : Subring S) : Subring R :=
   { s.toSubmonoid.comap (f : R →* S), s.toAddSubgroup.comap (f : R →+ S) with
     carrier := f ⁻¹' s.carrier }
 
@@ -204,7 +204,7 @@ theorem comap_comap (s : Subring T) (g : S →+* T) (f : R →+* S) :
 
 
 /-- The image of a subring along a ring homomorphism is a subring. -/
-def map {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) (s : Subring R) : Subring S :=
+def map (f : R →+* S) (s : Subring R) : Subring S :=
   { s.toSubmonoid.map (f : R →* S), s.toAddSubgroup.map (f : R →+ S) with
     carrier := f '' s.carrier }
 
@@ -250,7 +250,7 @@ variable (g : S →+* T) (f : R →+* S)
 
 
 /-- The range of a ring homomorphism, as a subring of the target. See Note [range copy pattern]. -/
-def range {R : Type u} {S : Type v} [Ring R] [Ring S] (f : R →+* S) : Subring S :=
+def range (f : R →+* S) : Subring S :=
   ((⊤ : Subring R).map f).copy (Set.range f) Set.image_univ.symm
 
 @[simp]
@@ -384,18 +384,18 @@ theorem center_toSubsemiring : (center R).toSubsemiring = Subsemiring.center R :
 
 variable {R}
 
-theorem mem_center_iff {z : R} : z ∈ center R ↔ ∀ g, g * z = z * g :=
+theorem mem_center_iff {R : Type*} [Ring R] {z : R} : z ∈ center R ↔ ∀ g, g * z = z * g :=
   Subsemigroup.mem_center_iff
 
-instance decidableMemCenter [DecidableEq R] [Fintype R] : DecidablePred (· ∈ center R) := fun _ =>
-  decidable_of_iff' _ mem_center_iff
+instance decidableMemCenter {R} [Ring R] [DecidableEq R] [Fintype R] :
+    DecidablePred (· ∈ center R) := fun _ => decidable_of_iff' _ mem_center_iff
 
 @[simp]
 theorem center_eq_top (R) [CommRing R] : center R = ⊤ :=
   SetLike.coe_injective (Set.center_eq_univ R)
 
 /-- The center is commutative. -/
-instance : CommRing (center R) :=
+instance {R} [Ring R] : CommRing (center R) :=
   { (inferInstance : CommSemiring (Subsemiring.center R)), (center R).toRing with }
 
 /-- The center of isomorphic (not necessarily associative) rings are isomorphic. -/
@@ -438,40 +438,40 @@ end DivisionRing
 section Centralizer
 
 /-- The centralizer of a set inside a ring as a `Subring`. -/
-def centralizer (s : Set R) : Subring R :=
+def centralizer {R} [Ring R] (s : Set R) : Subring R :=
   { Subsemiring.centralizer s with neg_mem' := Set.neg_mem_centralizer }
 
 @[simp, norm_cast]
-theorem coe_centralizer (s : Set R) : (centralizer s : Set R) = s.centralizer :=
+theorem coe_centralizer {R} [Ring R] (s : Set R) : (centralizer s : Set R) = s.centralizer :=
   rfl
 
-theorem centralizer_toSubmonoid (s : Set R) :
+theorem centralizer_toSubmonoid {R} [Ring R] (s : Set R) :
     (centralizer s).toSubmonoid = Submonoid.centralizer s :=
   rfl
 
-theorem centralizer_toSubsemiring (s : Set R) :
+theorem centralizer_toSubsemiring {R} [Ring R] (s : Set R) :
     (centralizer s).toSubsemiring = Subsemiring.centralizer s :=
   rfl
 
-theorem centralizer_toNonUnitalSubring (s : Set R) :
+theorem centralizer_toNonUnitalSubring {R} [Ring R] (s : Set R) :
     (centralizer s).toNonUnitalSubring = NonUnitalSubring.centralizer s :=
   rfl
 
-theorem mem_centralizer_iff {s : Set R} {z : R} : z ∈ centralizer s ↔ ∀ g ∈ s, g * z = z * g :=
-  Iff.rfl
+theorem mem_centralizer_iff {R} [Ring R] {s : Set R} {z : R} :
+    z ∈ centralizer s ↔ ∀ g ∈ s, g * z = z * g := Iff.rfl
 
-theorem center_le_centralizer (s) : center R ≤ centralizer s :=
+theorem center_le_centralizer {R} [Ring R] (s) : center R ≤ centralizer s :=
   s.center_subset_centralizer
 
-theorem centralizer_le (s t : Set R) (h : s ⊆ t) : centralizer t ≤ centralizer s :=
+theorem centralizer_le {R} [Ring R] (s t : Set R) (h : s ⊆ t) : centralizer t ≤ centralizer s :=
   Set.centralizer_subset h
 
 @[simp]
-theorem centralizer_eq_top_iff_subset {s : Set R} : centralizer s = ⊤ ↔ s ⊆ center R :=
+theorem centralizer_eq_top_iff_subset {R} [Ring R] {s : Set R} : centralizer s = ⊤ ↔ s ⊆ center R :=
   SetLike.ext'_iff.trans Set.centralizer_eq_top_iff_subset
 
 @[simp]
-theorem centralizer_univ : centralizer Set.univ = center R :=
+theorem centralizer_univ {R} [Ring R] : centralizer Set.univ = center R :=
   SetLike.ext' (Set.centralizer_univ R)
 
 end Centralizer
@@ -589,19 +589,19 @@ theorem mem_closure_iff {s : Set R} {x} :
       | add _ _ _ _ h₁ h₂ => exact add_mem h₁ h₂
       | neg _ _ h => exact neg_mem h⟩
 
-lemma closure_le_centralizer_centralizer (s : Set R) :
+lemma closure_le_centralizer_centralizer {R} [Ring R] (s : Set R) :
     closure s ≤ centralizer (centralizer s) :=
   closure_le.mpr Set.subset_centralizer_centralizer
 
 /-- If all elements of `s : Set A` commute pairwise, then `closure s` is a commutative ring. -/
-abbrev closureCommRingOfComm {s : Set R} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) :
+abbrev closureCommRingOfComm {R} [Ring R] {s : Set R} (hcomm : ∀ x ∈ s, ∀ y ∈ s, x * y = y * x) :
     CommRing (closure s) :=
   { (closure s).toRing with
     mul_comm := fun ⟨_, h₁⟩ ⟨_, h₂⟩ ↦
       have := closure_le_centralizer_centralizer s
       Subtype.ext <| Set.centralizer_centralizer_comm_of_comm hcomm _ (this h₁) _ (this h₂) }
 
-theorem exists_list_of_mem_closure {s : Set R} {x : R} (hx : x ∈ closure s) :
+theorem exists_list_of_mem_closure {R} [Ring R] {s : Set R} {x : R} (hx : x ∈ closure s) :
     ∃ L : List (List R), (∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = (-1 : R)) ∧ (L.map List.prod).sum = x := by
   rw [mem_closure_iff] at hx
   induction hx using AddSubgroup.closure_induction with
@@ -962,7 +962,8 @@ namespace Subring
 variable {s : Set R}
 
 @[elab_as_elim]
-protected theorem InClosure.recOn {C : R → Prop} {x : R} (hx : x ∈ closure s) (h1 : C 1)
+protected theorem InClosure.recOn {R} [Ring R] {s : Set R}
+    {C : R → Prop} {x : R} (hx : x ∈ closure s) (h1 : C 1)
     (hneg1 : C (-1)) (hs : ∀ z ∈ s, ∀ n, C n → C (z * n)) (ha : ∀ {x y}, C x → C y → C (x + y)) :
     C x := by
   have h0 : C 0 := add_neg_cancel (1 : R) ▸ ha h1 hneg1
@@ -1055,48 +1056,48 @@ instance [SMul R α] [FaithfulSMul R α] (S : Subring R) : FaithfulSMul S α :=
   (inferInstance : FaithfulSMul S.toSubsemiring α)
 
 /-- The action by a subring is the action by the underlying ring. -/
-instance [MulAction R α] (S : Subring R) : MulAction S α :=
+instance {R} [Ring R] [MulAction R α] (S : Subring R) : MulAction S α :=
   (inferInstance : MulAction S.toSubsemiring α)
 
 /-- The action by a subring is the action by the underlying ring. -/
-instance [AddMonoid α] [DistribMulAction R α] (S : Subring R) : DistribMulAction S α :=
-  (inferInstance : DistribMulAction S.toSubsemiring α)
+instance {R} [Ring R] [AddMonoid α] [DistribMulAction R α] (S : Subring R) :
+    DistribMulAction S α := (inferInstance : DistribMulAction S.toSubsemiring α)
 
 /-- The action by a subring is the action by the underlying ring. -/
-instance [Monoid α] [MulDistribMulAction R α] (S : Subring R) : MulDistribMulAction S α :=
-  (inferInstance : MulDistribMulAction S.toSubsemiring α)
+instance {R} [Ring R] [Monoid α] [MulDistribMulAction R α] (S : Subring R) :
+    MulDistribMulAction S α := (inferInstance : MulDistribMulAction S.toSubsemiring α)
 
 /-- The action by a subring is the action by the underlying ring. -/
 instance [Zero α] [SMulWithZero R α] (S : Subring R) : SMulWithZero S α :=
   (inferInstance : SMulWithZero S.toSubsemiring α)
 
 /-- The action by a subring is the action by the underlying ring. -/
-instance [Zero α] [MulActionWithZero R α] (S : Subring R) : MulActionWithZero S α :=
+instance {R} [Ring R] [Zero α] [MulActionWithZero R α] (S : Subring R) : MulActionWithZero S α :=
   (inferInstance : MulActionWithZero S.toSubsemiring α)
 
 /-- The action by a subring is the action by the underlying ring. -/
-instance [AddCommMonoid α] [Module R α] (S : Subring R) : Module S α :=
+instance {R} [Ring R] [AddCommMonoid α] [Module R α] (S : Subring R) : Module S α :=
   (inferInstance : Module S.toSubsemiring α)
 
 /-- The action by a subsemiring is the action by the underlying ring. -/
-instance [Semiring α] [MulSemiringAction R α] (S : Subring R) : MulSemiringAction S α :=
-  (inferInstance : MulSemiringAction S.toSubmonoid α)
+instance {R} [Ring R] [Semiring α] [MulSemiringAction R α] (S : Subring R) :
+    MulSemiringAction S α := (inferInstance : MulSemiringAction S.toSubmonoid α)
 
 /-- The center of a semiring acts commutatively on that semiring. -/
-instance center.smulCommClass_left : SMulCommClass (center R) R R :=
+instance center.smulCommClass_left {R} [Ring R] : SMulCommClass (center R) R R :=
   Subsemiring.center.smulCommClass_left
 
 /-- The center of a semiring acts commutatively on that semiring. -/
-instance center.smulCommClass_right : SMulCommClass R (center R) R :=
+instance center.smulCommClass_right {R} [Ring R] : SMulCommClass R (center R) R :=
   Subsemiring.center.smulCommClass_right
 
 /-- The center of a semiring acts commutatively on any `R`-module -/
-instance {M : Type*} [MulAction R M] :
+instance {R M : Type*} [Ring R] [MulAction R M] :
     SMulCommClass R (Subring.center R) M :=
   (inferInstance : SMulCommClass R (Submonoid.center R) M)
 
 /-- The center of a semiring acts commutatively on any `R`-module -/
-instance {M : Type*} [MulAction R M] :
+instance {R M : Type*} [Ring R] [MulAction R M] :
     SMulCommClass (Subring.center R) R M :=
   (inferInstance : SMulCommClass (Submonoid.center R) R M)