English
The first projection of compEquiv matches the map on cotangent spaces induced by composition; i.e., the left projection of compEquiv equals the base-change cotangent map.
Русский
Первая проекция compEquiv совпадает с отображением котантного пространства, индуцированного композицией; то есть левая проекция равна базовому изменению котантного пространства.
LaTeX
$$$$ (compEquiv(Q,P) ) x).fst = \mathrm{Extension.CotangentSpace.map}(Q.ofComp P).toExtensionHom(x). $$$$
Lean4
theorem exact :
Function.Exact ((Extension.CotangentSpace.map (Q.toComp P).toExtensionHom).liftBaseChange T)
(Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) :=
by
rw [← fst_compEquiv, ← compEquiv_symm_inr]
conv_rhs => rw [← LinearEquiv.symm_symm (compEquiv Q P)]
rw [LinearEquiv.conj_exact_iff_exact]
exact Function.Exact.inr_fst
