Контрамодули как контрагерентные копучки, зануляющиеся на открытой подсхеме

В развитие предыдущего математического постинга. Пусть R -- коммутативное кольцо, I ⊂ R -- идеал. Напомним, что R-модуль P называется (R,I)-контрамодулем, если Ext_R¹(R[s⁻¹],P) = 0 для любого s ∈ R и Ext_R^0,1(R[s⁻¹],P) = 0 для любого s ∈ I. Геометрически это означает, что P -- (локально контраприспособленный) контрагерентный копучок контрамодулей на формальной окрестности замкнутой подсхемы нулей I в спектре R.

Утверждение: категория (R,I)-контрамодулей эквивалентна категории (локально контраприспособленных) контрагерентных копучков на Spec R, равных нулю в ограничении на дополнение к замкнутой подсхеме нулей I.

Доказательство: утверждение тавтологично. По определению, категория контрагерентных копучков на Spec R эквивалентна категории R-модулей P со свойством Ext_R¹(R[s⁻¹],P) = 0 для любого s ∈ R. Дополнение к замкнутой подсхеме нулей I в Spec R покрывается своими открытыми подмножествами вида Spec R[s⁻¹], где s пробегает элементы I (или какую-нибудь систему образующих I как идеала). Ограничение контрагерентного копучка на Spec R, соответствующего R-модулю P, на главное открытое подмножество Spec R[s⁻¹] ⊂ Spec R, соответствует R[s⁻¹]-модулю Hom_R(R[s⁻¹],P). Конец доказательства.

Что-то важное должно проистекать из этой тавтологии, но я не понимаю пока, что.