English
Let I be a two-sided ideal of a ring A, and suppose A is an R1-algebra. Then the quotient A/I carries a natural R1-algebra structure, where the structure map is given by composing the algebra map A with the quotient map A → A/I.
Русский
Пусть I — двусторонний идеал кольца A, и A является R1-алгеброй. Тогда частное кольцо A/I естественным образом считается R1-алгеброй: структура задаётся композицией отображений R1 → A и A → A/I.
LaTeX
$$$ (A/I) \text{ is an } R_1\text{-algebra with } (algebraMap_{R_1,A/I}) = (Quotient.mk_I) \circ (algebraMap_{R_1,A}) $$$
Lean4
/-- The `R₁`-algebra structure on `A/I` for an `R₁`-algebra `A` -/
instance algebra {I : Ideal A} [I.IsTwoSided] : Algebra R₁ (A ⧸ I)
where
algebraMap := (Ideal.Quotient.mk I).comp (algebraMap R₁ A)
smul_def' := fun _ x =>
Quotient.inductionOn' x fun _ => ((Quotient.mk I).congr_arg <| Algebra.smul_def _ _).trans (RingHom.map_mul _ _ _)
commutes' := by rintro r ⟨x⟩; exact congr_arg (⟦·⟧) (Algebra.commutes r x)
