English
Lifting property: for any ring L of characteristic p that is perfect, ring homomorphisms K → L correspond bijectively to ring homomorphisms PerfectClosure(K,p) → L.
Русский
Свойство подъёма: для любого кольца L характеристикой p, являющегося совершенным, гомоморфизмы K → L и PerfectClosure(K,p) → L взаимно однозначно соответствуют.
LaTeX
$$$\text{lift}_{K,p}: (K \to^+ L) \simeq (\mathrm{PerfectClosure}(K,p) \to^+ L).$$$
Lean4
/-- Given a ring `K` of characteristic `p` and a perfect ring `L` of the same characteristic,
any homomorphism `K →+* L` can be lifted to `PerfectClosure K p`. -/
noncomputable def lift (L : Type v) [CommSemiring L] [CharP L p] [PerfectRing L p] :
(K →+* L) ≃ (PerfectClosure K p →+* L)
where
toFun
f :=
{ toFun := by
refine fun e => liftOn e (fun x => (frobeniusEquiv L p).symm^[x.1] (f x.2)) ?_
rintro - - ⟨n, x⟩
simp [f.map_frobenius]
map_one' := f.map_one
map_zero' := f.map_zero
map_mul' := by
rintro ⟨n, x⟩ ⟨m, y⟩
simp only [quot_mk_eq_mk, liftOn_mk, f.map_iterate_frobenius, mk_mul_mk, map_mul, iterate_map_mul]
have := LeftInverse.iterate (frobeniusEquiv_symm_apply_frobenius L p)
rw [iterate_add_apply, this _ _, add_comm, iterate_add_apply, this _ _]
map_add' := by
rintro ⟨n, x⟩ ⟨m, y⟩
simp only [quot_mk_eq_mk, liftOn_mk, f.map_iterate_frobenius, mk_add_mk, map_add, iterate_map_add]
have := LeftInverse.iterate (frobeniusEquiv_symm_apply_frobenius L p)
rw [iterate_add_apply, this _ _, add_comm n, iterate_add_apply, this _ _] }
invFun f := f.comp (of K p)
right_inv
f := by
ext ⟨n, x⟩
simp only [quot_mk_eq_mk, RingHom.comp_apply, RingHom.coe_mk, MonoidHom.coe_mk, OneHom.coe_mk, liftOn_mk]
apply (injective_frobenius L p).iterate n
rw [← f.map_iterate_frobenius, iterate_frobenius_mk,
RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm L p) n]
