feat(RingTheory/Ideal/QuotientOperations): remove commutativity insta…

…nces (#9556)

Remove one commutativity instances for the universal property of a quotient algebra :
the target algebra only needs to have `Semiring`.



Co-authored-by: Antoine Chambert-Loir <antoine.chambert-loir@math.univ-paris-diderot.fr>

Mathlib/RingTheory/Ideal/QuotientOperations.lean

@@ -286,9 +286,9 @@ section QuotientAlgebra
 
 variable (R₁ R₂ : Type*) {A B : Type*}
 
-variable [CommSemiring R₁] [CommSemiring R₂] [CommRing A] [CommRing B]
+variable [CommSemiring R₁] [CommSemiring R₂] [CommRing A]
 
-variable [Algebra R₁ A] [Algebra R₂ A] [Algebra R₁ B]
+variable [Algebra R₁ A] [Algebra R₂ A]
 
 /-- The `R₁`-algebra structure on `A/I` for an `R₁`-algebra `A` -/
 instance Quotient.algebra {I : Ideal A} : Algebra R₁ (A ⧸ I) :=
@@ -362,6 +362,10 @@ theorem Quotient.mkₐ_ker (I : Ideal A) : RingHom.ker (Quotient.mkₐ R₁ I :
 
 variable {R₁}
 
+section
+
+variable [Semiring B] [Algebra R₁ B]
+
 /-- `Ideal.quotient.lift` as an `AlgHom`. -/
 def Quotient.liftₐ (I : Ideal A) (f : A →ₐ[R₁] B) (hI : ∀ a : A, a ∈ I → f a = 0) :
     A ⧸ I →ₐ[R₁] B :=
@@ -460,6 +464,8 @@ noncomputable def quotientKerAlgEquivOfSurjective {f : A →ₐ[R₁] B} (hf : F
   quotientKerAlgEquivOfRightInverse (Classical.choose_spec hf.hasRightInverse)
 #align ideal.quotient_ker_alg_equiv_of_surjective Ideal.quotientKerAlgEquivOfSurjective
 
+end
+
 section CommRing_CommRing
 
 variable {S : Type v} [CommRing S]
@@ -564,6 +570,11 @@ theorem comp_quotientMap_eq_of_comp_eq {R' S' : Type*} [CommRing R'] [CommRing S
 
 end CommRing_CommRing
 
+
+section
+
+variable [CommRing B] [Algebra R₁ B]
+
 /-- The algebra hom `A/I →+* B/J` induced by an algebra hom `f : A →ₐ[R₁] B` with `I ≤ f⁻¹(J)`. -/
 def quotientMapₐ {I : Ideal A} (J : Ideal B) (f : A →ₐ[R₁] B) (hIJ : I ≤ J.comap f) :
     A ⧸ I →ₐ[R₁] B ⧸ J :=
@@ -595,6 +606,8 @@ def quotientEquivAlg (I : Ideal A) (J : Ideal B) (f : A ≃ₐ[R₁] B) (hIJ : J
       RingEquiv.coe_toRingHom, AlgEquiv.coe_ringEquiv, AlgEquiv.commutes, Quotient.mk_algebraMap]}
 #align ideal.quotient_equiv_alg Ideal.quotientEquivAlg
 
+end
+
 instance (priority := 100) quotientAlgebra {I : Ideal A} [Algebra R A] :
     Algebra (R ⧸ I.comap (algebraMap R A)) (A ⧸ I) :=
   (quotientMap I (algebraMap R A) (le_of_eq rfl)).toAlgebra