liftOfDerivationToSquareZero_mk_apply

English

For a derivation d: A → I, the quotient map of the lift evaluated at x equals the canonical image in the quotient; i.e., the quotient of lift x equals algebra map to the quotient.

Русский

Для денерации d: A → I, изображение лифта через квазиформу на x равно каноническому изображению в факторкольце; то есть квота lift x совпадает с алгебраической картой к B/I.

LaTeX

$$$\big( Ideal.Quotient.mk I \big) ( liftOfDerivationToSquareZero I hI d x ) = algebraMap A (HasQuotient.Quotient B I) x$$$

Lean4

theorem liftOfDerivationToSquareZero_mk_apply [IsScalarTower R A B] (d : Derivation R A I) (x : A) :
    Ideal.Quotient.mk I (liftOfDerivationToSquareZero I hI d x) = algebraMap A (B ⧸ I) x :=
  by
  rw [liftOfDerivationToSquareZero_apply, map_add, Ideal.Quotient.eq_zero_iff_mem.mpr (d x).prop, zero_add]
  rfl

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