Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-26 23:31 163d1a6d

View on Github →

feat(category_theory/idempotents): idempotent completeness and functor categories (#12270)

Estimated changes

Created src/category_theory/idempotents/functor_categories.lean

added def category_theory.idempotents.karoubi_functor_category_embedding.map

added def category_theory.idempotents.karoubi_functor_category_embedding.obj

added def category_theory.idempotents.karoubi_functor_category_embedding

added theorem category_theory.idempotents.to_karoubi_comp_karoubi_functor_category_embedding

Created src/category_theory/idempotents/simplicial_object.lean