English
There is a canonical S-linear map induced on the first homology of the naive cotangent complex by any morphism f: P → P'.
Русский
Существует каноническое S-линеарное отображение на первой гомологии наивного котантантного комплекса, порождаемое гомоморфизмом f: P → P'.
LaTeX
$$$\\mathrm{map}(f): P.H1Cotangent \\to_S P'.H1Cotangent \\;\\text{is defined by} \\; (\\mathrm{Cotangent.map}(f))|_{\\ker(P.cotangentComplex)}$$$
Lean4
/-- The induced map on the first homology of the (naive) cotangent complex.
-/
@[simps!]
noncomputable def map (f : Hom P P') : P.H1Cotangent →ₗ[S] P'.H1Cotangent :=
by
refine
(Cotangent.map f).restrict (p := LinearMap.ker P.cotangentComplex) (q :=
(LinearMap.ker P'.cotangentComplex).restrictScalars S) fun x hx ↦ ?_
simp only [LinearMap.mem_ker, Submodule.restrictScalars_mem] at hx ⊢
apply_fun (CotangentSpace.map f) at hx
rw [CotangentSpace.map_cotangentComplex] at hx
rw [hx]
exact LinearMap.map_zero _
