instIsIdempotentCompleteOpposite

Mathlib.CategoryTheory.Idempotents.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Idempotents.instIsIdempotentCompleteOpposite

English

If an idempotent completion holds for C, then it holds for Cᵒᵖ.

Русский

Если идемпотентная полнота выполняется для C, то она выполняется и для Cᵒᵖ.

LaTeX

$$$ \\text{IsIdempotentComplete } C \\Rightarrow \\text{IsIdempotentComplete } C^\\mathrm{op} $$$

Lean4

instance [IsIdempotentComplete C] : IsIdempotentComplete Cᵒᵖ := by rwa [isIdempotentComplete_iff_opposite]

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru