English
Given an algebra map f: A → B over a base ring R, there is a canonical R-algebra structure on the quotient A/(ker f)^2 that lifts f to a map into B.
Русский
Суммаю основание, существует каноническая структура R-алгебры на A/(ker f)^2, которая поднимает отображение f до отображения в B.
LaTeX
$$AlgHom kerSquareLift (f) : A / (ker f)^2 →ₐ[R] B$$
Lean4
/-- The lift of `f : A →ₐ[R] B` to `A ⧸ J ^ 2 →ₐ[R] B` with `J` being the kernel of `f`. -/
def _root_.AlgHom.kerSquareLift (f : A →ₐ[R] B) : A ⧸ RingHom.ker f.toRingHom ^ 2 →ₐ[R] B :=
by
refine { Ideal.Quotient.lift (RingHom.ker f.toRingHom ^ 2) f.toRingHom ?_ with commutes' := ?_ }
· intro a ha; exact Ideal.pow_le_self two_ne_zero ha
· intro r
rw [IsScalarTower.algebraMap_apply R A, RingHom.toFun_eq_coe, Ideal.Quotient.algebraMap_eq, Ideal.Quotient.lift_mk]
exact f.map_algebraMap r
