English
There is a canonical equivalence lifting ring homomorphisms R →+* S to R →+* Perfection S p given a perfection map and π: P →+* S.
Русский
Существуют канонические эквивилиденты для подъёма гомоморфизмов кольца из R в S до R →+* Perfection S p через маппинг PerfectionMap p π.
LaTeX
$$PerfectionMap p π lifts to an equivalence $\\mathrm{RingHom}(R,S) \\simeq \\mathrm{RingHom}(R, \\mathrm{Ring.Perfection}(S,p))$$$
Lean4
/-- Given rings `R` and `S` of characteristic `p`, with `R` being perfect,
any homomorphism `R →+* S` can be lifted to a homomorphism `R →+* P`,
where `P` is any perfection of `S`. -/
@[simps]
noncomputable def lift [PerfectRing R p] (S : Type u₂) [CommSemiring S] [CharP S p] (P : Type u₃) [CommSemiring P]
[CharP P p] [PerfectRing P p] (π : P →+* S) (m : PerfectionMap p π) : (R →+* S) ≃ (R →+* P)
where
toFun f := RingHom.comp ↑m.equiv.symm <| Perfection.lift p R S f
invFun f := π.comp f
left_inv
f := by
simp_rw [← RingHom.comp_assoc, comp_symm_equiv']
exact (Perfection.lift p R S).symm_apply_apply f
right_inv
f := by
exact
RingHom.ext fun x =>
m.equiv.injective <|
(m.equiv.apply_symm_apply _).trans <|
show Perfection.lift p R S (π.comp f) x = RingHom.comp (↑m.equiv) f x from
RingHom.ext_iff.1 (by rw [Equiv.apply_eq_iff_eq_symm_apply]; rfl) _
