English
Given a morphism of presentations f : P → P', there is a canonical linear map on cotangent spaces, functorial in f, describing how the cotangent data changes under f.
Русский
Для отображения между презентациями f : P → P' существует каноническое линейное отображение на котантстановых пространствах, сохраняющее структуру при f.
LaTeX
$$$\\mathrm{CotangentSpace}.map(f) : P.\\CotangentSpace \\to_L[S] P'.\\CotangentSpace$$$
Lean4
/-- This is the map on the cotangent space associated to a map of presentation.
The matrix associated to this map is the Jacobian matrix. See `CotangentSpace.repr_map`.
-/
protected noncomputable def map (f : Hom P P') : P.CotangentSpace →ₗ[S] P'.CotangentSpace :=
by
letI := ((algebraMap S S').comp (algebraMap P.Ring S)).toAlgebra
haveI : IsScalarTower P.Ring S S' := IsScalarTower.of_algebraMap_eq' rfl
letI := f.toAlgHom.toAlgebra
haveI : IsScalarTower P.Ring P'.Ring S' := IsScalarTower.of_algebraMap_eq (fun x ↦ (f.algebraMap_toRingHom x).symm)
apply LinearMap.liftBaseChange
refine (TensorProduct.mk _ _ _ 1).restrictScalars _ ∘ₗ KaehlerDifferential.map R R' P.Ring P'.Ring
