desc_d — Mathlib

English

For a derivation D, the desc component recovers the differential D.d on the base ring element b via a universal lift property.

Русский

Для деривации D компонент desc восстанавливает дифференциал D.d на основании через универсальное свойство подъёма.

LaTeX

$$$D^{-1} \\text{(desc }(d(b))) = D.d(b).$$$

Lean4

@[simp]
theorem desc_d (b : B) : D.desc (CommRingCat.KaehlerDifferential.d b) = D.d b :=
  by
  letI := f.hom.toAlgebra
  letI := Module.compHom M f.hom
  apply D.liftKaehlerDifferential_comp_D

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