isIdempotentComplete_iff_opposite

English

A category is idempotent complete iff its opposite category is idempotent complete.

Русский

Категория идемпотентно полна тогда и только тогда, когда её противоположная категория полна идемпотентами.

LaTeX

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

Lean4

theorem isIdempotentComplete_iff_opposite : IsIdempotentComplete Cᵒᵖ ↔ IsIdempotentComplete C :=
  by
  constructor
  · exact isIdempotentComplete_of_isIdempotentComplete_opposite
  · intro h
    apply isIdempotentComplete_of_isIdempotentComplete_opposite
    rw [isIdempotentComplete_iff_of_equivalence (opOpEquivalence C)]
    exact h

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