English
Given a ring hom f: R → S that vanishes on I, there exists a lift to a ring hom from R/I to S extending f.
Русский
Если данный кольцевой гомоморфизм f: R → S уничтожает I, существует поднятие (lifting) на кольцо R/I в S, сохраняющее структуру гомоморфизма.
LaTeX
$$$\\exists \\hat f: R/I \\to S\\text{ such that }\\hat f \\circ \\pi_I = f \\text{ and } f(a)=0 \\ \\forall a\\in I$$$
Lean4
/-- Given a ring homomorphism `f : R →+* S` sending all elements of an ideal to zero,
lift it to the quotient by this ideal. -/
def lift (f : R →+* S) (H : ∀ a : R, a ∈ I → f a = 0) : R ⧸ I →+* S :=
{
QuotientAddGroup.lift I.toAddSubgroup f.toAddMonoidHom
H with
map_one' := f.map_one
map_mul' := fun a₁ a₂ => Quotient.inductionOn₂' a₁ a₂ f.map_mul }
