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.

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, 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.

instance RingCon.instAlgebraQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToMulInstSemiringQuotientToAddToDistribToNonUnitalNonAssocSemiringToNonAssocSemiringToMul {S : Type uS} [CommSemiring S] {A : Type uA} [Semiring A] [Algebra S A] (c : RingCon A) : Algebra S (RingCon.Quotient c)

@[simp]

theorem RingCon.coe_algebraMap {S : Type uS} [CommSemiring S] {A : Type uA} [Semiring A] [Algebra S A] (c : RingCon A) (s : S) : ↑(↑(algebraMap S A) s) = ↑(algebraMap S (RingCon.Quotient c)) s

inductive RingQuot.Rel {R : Type uR} [Semiring R] (r : R → R → Prop) : R → R → Prop

• of: ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃x y : R⦄, r x y → RingQuot.Rel r x y
• add_left: ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃a b c : R⦄, RingQuot.Rel r a b → RingQuot.Rel r (a + c) (b + c)
• mul_left: ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃a b c : R⦄, RingQuot.Rel r a b → RingQuot.Rel r (a * c) (b * c)
• mul_right: ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} ⦃a b c : R⦄, RingQuot.Rel r b c → RingQuot.Rel r (a * b) (a * c)

Given an arbitrary relation r on a ring, we strengthen it to a relation Rel r, such that the equivalence relation generated by Rel r has x ~ y if and only if x - y is in the ideal generated by elements a - b such that r a b.

theorem RingQuot.Rel.add_right {R : Type uR} [Semiring R] {r : R → R → Prop} ⦃a : R⦄ ⦃b : R⦄ ⦃c : R⦄ (h : RingQuot.Rel r b c) : RingQuot.Rel r (a + b) (a + c)

