English
Compatibility between the two-step maps on cotangent spaces and cotangent complexes: map f composed with cotangentComplex is the same as composing cotangent.map and cotangentSpace.map with base change.
Русский
Совместимость двух шагов отображения котантSpaces и котантентного комплекса: map f, состыкованное с cotangentComplex, равно композиции cotangent.map и CotangentSpace.map с базовым изменением.
LaTeX
$$$\\mathrm{CotangentSpace}.map(f) \\circ P.cotangentComplex = P'.cotangentComplex.\\restrictScalars S \\circ_\\ell \\Cotangent.map f$$$
Lean4
theorem sub_one_tmul (f g : Hom P P') (x) : f.sub g (1 ⊗ₜ .D _ _ x) = 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, one_smul]
