lift — Mathlib

English

Given rings R,S of characteristic p with R perfect, any ring homomorphism R →+* S can be lifted to a homomorphism R →+* Perfection S p, giving an equivalence between these two Hom-sets.

Русский

Пусть R,S имеют характеристику p и R совершенное; любой гомоморфизм R →+* S может быть вознесён до гомоморфизма R →+* Perfection S p, образуя эквиваленцию между соответствующими множествами гомоморфизмов.

LaTeX

$$$\\text{ lift }(p)\\; R\\; S:\\; (R \\to+* S) \\simeq (R \\to+* \\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 →+* Perfection S p`. -/
@[simps]
noncomputable def lift (R : Type u₁) [CommSemiring R] [CharP R p] [PerfectRing R p] (S : Type u₂) [CommSemiring S]
    [CharP S p] : (R →+* S) ≃ (R →+* Ring.Perfection S p)
    where
  toFun
    f :=
    { toFun := fun r =>
        ⟨fun n => f (((frobeniusEquiv R p).symm : R →+* R)^[n] r), fun n => by
          rw [← f.map_pow, Function.iterate_succ_apply', RingHom.coe_coe, frobeniusEquiv_symm_pow_p]⟩
      map_one' := ext fun _ => (congr_arg f <| iterate_map_one _ _).trans f.map_one
      map_mul' := fun _ _ => ext fun _ => (congr_arg f <| iterate_map_mul _ _ _ _).trans <| f.map_mul _ _
      map_zero' := ext fun _ => (congr_arg f <| iterate_map_zero _ _).trans f.map_zero
      map_add' := fun _ _ => ext fun _ => (congr_arg f <| iterate_map_add _ _ _ _).trans <| f.map_add _ _ }
  invFun := RingHom.comp <| coeff S p 0
  right_inv
    f :=
    RingHom.ext fun r =>
      ext fun n =>
        show coeff S p 0 (f (((frobeniusEquiv R p).symm)^[n] r)) = coeff S p n (f r) by
          rw [← coeff_iterate_frobenius _ 0 n, zero_add, ← RingHom.map_iterate_frobenius,
            Function.RightInverse.iterate (frobenius_apply_frobeniusEquiv_symm R p) n]

Похожие утверждения