theorem RingQuot.Rel.neg {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a : R⦄ ⦃b : R⦄ (h : RingQuot.Rel r a b) : RingQuot.Rel r (-a) (-b)

theorem RingQuot.Rel.sub_left {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a : R⦄ ⦃b : R⦄ ⦃c : R⦄ (h : RingQuot.Rel r a b) : RingQuot.Rel r (a - c) (b - c)

theorem RingQuot.Rel.sub_right {R : Type uR} [Ring R] {r : R → R → Prop} ⦃a : R⦄ ⦃b : R⦄ ⦃c : R⦄ (h : RingQuot.Rel r b c) : RingQuot.Rel r (a - b) (a - c)

theorem RingQuot.Rel.smul {S : Type uS} [CommSemiring S] {A : Type uA} [Semiring A] [Algebra S A] {r : A → A → Prop} (k : S) ⦃a : A⦄ ⦃b : A⦄ (h : RingQuot.Rel r a b) : RingQuot.Rel r (k • a) (k • b)

def RingQuot.ringCon {R : Type uR} [Semiring R] (r : R → R → Prop) : RingCon R

EqvGen (RingQuot.Rel r) is a ring congruence.

theorem RingQuot.eqvGen_rel_eq {R : Type uR} [Semiring R] (r : R → R → Prop) : EqvGen (RingQuot.Rel r) = RingConGen.Rel r

structure RingQuot {R : Type uR} [Semiring R] (r : R → R → Prop) : Type uR

• toQuot : Quot (RingQuot.Rel r)

The quotient of a ring by an arbitrary relation.

instance RingQuot.instNatCastRingQuot {R : Type uR} [Semiring R] (r : R → R → Prop) : NatCast (RingQuot r)

instance RingQuot.instZeroRingQuot {R : Type uR} [Semiring R] (r : R → R → Prop) : Zero (RingQuot r)

instance RingQuot.instOneRingQuot {R : Type uR} [Semiring R] (r : R → R → Prop) : One (RingQuot r)

instance RingQuot.instAddRingQuot {R : Type uR} [Semiring R] (r : R → R → Prop) : Add (RingQuot r)

instance RingQuot.instMulRingQuot {R : Type uR} [Semiring R] (r : R → R → Prop) : Mul (RingQuot r)

instance RingQuot.instPowRingQuotNat {R : Type uR} [Semiring R] (r : R → R → Prop) : Pow (RingQuot r) ℕ

instance RingQuot.instNegRingQuotToSemiring {R : Type uR} [Ring R] (r : R → R → Prop) : Neg (RingQuot r)

instance RingQuot.instSubRingQuotToSemiring {R : Type uR} [Ring R] (r : R → R → Prop) : Sub (RingQuot r)

instance RingQuot.instSMulRingQuot {R : Type uR} [Semiring R] {S : Type uS} [CommSemiring S] (r : R → R → Prop) [Algebra S R] : SMul S (RingQuot r)

theorem RingQuot.zero_quot {R : Type uR} [Semiring R] (r : R → R → Prop) : { toQuot := Quot.mk (RingQuot.Rel r) 0 } = 0

theorem RingQuot.one_quot {R : Type uR} [Semiring R] (r : R → R → Prop) : { toQuot := Quot.mk (RingQuot.Rel r) 1 } = 1

theorem RingQuot.add_quot {R : Type uR} [Semiring R] (r : R → R → Prop) {a : R} {b : R} : { toQuot := Quot.mk (RingQuot.Rel r) a } + { toQuot := Quot.mk (RingQuot.Rel r) b } = { toQuot := Quot.mk (RingQuot.Rel r) (a + b) }

theorem RingQuot.mul_quot {R : Type uR} [Semiring R] (r : R → R → Prop) {a : R} {b : R} : { toQuot := Quot.mk (RingQuot.Rel r) a } * { toQuot := Quot.mk (RingQuot.Rel r) b } = { toQuot := Quot.mk (RingQuot.Rel r) (a * b) }

theorem RingQuot.pow_quot {R : Type uR} [Semiring R] (r : R → R → Prop) {a : R} {n : ℕ} : { toQuot := Quot.mk (RingQuot.Rel r) a } ^ n = { toQuot := Quot.mk (RingQuot.Rel r) (a ^ n) }

theorem RingQuot.neg_quot {R : Type uR} [Ring R] (r : R → R → Prop) {a : R} : -{ toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (-a) }

theorem RingQuot.sub_quot {R : Type uR} [Ring R] (r : R → R → Prop) {a : R} {b : R} : { toQuot := Quot.mk (RingQuot.Rel r) a } - { toQuot := Quot.mk (RingQuot.Rel r) b } = { toQuot := Quot.mk (RingQuot.Rel r) (a - b) }

theorem RingQuot.smul_quot {R : Type uR} [Semiring R] {S : Type uS} [CommSemiring S] (r : R → R → Prop) [Algebra S R] {n : S} {a : R} : n • { toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (n • a) }

instance RingQuot.instIsScalarTower {R : Type uR} [Semiring R] {S : Type uS} [CommSemiring S] {T : Type uT} (r : R → R → Prop) [CommSemiring T] [SMul S T] [Algebra S R] [Algebra T R] [IsScalarTower S T R] : IsScalarTower S T (RingQuot r)

instance RingQuot.instSMulCommClass {R : Type uR} [Semiring R] {S : Type uS} [CommSemiring S] {T : Type uT} (r : R → R → Prop) [CommSemiring T] [Algebra S R] [Algebra T R] [SMulCommClass S T R] : SMulCommClass S T (RingQuot r)

instance RingQuot.instAddCommMonoid {R : Type uR} [Semiring R] (r : R → R → Prop) : AddCommMonoid (RingQuot r)

instance RingQuot.instMonoidWithZero {R : Type uR} [Semiring R] (r : R → R → Prop) : MonoidWithZero (RingQuot r)

instance RingQuot.instSemiring {R : Type uR} [Semiring R] (r : R → R → Prop) : Semiring (RingQuot r)

instance RingQuot.instRing {R : Type uR} [Ring R] (r : R → R → Prop) : Ring (RingQuot r)

instance RingQuot.instCommSemiring {R : Type uR} [CommSemiring R] (r : R → R → Prop) : CommSemiring (RingQuot r)

instance RingQuot.instCommRingRingQuotToSemiringToCommSemiring {R : Type uR} [CommRing R] (r : R → R → Prop) : CommRing (RingQuot r)

instance RingQuot.instInhabited {R : Type uR} [Semiring R] (r : R → R → Prop) : Inhabited (RingQuot r)

instance RingQuot.instAlgebra {R : Type uR} [Semiring R] {S : Type uS} [CommSemiring S] [Algebra S R] (r : R → R → Prop) : Algebra S (RingQuot r)

@[irreducible]

def RingQuot.mkRingHom {R : Type u_1} [Semiring R] (r : R → R → Prop) : R →+* RingQuot r

The quotient map from a ring to its quotient, as a homomorphism of rings.

theorem RingQuot.mkRingHom_def {R : Type u_1} [Semiring R] (r : R → R → Prop) : RingQuot.mkRingHom r = { toMonoidHom := { toOneHom := { toFun := fun x => { toQuot := Quot.mk (RingQuot.Rel r) x }, map_one' := (_ : { toQuot := Quot.mk (RingQuot.Rel r) 1 } = 1) }, map_mul' := (_ : ∀ (a a_1 : R), { toQuot := Quot.mk (RingQuot.Rel r) (a * a_1) } = { toQuot := Quot.mk (RingQuot.Rel r) a } * { toQuot := Quot.mk (RingQuot.Rel r) a_1 }) }, map_zero' := (_ : { toQuot := Quot.mk (RingQuot.Rel r) 0 } = 0), map_add' := (_ : ∀ (a a_1 : R), { toQuot := Quot.mk (RingQuot.Rel r) (a + a_1) } = { toQuot := Quot.mk (RingQuot.Rel r) a } + { toQuot := Quot.mk (RingQuot.Rel r) a_1 }) }

theorem RingQuot.mkRingHom_rel {R : Type uR} [Semiring R] {r : R → R → Prop} {x : R} {y : R} (w : r x y) : ↑(RingQuot.mkRingHom r) x = ↑(RingQuot.mkRingHom r) y

theorem RingQuot.mkRingHom_surjective {R : Type uR} [Semiring R] (r : R → R → Prop) : Function.Surjective ↑(RingQuot.mkRingHom r)

theorem RingQuot.ringQuot_ext {R : Type uR} [Semiring R] {T : Type uT} [Semiring T] {r : R → R → Prop} (f : RingQuot r →+* T) (g : RingQuot r →+* T) (w : RingHom.comp f (RingQuot.mkRingHom r) = RingHom.comp g (RingQuot.mkRingHom r)) : f = g

theorem RingQuot.preLift_def {R : Type u_1} [Semiring R] {T : Type u_2} [Semiring T] {r : R → R → Prop} {f : R →+* T} (h : ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y) : RingQuot.preLift h = { toMonoidHom := { toOneHom := { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) }, map_mul' := (_ : ∀ (x y : RingQuot r), OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) } (x * y) = OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) } x * OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) } y) }, map_zero' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 0.toQuot = 0), map_add' := (_ : ∀ (x y : RingQuot r), OneHom.toFun (↑{ toOneHom := { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) }, map_mul' := (_ : ∀ (x y : RingQuot r), OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) } (x * y) = OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) } x * OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) } y) }) (x + y) = OneHom.toFun (↑{ toOneHom := { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) }, map_mul' := (_ : ∀ (x y : RingQuot r), OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) } (x * y) = OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) } x * OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) } y) }) x + OneHom.toFun (↑{ toOneHom := { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) }, map_mul' := (_ : ∀ (x y : RingQuot r), OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) } (x * y) = OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) } x * OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : R), RingQuot.Rel r a b → ↑f a = ↑f b) 1.toQuot = 1) } y) }) y) }

