English
Let A be a semiring with an S-algebra structure, and c a RingCon on A. Then the quotient c.Quotient carries a natural algebra structure over S, induced by the quotient map and the given S-action on A; in particular the quotient map A → c.Quotient is S-linear.
Русский
Пусть A — полукольцо с заданной структурой алгебры над S, и c — RingCon на A. Тогда фактор-объект c.Quotient естественно наследует структуру алгебры над S, индукцию которой задают каноническое отображение A → c.Quotient и исходная S-структура на A; при этом фактор-отображение A → c.Quotient сохраняет линейность по S.
LaTeX
$$$\\exists \\mathcal{A}: \\mathrm{Algebra}(S, c^{\\mathrm{Quot}}) \\text{ such that } \\operatorname{algebraMap}_{S}^{c^{\\mathrm{Quot}}} = c.mk' \\circ \\operatorname{algebraMap}_{S}^{A}.$$$
Lean4
instance (c : RingCon A) : Algebra S c.Quotient where
smul := (· • ·)
algebraMap := c.mk'.comp (algebraMap S A)
commutes' _ := Quotient.ind' fun _ ↦ congr_arg Quotient.mk'' <| Algebra.commutes _ _
smul_def' _ := Quotient.ind' fun _ ↦ congr_arg Quotient.mk'' <| Algebra.smul_def _ _
