>это идиотская книга Хартсхорна Residues and Duality, и гениальное приложение к ней, на 5 страниц, написанное Делинем

По-моему, двойственность Гротендика как раз пример, где требуется очень много усилий, чтобы доказать, что все конструкции согласованы правильным образом. Мне понадобилось для двойственности Пуанкаре обобщать конструкцию f^! на универсально когерентные схемы (например, конечно-представленные над кольцом валюации) и пришлось проверять все согласованности, я следовал Липману-Ниману, там в сумме выходит очень много проверок.

Книжка Хартсхорна же в этом плане абсолютно ужасная и непригодная, там просто какой-то ужас происходит, когда он пытается проверить согласованность хоть чего-либо. Самое ужасное, что Габбер с Рамеро в книжке по почти математике строят этот функтор f^! в похожих предположениях, переговаривая книжку Харстхорна, и читать это абсолютно невозможно. Конструкцию следа они в итоге так и не обсуждают, ну или я не смог это найти в их трактате на 2000 страниц.

Но даже в основаниях Нимана, многие детали сложно проверять. Например, имхо совершенно неочевидно (дажё в нётеровом случае) что если есть плоский конечно-представленный морфизм f:X-->S и морфизм g:S'-->S с морфизмами в расслоенной диаграмме f':X'-->S', g':X'-->X, то есть изоморфизм функторов Lg'^*f^! --> f'^!Lg^*. В собственном случае морфизм приходит как сопряжённый к f^! --> f^!g_*Lg^* <-- Lg'_*f'^!Lg^* (вторую стрелку надо обернуть), где вторая стрелка изоморфизм из тор-независимости.

В общем случае не очень понятно как определить эту стрелку, потому что f^! определяется через выбор компактификации, а как выбрать тор-независимую c g:S'-->S компактификацию я не знаю. На удивление этот вопрос везде обходится стороной, я не нашёл ссылки на построение этого морфизма и доказательство того, что это изоморфизм за пределами Коэн-Маколеевого случая, который сделан в книжке Конрада в основаниях Харстхорна.

Единственный аргумент вне собственного случая, который я придумал, это во-первых показать, что в плоском случае имеется изоморфизм f^!(-) \cong f^*(-) \otimes^L f^!\O_S. Тогда достаточно определять морфизм на f^!\O_S, но это дуализирующий комплекс, который приходит с канонической структурой "rigidification", поэтому из локального вычисления Lg'^*(f^!)\O_S есть дуализирующий комплекс + там есть каноническая структура "rigification", которая задаёт канонический изоморфизм с другой такой структурой на f'^!\O_{S'}. Но тогда встаёт вопрос почему этот морфизм согласован с морфизмом, который построен выше в собственном случае, я не знаю как это проверять без проверки коммутативности кучи диаграмм. Это важно, например, потому что в таком определении неочевидно, что эта замена базы коммутирует со следом в собственном случае, а конструкция из собственного случая коммутирует со следом из абстрактных соображений (хотя там тоже коммутативность диаграмм проверять, но не таких сложных).