@[irreducible]

def RingQuot.preLift {R : Type u_1} [Semiring R] {T : Type u_2} [Semiring T] {r : R → R → Prop} {f : R →+* T} (h : ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y) : RingQuot r →+* T

theorem RingQuot.lift_def {R : Type u_1} [Semiring R] {T : Type u_2} [Semiring T] {r : R → R → Prop} : RingQuot.lift = { toFun := fun f => RingQuot.preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y), invFun := fun F => { val := RingHom.comp F (RingQuot.mkRingHom r), property := (_ : ∀ (x y : R), r x y → ↑F (↑(RingQuot.mkRingHom r) x) = ↑F (↑(RingQuot.mkRingHom r) y)) }, left_inv := (_ : ∀ (f : { f // ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y }), (fun F => { val := RingHom.comp F (RingQuot.mkRingHom r), property := (_ : ∀ (x y : R), r x y → ↑F (↑(RingQuot.mkRingHom r) x) = ↑F (↑(RingQuot.mkRingHom r) y)) }) ((fun f => RingQuot.preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y)) f) = f), right_inv := (_ : ∀ (F : RingQuot r →+* T), (fun f => RingQuot.preLift (_ : ∀ ⦃x y : R⦄, r x y → ↑↑f x = ↑↑f y)) ((fun F => { val := RingHom.comp F (RingQuot.mkRingHom r), property := (_ : ∀ (x y : R), r x y → ↑F (↑(RingQuot.mkRingHom r) x) = ↑F (↑(RingQuot.mkRingHom r) y)) }) F) = F) }

@[irreducible]

def RingQuot.lift {R : Type u_1} [Semiring R] {T : Type u_2} [Semiring T] {r : R → R → Prop} : { f // ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y } ≃ (RingQuot r →+* T)

Any ring homomorphism f : R →+* T which respects a relation r : R → R → Prop factors uniquely through a morphism RingQuot r →+* T.

@[simp]

theorem RingQuot.lift_mkRingHom_apply {R : Type uR} [Semiring R] {T : Type uT} [Semiring T] (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y) (x : R) : ↑(↑RingQuot.lift { val := f, property := w }) (↑(RingQuot.mkRingHom r) x) = ↑f x

theorem RingQuot.lift_unique {R : Type uR} [Semiring R] {T : Type uT} [Semiring T] (f : R →+* T) {r : R → R → Prop} (w : ∀ ⦃x y : R⦄, r x y → ↑f x = ↑f y) (g : RingQuot r →+* T) (h : RingHom.comp g (RingQuot.mkRingHom r) = f) : g = ↑RingQuot.lift { val := f, property := w }

theorem RingQuot.eq_lift_comp_mkRingHom {R : Type uR} [Semiring R] {T : Type uT} [Semiring T] {r : R → R → Prop} (f : RingQuot r →+* T) : f = ↑RingQuot.lift { val := RingHom.comp f (RingQuot.mkRingHom r), property := (_ : ∀ (x y : R), r x y → ↑f (↑(RingQuot.mkRingHom r) x) = ↑f (↑(RingQuot.mkRingHom r) y)) }

We now verify that in the case of a commutative ring, the RingQuot construction agrees with the quotient by the appropriate ideal.

def RingQuot.ringQuotToIdealQuotient {B : Type uR} [CommRing B] (r : B → B → Prop) : RingQuot r →+* B ⧸ Ideal.ofRel r

The universal ring homomorphism from RingQuot r to B ⧸ Ideal.ofRel r.

@[simp]

theorem RingQuot.ringQuotToIdealQuotient_apply {B : Type uR} [CommRing B] (r : B → B → Prop) (x : B) : ↑(RingQuot.ringQuotToIdealQuotient r) (↑(RingQuot.mkRingHom r) x) = ↑(Ideal.Quotient.mk (Ideal.ofRel r)) x

def RingQuot.idealQuotientToRingQuot {B : Type uR} [CommRing B] (r : B → B → Prop) : B ⧸ Ideal.ofRel r →+* RingQuot r

The universal ring homomorphism from B ⧸ Ideal.ofRel r to RingQuot r.

@[simp]

theorem RingQuot.idealQuotientToRingQuot_apply {B : Type uR} [CommRing B] (r : B → B → Prop) (x : B) : ↑(RingQuot.idealQuotientToRingQuot r) (↑(Ideal.Quotient.mk (Ideal.ofRel r)) x) = ↑(RingQuot.mkRingHom r) x

def RingQuot.ringQuotEquivIdealQuotient {B : Type uR} [CommRing B] (r : B → B → Prop) : RingQuot r ≃+* B ⧸ Ideal.ofRel r

The ring equivalence between RingQuot r and (Ideal.ofRel r).quotient

theorem RingQuot.Rel.star {R : Type uR} [Semiring R] (r : R → R → Prop) [StarRing R] (hr : (a b : R) → r a b → r (star a) (star b)) ⦃a : R⦄ ⦃b : R⦄ (h : RingQuot.Rel r a b) : RingQuot.Rel r (star a) (star b)

theorem RingQuot.star'_quot {R : Type uR} [Semiring R] (r : R → R → Prop) [StarRing R] (hr : (a b : R) → r a b → r (star a) (star b)) {a : R} : RingQuot.star' r hr { toQuot := Quot.mk (RingQuot.Rel r) a } = { toQuot := Quot.mk (RingQuot.Rel r) (star a) }

def RingQuot.starRing {R : Type uR} [Semiring R] [StarRing R] (r : R → R → Prop) (hr : (a b : R) → r a b → r (star a) (star b)) : StarRing (RingQuot r)

Transfer a star_ring instance through a quotient, if the quotient is invariant to star

@[irreducible]

def RingQuot.mkAlgHom (S : Type u_1) [CommSemiring S] {A : Type u_2} [Semiring A] [Algebra S A] (s : A → A → Prop) : A →ₐ[S] RingQuot s

The quotient map from an S-algebra to its quotient, as a homomorphism of S-algebras.

theorem RingQuot.mkAlgHom_def (S : Type u_1) [CommSemiring S] {A : Type u_2} [Semiring A] [Algebra S A] (s : A → A → Prop) : RingQuot.mkAlgHom S s = let src := RingQuot.mkRingHom s; { toRingHom := { toMonoidHom := ↑src, map_zero' := (_ : OneHom.toFun (↑↑(RingQuot.mkRingHom s)) 0 = 0), map_add' := (_ : ∀ (x y : A), OneHom.toFun (↑↑(RingQuot.mkRingHom s)) (x + y) = OneHom.toFun (↑↑(RingQuot.mkRingHom s)) x + OneHom.toFun (↑↑(RingQuot.mkRingHom s)) y) }, commutes' := (_ : ∀ (x : S), OneHom.toFun (↑↑{ toMonoidHom := ↑(RingQuot.mkRingHom s), map_zero' := (_ : OneHom.toFun (↑↑(RingQuot.mkRingHom s)) 0 = 0), map_add' := (_ : ∀ (x y : A), OneHom.toFun (↑↑(RingQuot.mkRingHom s)) (x + y) = OneHom.toFun (↑↑(RingQuot.mkRingHom s)) x + OneHom.toFun (↑↑(RingQuot.mkRingHom s)) y) }) (↑(algebraMap S A) x) = ↑(algebraMap S (RingQuot s)) x) }

@[simp]

theorem RingQuot.mkAlgHom_coe (S : Type uS) [CommSemiring S] {A : Type uA} [Semiring A] [Algebra S A] (s : A → A → Prop) : ↑(RingQuot.mkAlgHom S s) = RingQuot.mkRingHom s

theorem RingQuot.mkAlgHom_rel (S : Type uS) [CommSemiring S] {A : Type uA} [Semiring A] [Algebra S A] {s : A → A → Prop} {x : A} {y : A} (w : s x y) : ↑(RingQuot.mkAlgHom S s) x = ↑(RingQuot.mkAlgHom S s) y

theorem RingQuot.mkAlgHom_surjective (S : Type uS) [CommSemiring S] {A : Type uA} [Semiring A] [Algebra S A] (s : A → A → Prop) : Function.Surjective ↑(RingQuot.mkAlgHom S s)

theorem RingQuot.ringQuot_ext' (S : Type uS) [CommSemiring S] {A : Type uA} [Semiring A] [Algebra S A] {B : Type u₄} [Semiring B] [Algebra S B] {s : A → A → Prop} (f : RingQuot s →ₐ[S] B) (g : RingQuot s →ₐ[S] B) (w : AlgHom.comp f (RingQuot.mkAlgHom S s) = AlgHom.comp g (RingQuot.mkAlgHom S s)) : f = g

theorem RingQuot.preLiftAlgHom_def (S : Type u_1) [CommSemiring S] {A : Type u_2} [Semiring A] [Algebra S A] {B : Type u_3} [Semiring B] [Algebra S B] {s : A → A → Prop} {f : A →ₐ[S] B} (h : ∀ ⦃x y : A⦄, s x y → ↑f x = ↑f y) : RingQuot.preLiftAlgHom S h = { toRingHom := { toMonoidHom := { toOneHom := { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) }, map_mul' := (_ : ∀ (x y : RingQuot s), OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) } (x * y) = OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) } x * OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) } y) }, map_zero' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 0.toQuot = 0), map_add' := (_ : ∀ (x y : RingQuot s), OneHom.toFun (↑{ toOneHom := { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) }, map_mul' := (_ : ∀ (x y : RingQuot s), OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) } (x * y) = OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) } x * OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) } y) }) (x + y) = OneHom.toFun (↑{ toOneHom := { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) }, map_mul' := (_ : ∀ (x y : RingQuot s), OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) } (x * y) = OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) } x * OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) } y) }) x + OneHom.toFun (↑{ toOneHom := { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) }, map_mul' := (_ : ∀ (x y : RingQuot s), OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) } (x * y) = OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) } x * OneHom.toFun { toFun := fun x => Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) x.toQuot, map_one' := (_ : Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) 1.toQuot = 1) } y) }) y) }, commutes' := (_ : ∀ (x : S), Quot.lift ↑f (_ : ∀ (a b : A), RingQuot.Rel s a b → ↑f a = ↑f b) (↑(algebraMap S (RingQuot s)) x).toQuot = ↑(algebraMap S B) x) }

