isIdempotentComplete_of_isIdempotentComplete_opposite

English

Idempotent completeness is preserved under opposite categories.

Русский

Идемпотентная полнота сохраняется при рассмотрении противоположной категории.

LaTeX

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

Lean4

theorem isIdempotentComplete_of_isIdempotentComplete_opposite (h : IsIdempotentComplete Cᵒᵖ) : IsIdempotentComplete C :=
  by
  refine ⟨?_⟩
  intro X p hp
  rcases IsIdempotentComplete.idempotents_split (op X) p.op (by rw [← op_comp, hp]) with ⟨Y, i, e, ⟨h₁, h₂⟩⟩
  use Y.unop, e.unop, i.unop
  constructor
  · simp only [← unop_comp, h₁]
    rfl
  · simp only [← unop_comp, h₂]
    rfl

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