English
Compatibility of maps under localization and cotangent construction is ensured by a structural equality.
Русский
Совместимость отображений при локализации и построении котангентов гарантирована структурным равенством.
LaTeX
$$$$ \mathrm{Cotangent}.map (g.comp f) = (\mathrm{map}~g).restrictScalars S \circ \mathrm{map} f $$$$
Lean4
/-- A hom between two extensions induces a map between cotangent spaces. -/
noncomputable def map (f : Hom P P') : P.Cotangent →ₗ[S] P'.Cotangent
where
toFun
x :=
.of
(Ideal.mapCotangent (R := R) _ _ f.toAlgHom (fun x hx ↦ by simpa using RingHom.congr_arg (algebraMap S S') hx)
x.val)
map_add' x y := ext (map_add _ x.val y.val)
map_smul' r
x := by
ext
obtain ⟨x, rfl⟩ := Cotangent.mk_surjective x
obtain ⟨r, rfl⟩ := P.algebraMap_surjective r
simp only [algebraMap_smul, val_smul', val_mk, val_of, Ideal.mapCotangent_toCotangent, RingHomCompTriple.comp_apply,
← (Ideal.toCotangent _).map_smul]
conv_rhs =>
rw [← algebraMap_smul S', ← f.algebraMap_toRingHom, algebraMap_smul, val_smul', val_of, ←
(Ideal.toCotangent _).map_smul]
congr 1
ext1
simp only [SetLike.val_smul, smul_eq_mul, map_mul, Hom.toAlgHom_apply]
