comp_lift — Mathlib

English

If we have a lift in the formally smooth setting, then composing it with the quotient map recovers the original map.

Русский

Если имеется подъем в постановке формально гладкого, то композиция с ограждающей проекцией восстанавливает исходную карту.

LaTeX

$$(quotient I).comp (lift I hI g) = g.$$

Lean4

@[simp]
theorem comp_lift [FormallySmooth R A] (I : Ideal B) (hI : IsNilpotent I) (g : A →ₐ[R] B ⧸ I) :
    (Ideal.Quotient.mkₐ R I).comp (FormallySmooth.lift I hI g) = g :=
  (FormallySmooth.exists_lift I hI g).choose_spec

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