English
The symmetrized right component of the cotangent compEquiv aligns with the liftBaseChange of the Extension.CotangentSpace.map; i.e., the symmetrized inverse composed with inr recovers liftBaseChange.
Русский
Симметричная правая часть компоновочного котант-эквивалента совместима с liftBaseChange отображения Extension.CotangentSpace.map; тождественность в точности восстанавливает liftBaseChange.
LaTeX
$$$$ (compEquiv(Q,P))^{-1} \circ \mathrm{inr}_T \; Q^{\cotangentSpace} (T \otimes_S P^{\cotangentSpace}) = \mathrm{Extension.CotangentSpace.map}(Q.toComp P).toExtensionHom \; \mathrm{liftBaseChange}_T . $$$$
Lean4
/-- Given `R[X] → S` and `S[Y] → T`, the cotangent space of `R[X][Y] → T` is isomorphic
to the direct product of the cotangent space of `S[Y] → T` and `R[X] → S` (base changed to `T`). -/
noncomputable def compEquiv :
(Q.comp P).toExtension.CotangentSpace ≃ₗ[T] Q.toExtension.CotangentSpace × (T ⊗[S] P.toExtension.CotangentSpace) :=
(Q.comp P).cotangentSpaceBasis.repr.trans (Q.cotangentSpaceBasis.prod (P.cotangentSpaceBasis.baseChange T)).repr.symm
