English
For f,g : P.Hom P' and r ∈ S, x ∈ P.Ring, the action on r ⊗ D x satisfies f.sub g(r ⊗ D x) = r • Cotangent.mk (f.subToKer g x).
Русский
Для отображений f,g и элементов r∈S, x∈P.Ring выполнено \(f.- g\) на \(r ⊗ D x\) равно \(r\) умножить на котантскую константу.
LaTeX
$$$f.\\mathrm{sub}(g)(r \\otimes_D x) = r \\cdot \\mathrm{Cotangent.mk}(f.\\mathrm{subToKer}\, g\\, x)$$$
Lean4
theorem map_sub_map (f g : Hom P P') :
CotangentSpace.map f - CotangentSpace.map g = P'.cotangentComplex.restrictScalars S ∘ₗ (f.sub g) :=
by
ext x
induction x using TensorProduct.induction_on with
| zero => simp only [map_zero]
| add => simp only [map_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, *]
| tmul x y =>
obtain ⟨y, rfl⟩ := KaehlerDifferential.tensorProductTo_surjective _ _ y
induction y with
| zero => simp only [map_zero, tmul_zero]
| add => simp only [map_add, tmul_add, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, *]
| tmul =>
simp only [Derivation.tensorProductTo_tmul, tmul_smul, smul_tmul', LinearMap.sub_apply, map_tmul,
Hom.toAlgHom_apply, LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, Hom.sub_tmul,
LinearMap.map_smul_of_tower, cotangentComplex_mk, Hom.subToKer_apply_coe, map_sub, ← algebraMap_eq_smul_one,
tmul_sub, smul_sub]
