English
The inverse construction tensorCotangentInvFun provides a canonical way to recover cotangent data after a formal étale base change, acting as a formal inverse to tensorCotangent under appropriate hypotheses. It is a step in comparing cotangent spaces along étale maps.
Русский
Обратная конструкция tensorCotangentInvFun обеспечивает канонический способ восстановления котангенентного (cotangent) данных после формального этиального базового изменения, выступая как формальная обратная операция к tensorCotangent при соответствующих предположениях. Это часть сравнения котангенентных пространств вдоль этиальных отображений.
LaTeX
$$$\\text{tensorCotangentInvFun}(f,\\text{halg},H) : Q.\\Cotangent \\to T \\otimes_S P.\\Cotangent$ является обратной к \\text{tensorCotangent}(f, halg, H)$$$
Lean4
instance isLocalizedModule_map (M : Submonoid S) [IsLocalization M T] : IsLocalizedModule M (map R R S T) :=
have := Algebra.FormallyEtale.of_isLocalization (Rₘ := T) M
(isLocalizedModule_iff_isBaseChange M T _).mpr (isBaseChange_of_formallyEtale R S T)
