mk_lift — Mathlib

English

For a formallly smooth R-algebra A, there is a lift function that assigns to I and hI and g a lift A → B.

Русский

Для формально гладкого R-алгебры A существует операция подъема, которая сопоставляет I, hI и g отображение A → B.

LaTeX

$$lift : I → A → B under FormallySmooth is defined (noncomputable).$$

Lean4

@[simp]
theorem mk_lift [FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) (x : A) :
    Ideal.Quotient.mk I (FormallySmooth.lift I hI g x) = g x :=
  AlgHom.congr_fun (FormallySmooth.comp_lift I hI g :) x

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