lift_self — Mathlib

English

There is an equivalence between ring homomorphisms K →* M and L →* M given by liftEquiv; the forward map is lift and the inverse maps back by precomposition with i.

Русский

Существует эквивалентность между гомоморфизмами K →* M и L →* M, заданная liftEquiv; переход вперёд = lift, обратное — композиция с i.

LaTeX

$$liftEquiv : (K →+* M) ≃ (L →+* M)$$

Lean4

@[simp]
theorem lift_self [PerfectRing L p] : lift i i p = RingHom.id L :=
  RingHom.ext (liftAux_self_apply i p)

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