English
For morphisms f : P → P' and g : P' → P'', the map on cotangent spaces respects composition: map(g ∘ f) = restrictScalars_S ∘ map f then map g.
Русский
Для отображений f: P→P' и g: P'→P'' отображение на котант пространства удовлетворяет композиции: map(g∘f) = restrictScalars_S ∘ map f затем map g.
LaTeX
$$$\\mathrm{CotangentSpace}.map(g\\circ f) = (\\mathrm{CotangentSpace}.map g).\\restrictScalars S \\circ_\\ell \\mathrm{CotangentSpace}.map f$$$
Lean4
theorem map_comp (f : Hom P P') (g : Hom P' P'') :
CotangentSpace.map (g.comp f) = (CotangentSpace.map g).restrictScalars S ∘ₗ CotangentSpace.map f :=
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', map_tmul, Hom.toAlgHom_apply,
Hom.comp_toRingHom, RingHom.coe_comp, Function.comp_apply, LinearMap.coe_comp, LinearMap.coe_restrictScalars,
← IsScalarTower.algebraMap_apply S S' S'']
