English
Let s be a relation on A that defines a congruence; RingQuot s is the quotient of A by this relation. For any S‑algebra B and any S‑algebra homomorphism f: RingQuot s → B, f is the unique S‑algebra homomorphism that extends the canonical map, i.e. f = liftAlgHom S ⟨ f ∘ mkAlgHom S s, proof ⟩.
Русский
Пусть s задаёт конгруэнцию на A; RingQuot s — фактор кольца A по этой конгруэнции. Для любого S‑алгебра B и любого S‑алгебра-гомоморфизма f: RingQuot s → B существует единственный такой гомоморфизм, расширяющий каноническое отображение, то есть f = liftAlgHom S ⟨ f ∘ mkAlgHom S s, доказательство ⟩.
LaTeX
$$$ f = \mathrm{liftAlgHom}_S \langle f \circ (\mathrm{mkAlgHom} S s), \; \lambda h, \; \mathrm{congrArg}(f)(\mathrm{mkAlgHom_rel} S h) \rangle $$$
Lean4
theorem eq_liftAlgHom_comp_mkAlgHom {s : A → A → Prop} (f : RingQuot s →ₐ[S] B) :
f = liftAlgHom S ⟨f.comp (mkAlgHom S s), fun _ _ h ↦ congr_arg f (mkAlgHom_rel S h)⟩ :=
liftAlgHom_unique S (f.comp (mkAlgHom S s)) (fun _ _ h ↦ congr_arg (⇑f) (mkAlgHom_rel S h)) f rfl
