English
The map liftEquiv M i p provides a one-to-one correspondence between ring homomorphisms K →* M and L →* M.
Русский
Картирование liftEquiv обеспечивает взаимно однозначное соответствие между гомоморфизмами K →* M и L →* M.
LaTeX
$$liftEquiv M i p : (K →+* M) ≃ (L →+* M)$$
Lean4
/-- If `i : K →+* L` is a homomorphisms of characteristic `p` rings, such that
`i` is `p`-radical, and `M` is a perfect ring of characteristic `p`,
then `K →+* M` is one-to-one correspondence to
`L →+* M`, given by `PerfectRing.lift`. This is a generalization to `PerfectClosure.lift`. -/
def liftEquiv : (K →+* M) ≃ (L →+* M) where
toFun j := lift i j p
invFun f := f.comp i
left_inv f := lift_comp i f p
right_inv f := comp_lift i f p
