liftOfSurjective — Mathlib

English

For a formally smooth R-algebra A and a surjective g: B → C with nilpotent kernel, there is a lift of f: A → C to B.

Русский

Для формально гладкого R-алгебры A и сюръективного g: B → C с нильпотентным ядром существует подъем f: A → B к g.

LaTeX

$$liftOfSurjective f g hg hg' : A → B with g ∘ liftOfSurjective f g hg hg' = f.$$

Lean4

/-- For a formally smooth `R`-algebra `A` and a map `f : A →ₐ[R] B ⧸ I` with `I` nilpotent,
this is an arbitrary lift `A →ₐ[R] B`. -/
noncomputable def liftOfSurjective [FormallySmooth R A] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (hg : Function.Surjective g)
    (hg' : IsNilpotent <| RingHom.ker (g : B →+* C)) : A →ₐ[R] B :=
  FormallySmooth.lift _ hg' ((Ideal.quotientKerAlgEquivOfSurjective hg).symm.toAlgHom.comp f)

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