lift_lift — Mathlib

English

Applying lift g after lift i j p yields the same as lifting the composite g ∘ i with j: lift g (lift i j p) p = lift (g ∘ i) j p.

Русский

Применение подъёма g после подъёма i j p эквивалентно подъёму по композиции g ∘ i с j: lift g (lift i j p) p = lift (g ∘ i) j p.

LaTeX

$$$ \operatorname{lift}\, g\, (\operatorname{lift}\, i\, j\, p)\, p = \operatorname{lift}\, (g \circ i)\, j\, p $$$

Lean4

@[simp]
theorem lift_lift : lift g (lift i j p) p = lift (g.comp i) j p :=
  by
  refine IsPRadical.injective_comp_of_perfect _ (g.comp i) p ?_
  simp_rw [← RingHom.comp_assoc _ _ (lift g _ p), lift_comp]

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