English
The base change map for the cotangent complex commutes with the cotangent map induced by composing generators: applying liftBaseChange to the base change and then base changing is the same as base changing the cotangent space map after composing.
Русский
Базовое переносное отображение для котангентного комплекса коммутирует с отображением котангентного пространства при композиции генераторов: применение liftBaseChange до переноса и затем базисное изменение эквивалентно базовому изменению отображения котангентного пространства после композиции.
LaTeX
$$$(\mathrm{Extension.CotangentSpace.map (Q.toComp P).toExtensionHom).liftBaseChange} \ T \;\circ_\ell \; P.toExtension.cotangentComplex.baseChange T = (Q.comp P).toExtension.cotangentComplex \circ_\ell (Extension.Cotangent.map (Q.toComp P).toExtensionHom).liftBaseChange T$$$
Lean4
theorem map_comp_cotangentComplex_baseChange :
(Extension.CotangentSpace.map (Q.toComp P).toExtensionHom).liftBaseChange T ∘ₗ
P.toExtension.cotangentComplex.baseChange T =
(Q.comp P).toExtension.cotangentComplex ∘ₗ
(Extension.Cotangent.map (Q.toComp P).toExtensionHom).liftBaseChange T :=
by ext x; simp [Extension.CotangentSpace.map_cotangentComplex]
