sub_tmul — Mathlib

English

The difference of two cotangent-space maps is equal to the restriction of the cotangent complex map composed with the subtraction map.

Русский

Разность отображений котантпространств равна ограничению отображения котантного комплекса на композицию с вычитанием.

LaTeX

$$$\\mathrm{map\_sub\_map}(f,g) = \\mathrm{CotangentSpace}.map(f) - \\mathrm{CotangentSpace}.map(g) = (P'.cotangentComplex).restrictScalars S \\circ_\\ell (f.supto g)$$$

Lean4

@[simp]
theorem sub_tmul (f g : Hom P P') (r x) : f.sub g (r ⊗ₜ .D _ _ x) = r • Cotangent.mk (f.subToKer g x) := by
  simp only [sub, LinearMap.liftBaseChange_tmul, Derivation.liftKaehlerDifferential_comp_D, Derivation.mk_coe,
    LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply]

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