English
There is a canonical algebra hom kerLiftAlg f from A/(ker f) to B given by ā ↦ f(a); this is the induced algebra morphism from the quotient by the kernel to the codomain.
Русский
Существует канонический алгебра-гомоморфизм kerLiftAlg f: A/(ker f) → B, действующий как ā ↦ f(a); это индуцированный алгебра-гомоморфизм из частного по ядру куда-то в кодомен.
LaTeX
$$$\operatorname{kerLiftAlg} f : A \!\! / \ker f \;\to_A\; B$ с $(a + \ker f) \mapsto f(a)$$$
Lean4
/-- The induced algebras morphism from the quotient by the kernel to the codomain.
This is an isomorphism if `f` has a right inverse (`quotientKerAlgEquivOfRightInverse`) /
is surjective (`quotientKerAlgEquivOfSurjective`).
-/
def kerLiftAlg (f : A →ₐ[R₁] B) : A ⧸ (RingHom.ker f) →ₐ[R₁] B :=
AlgHom.mk' (RingHom.kerLift (f : A →+* B)) fun _ _ => KerLift.map_smul f _ _
