lift_comp_lift_eq_id — Mathlib

English

The composition of lifts is the identity ring hom on L: (lift j i p) ∘ (lift i j p) = id_L.

Русский

Состав подъёмов равен тождественному отображению на L: (lift j i p) ∘ (lift i j p) = id_L.

LaTeX

$$$ (\mathrm{lift}\, j\, i\, p) \circ (\mathrm{lift}\, i\, j\, p) = \mathrm{id}\,L $$$

Lean4

theorem lift_comp_lift_eq_id [PerfectRing L p] : (lift j i p).comp (lift i j p) = RingHom.id L :=
  RingHom.ext (lift_comp_lift_apply_eq_self i j p)

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