isIdempotentComplete — Mathlib

English

Guitart exactness transfers along an equivalence of categories.

Русский

Точность Guitart переносится через эквивалентность категорий.

LaTeX

$$$ \\forall \\varepsilon: C \\simeq D, \\; IsIdempotentComplete C \\Rightarrow IsIdempotentComplete D $$$

Lean4

theorem isIdempotentComplete {D : Type*} [Category D] (ε : C ≌ D) (h : IsIdempotentComplete C) :
    IsIdempotentComplete D := by
  refine ⟨?_⟩
  intro X' p hp
  let φ := ε.counitIso.symm.app X'
  erw [split_iff_of_iso φ p (φ.inv ≫ p ≫ φ.hom)
      (by
        slice_rhs 1 2 => rw [φ.hom_inv_id]
        rw [id_comp])]
  rcases
    IsIdempotentComplete.idempotents_split (ε.inverse.obj X') (ε.inverse.map p) (by rw [← ε.inverse.map_comp, hp]) with
    ⟨Y, i, e, ⟨h₁, h₂⟩⟩
  use ε.functor.obj Y, ε.functor.map i, ε.functor.map e
  constructor
  · rw [← ε.functor.map_comp, h₁, ε.functor.map_id]
  · simp only [← ε.functor.map_comp, h₂, Equivalence.fun_inv_map]
    rfl

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