English
If f: R →+* T is a ring homomorphism that respects the relation r (i.e., r x y implies f x = f y), then there exists a RingQuot r →+* T, called preLift, whose composition with the quotient map mkRingHom r equals f.
Русский
Если f: R →+* T — гомоморфизм колец, сохраняющий отношение r (то есть r x y → f x = f y), то существует отображение RingQuot r →+* T под названием preLift, такое что preLift ∘ mkRingHom r = f.
LaTeX
$$$\\forall f:\\, R \\to\\+* T\\;\\big(\\forall x,y,\\, r\\ x\\ y\\rightarrow f\\,x=f\\,y\\big) \\Rightarrow\\exists!\\, \\text{preLift}\\!\\;\\text{with}\\;\\text{preLift} \\circ mkRingHom r = f$$$
Lean4
def preLift :=
val_proj @wrapped✝.{}
