Еще одна версия любимой теоремы о полной строгости
В духе предложения 1.5 из 1102.0261 и далее -- их уже много по нынешним временам -- следствий A.2.1(b-c)/А.5.2 из 1209.2995 и др. -- нельзя ли доказать следующие утверждения?

Теорема 1. Пусть C -- кокольцо над ассоциативным кольцом A; предположим, что C является плоским правым A-модулем. Тогда копроизводная категория абелевой категории левых C-комодулей эквивалентна факторкатегории гомотопической категории комплексов коиндуцированных левых C-комодулей по ее минимальной триангулированной категории, содержащей тотализации точных троек комплексов C-комодулей, почленно коиндуцированных с точных троек A-модулей, и замкнутой относительно бесконечных прямых сумм.

Теорема 2. Пусть C -- кокольцо над ассоциативным кольцом A; предположим, что C является проективным левым A-модулем. Тогда контрапроизводная категория абелевой категории левых C-контрамодулей эквивалентна факторкатегории гомотопической категории комплексов индуцированных левых C-контрамодулей по ее минимальной триангулированной категории, содержащей тотализации точных троек комплексов C-контрамодулей, почленно индуцированных с точных троек A-модулей, и замкнутой относительно бесконечных произведений.

Теорема 3. Пусть C -- кокольцо над ассоциативным кольцом A; предположим, что C является плоским левым A-модулем. Тогда контрапроизводная категория точной категории левых C-контрамодулей A-кокручения эквивалентна факторкатегории гомотопической категории комплексов левых C-контрамодулей, (почленно) индуцированых с А-модулей кокручения, по ее минимальной триангулированной категории, содержащей тотализации точных троек комплексов C-контрамодулей, почленно индуцированных с точных троек A-модулей кокручения, и замкнутой относительно бесконечных произведений.

Во всех трех случаях, сравнительно несложно показать, что естественный функтор (индуцированный вложением гомотопических категорий) является функтором локализации по Вердье. Трудность в проверке полной строгости (или, хотя бы, консервативности). На этот предмет и используется длинное рассуждение из 1102.0261.

Будет ли оно работать в этой ситуации, где индуцированные контрамодули (или коиндуцированные комодули) не образуют даже точной категории?