English
The construction tensorCotangentInvFun provides a universal, functorial map from cotangent data over Q back to a tensor product of the base with the cotangent data over P, designed to be inverse to the tensorCotangent map along a formally étale map. It is a tool to realize the inverse of the base-change for cotangent spaces.
Русский
Конструкция tensorCotangentInvFun задаёт универсальную, функториальную передачу котангенентальных данных над Q обратно в тензорное произведение над S с котангенентальными данными над P, рассчитанную как обратная к отображению tensorCotangent вдоль формально этиального отображения. Это инструмент для реализации обратного базового изменения котангенентальных пространств.
LaTeX
$$$\\text{tensorCotangentInvFun}(f, halg, H) : Q.Cotangent \\to T \\otimes_S P.Cotangent$ является частной инверсией toTensorCotangent$$$
Lean4
theorem tensorCotangentInvFun_smul_mk [alg : Algebra P.Ring Q.Ring] (halg : algebraMap P.Ring Q.Ring = f.toRingHom)
(H : Function.Bijective ((f.mapKer halg).liftBaseChange Q.Ring)) (x : Q.Ring) (y : P.ker) :
tensorCotangentInvFun f halg H (x • .mk ⟨f.toRingHom y, (f.mapKer halg y).2⟩) = x • 1 ⊗ₜ .mk y :=
by
letI := ((algebraMap S T).comp (algebraMap P.Ring S)).toAlgebra
haveI : IsScalarTower P.Ring S T := .of_algebraMap_eq' rfl
haveI : IsScalarTower P.Ring Q.Ring T := .of_algebraMap_eq fun r ↦ halg ▸ (f.algebraMap_toRingHom r).symm
letI e := LinearEquiv.ofBijective _ H
trans tensorCotangentInvFun f halg H (.mk ((f.mapKer halg).liftBaseChange Q.Ring (x ⊗ₜ y)))
· simp; rfl
change ((TensorProduct.mk _ _ _ 1).restrictScalars _ ∘ₗ Cotangent.mk).liftBaseChange _ (e.symm (e (x ⊗ₜ y))) = _
rw [e.symm_apply_apply]
simp
