range_lift — Mathlib

English

The image of the lifted map is generated by the base image and the nilpotent perturbation.

Русский

Образ лифта образуется за счёт образа основания и нилпотентной поправки.

LaTeX

$$range_lift (fe) : (lift fe).range = fe.1.1.range ⊔ Algebra.adjoin R { fe.1 .2 }$$

Lean4

@[simp]
theorem range_lift (fe : { fe : (A →ₐ[R] B) × B // fe.2 * fe.2 = 0 ∧ ∀ a, Commute fe.2 (fe.1 a) }) :
    (lift fe).range = fe.1.1.range ⊔ Algebra.adjoin R { fe.1 .2 } := by
  simp_rw [← Algebra.map_top, ← range_inlAlgHom_sup_adjoin_eps, Algebra.map_sup, AlgHom.map_adjoin, ← AlgHom.range_comp,
    Set.image_singleton, lift_apply_eps, lift_comp_inlHom, Algebra.map_top]

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