equiv — Mathlib

English

The underlying RingHom of the isomorphism equiv i j p is exactly PerfectRing.lift i j p.

Русский

Базовый RingHom из изоморфизма equiv i j p совпадает с PerfectRing.lift i j p.

LaTeX

$$$ (equiv\ i\ j\ p).toRingHom = \operatorname{PerfectRing.lift} i j p $$$

Lean4

/-- If `L` and `M` are both perfect closures of `K`, then there is a ring isomorphism `L ≃+* M`.
This is similar to `IsAlgClosure.equiv` and `IsSepClosure.equiv`. -/
def equiv : L ≃+* M where
  __ := PerfectRing.lift i j p
  invFun := PerfectRing.liftAux j i p
  left_inv := PerfectRing.lift_comp_lift_apply_eq_self i j p
  right_inv := PerfectRing.lift_comp_lift_apply_eq_self j i p

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