instFullKaroubiFunctorKaroubiFunctorCategoryEmbedding

English

If C is idempotent complete, then the functor category J ⥤ C is idempotent complete.

Русский

Если C удовлетворяет условию идемпотентного дополнения, то функторная категория J ⥤ C также идемпотентно дополнена.

LaTeX

$$IsIdempotentComplete(J ⥤ C)$$

Lean4

instance : (karoubiFunctorCategoryEmbedding J C).Full where
  map_surjective {P Q}
    f :=
    ⟨{  f :=
          { app := fun j => (f.app j).f
            naturality := fun j j' φ => by
              rw [← Karoubi.comp_p_assoc]
              have h := hom_ext_iff.mp (f.naturality φ)
              simp only [comp_f] at h
              dsimp [karoubiFunctorCategoryEmbedding] at h
              erw [← h, assoc, ← P.p.naturality_assoc φ, p_comp (f.app j')] }
        comm := by
          ext j
          exact (f.app j).comm },
      rfl⟩

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