isIdempotentComplete_iff_of_equivalence

English

If C and D are equivalent, idempotent completeness is preserved in both directions.

Русский

Если C и D эквивалентны, идемпотентная полнота сохраняется в обоих направлениях.

LaTeX

$$$ \\text{IsIdempotentComplete } C \\iff \\text{IsIdempotentComplete } D $ under \\varepsilon: C \\simeq D$$

Lean4

/-- If `C` and `D` are equivalent categories, that `C` is idempotent complete iff `D` is. -/
theorem isIdempotentComplete_iff_of_equivalence {D : Type*} [Category D] (ε : C ≌ D) :
    IsIdempotentComplete C ↔ IsIdempotentComplete D :=
  by
  constructor
  · exact Equivalence.isIdempotentComplete ε
  · exact Equivalence.isIdempotentComplete ε.symm

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