frobenius_pthRoot — Mathlib

English

The Frobenius and pthRoot maps compose to identity on Ring.Perfection: Frobenius_pthRoot = id.

Русский

Фробениус и pthRoot образуют тождественность: Frobenius_pthRoot = id.

LaTeX

$$$(\\mathrm{frobenius}_{p}) \\circ (\\mathrm{pthRoot} \\; R \\; p) = \\mathrm{id}_{\\mathrm{Ring.Perfection}(R,p)}$$$

Lean4

theorem frobenius_pthRoot : (frobenius _ p).comp (pthRoot R p) = RingHom.id _ :=
  RingHom.ext fun x =>
    ext fun n => by
      rw [RingHom.comp_apply, RingHom.id_apply, RingHom.map_frobenius, coeff_pthRoot, ←
        @RingHom.map_frobenius (Ring.Perfection R p) _ R, coeff_frobenius]

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