English
There is a linear map from the cotangent space to the kernel capturing the deviation between two maps f and g, i.e., the difference f − g factors through the kernel.
Русский
Существует линейное отображение от котантпространства в ядро, фиксирующее расхождение между f и g; разность факторизуется через ядро.
LaTeX
$$$\\mathrm{sub}(f,g) : P.\\CotangentSpace \\to_L[S] P'.\\ker$ with $\\mathrm{im}(f - g) \\subseteq \\ker$$$
Lean4
/-- If `f` and `g` are two maps `P → P'` between presentations,
their difference induces a map `P.CotangentSpace →ₗ[S] P'.Cotangent` that makes two maps
between the cotangent complexes homotopic.
-/
noncomputable def sub (f g : Hom P P') : P.CotangentSpace →ₗ[S] P'.Cotangent :=
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
haveI : IsScalarTower R P.Ring S' :=
IsScalarTower.of_algebraMap_eq fun x ↦
show algebraMap R S' x = algebraMap S S' (algebraMap P.Ring S (algebraMap R P.Ring x)) by
rw [← IsScalarTower.algebraMap_apply R P.Ring S, ← IsScalarTower.algebraMap_apply]
refine (Derivation.liftKaehlerDifferential ?_).liftBaseChange S
refine
{ __ := Cotangent.mk.restrictScalars R ∘ₗ f.subToKer g
map_one_eq_zero' := ?_
leibniz' := ?_ }
· ext
simp [Ideal.toCotangent_eq_zero]
· intro x y
ext
simp only [LinearMap.coe_comp, LinearMap.coe_restrictScalars, Function.comp_apply, Cotangent.val_mk,
Cotangent.val_add, Cotangent.val_smul''', ← map_smul, ← map_add, Ideal.toCotangent_eq]
exact Hom.sub_aux f g x y