@[irreducible]

def RingQuot.preLiftAlgHom (S : Type u_1) [CommSemiring S] {A : Type u_2} [Semiring A] [Algebra S A] {B : Type u_3} [Semiring B] [Algebra S B] {s : A → A → Prop} {f : A →ₐ[S] B} (h : ∀ ⦃x y : A⦄, s x y → ↑f x = ↑f y) : RingQuot s →ₐ[S] B

@[irreducible]

def RingQuot.liftAlgHom (S : Type u_1) [CommSemiring S] {A : Type u_2} [Semiring A] [Algebra S A] {B : Type u_3} [Semiring B] [Algebra S B] {s : A → A → Prop} : { f // ∀ ⦃x y : A⦄, s x y → ↑f x = ↑f y } ≃ (RingQuot s →ₐ[S] B)

Any S-algebra homomorphism f : A →ₐ[S] B which respects a relation s : A → A → Prop factors uniquely through a morphism RingQuot s →ₐ[S] B.

theorem RingQuot.liftAlgHom_def (S : Type u_1) [CommSemiring S] {A : Type u_2} [Semiring A] [Algebra S A] {B : Type u_3} [Semiring B] [Algebra S B] {s : A → A → Prop} : RingQuot.liftAlgHom S = { toFun := fun f' => RingQuot.preLiftAlgHom S (_ : ∀ ⦃x y : A⦄, s x y → ↑↑f' x = ↑↑f' y), invFun := fun F => { val := AlgHom.comp F (RingQuot.mkAlgHom S s), property := (_ : ∀ (x x_1 : A), s x x_1 → ↑F (↑↑(RingQuot.mkAlgHom S s) x) = ↑F (↑↑(RingQuot.mkAlgHom S s) x_1)) }, left_inv := (_ : ∀ (f : { f // ∀ ⦃x y : A⦄, s x y → ↑f x = ↑f y }), (fun F => { val := AlgHom.comp F (RingQuot.mkAlgHom S s), property := (_ : ∀ (x x_1 : A), s x x_1 → ↑F (↑↑(RingQuot.mkAlgHom S s) x) = ↑F (↑↑(RingQuot.mkAlgHom S s) x_1)) }) ((fun f' => RingQuot.preLiftAlgHom S (_ : ∀ ⦃x y : A⦄, s x y → ↑↑f' x = ↑↑f' y)) f) = f), right_inv := (_ : ∀ (F : RingQuot s →ₐ[S] B), (fun f' => RingQuot.preLiftAlgHom S (_ : ∀ ⦃x y : A⦄, s x y → ↑↑f' x = ↑↑f' y)) ((fun F => { val := AlgHom.comp F (RingQuot.mkAlgHom S s), property := (_ : ∀ (x x_1 : A), s x x_1 → ↑F (↑↑(RingQuot.mkAlgHom S s) x) = ↑F (↑↑(RingQuot.mkAlgHom S s) x_1)) }) F) = F) }

@[simp]

theorem RingQuot.liftAlgHom_mkAlgHom_apply (S : Type uS) [CommSemiring S] {A : Type uA} [Semiring A] [Algebra S A] {B : Type u₄} [Semiring B] [Algebra S B] (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y : A⦄, s x y → ↑f x = ↑f y) (x : A) : ↑(↑(RingQuot.liftAlgHom S) { val := f, property := w }) (↑(RingQuot.mkAlgHom S s) x) = ↑f x

theorem RingQuot.liftAlgHom_unique (S : Type uS) [CommSemiring S] {A : Type uA} [Semiring A] [Algebra S A] {B : Type u₄} [Semiring B] [Algebra S B] (f : A →ₐ[S] B) {s : A → A → Prop} (w : ∀ ⦃x y : A⦄, s x y → ↑f x = ↑f y) (g : RingQuot s →ₐ[S] B) (h : AlgHom.comp g (RingQuot.mkAlgHom S s) = f) : g = ↑(RingQuot.liftAlgHom S) { val := f, property := w }

theorem RingQuot.eq_liftAlgHom_comp_mkAlgHom (S : Type uS) [CommSemiring S] {A : Type uA} [Semiring A] [Algebra S A] {B : Type u₄} [Semiring B] [Algebra S B] {s : A → A → Prop} (f : RingQuot s →ₐ[S] B) : f = ↑(RingQuot.liftAlgHom S) { val := AlgHom.comp f (RingQuot.mkAlgHom S s), property := (_ : ∀ (x y : A), s x y → ↑f (↑↑(RingQuot.mkAlgHom S s) x) = ↑f (↑↑(RingQuot.mkAlgHom S s) y)) }