English
The quotient map from an S-algebra to its quotient, as an S-algebra homomorphism, exists and is denoted mkAlgHom.
Русский
Существуют и задаются как AlgHom отображение-квота из S-алгебры в её фактор-алгебру, обозначаемое mkAlgHom.
LaTeX
$$$\\text{mkAlgHom} : S\\text{-Alg}(A) \\to\\!\\text{AlgHom} S A (RingQuot s)$$$
Lean4
/-- The universal ring homomorphism from `B ⧸ Ideal.ofRel r` to `RingQuot r`. -/
def idealQuotientToRingQuot (r : B → B → Prop) : B ⧸ Ideal.ofRel r →+* RingQuot r :=
Ideal.Quotient.lift (Ideal.ofRel r) (mkRingHom r)
(by
refine fun x h ↦ Submodule.span_induction ?_ ?_ ?_ ?_ h
· rintro y ⟨a, b, h, su⟩
symm at su
rw [← sub_eq_iff_eq_add] at su
rw [← su, RingHom.map_sub, mkRingHom_rel h, sub_self]
· simp
· intro a b _ _ ha hb
simp [ha, hb]
· intro a x _ hx
simp [hx])
