Commit 2023-04-06 15:42 8f5e0418

View on Github →

feat: port CategoryTheory.Idempotents.FunctorCategories (#3301)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Idempotents/FunctorCategories.lean

added def CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map

added def CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj

added theorem CategoryTheory.Idempotents.app_comp_p

added theorem CategoryTheory.Idempotents.app_idem

added theorem CategoryTheory.Idempotents.app_p_comm

added theorem CategoryTheory.Idempotents.app_p_comp

added def CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding

added theorem CategoryTheory.Idempotents.toKaroubi_comp_karoubiFunctorCategoryEmbedding

Modified Mathlib/CategoryTheory/Idempotents/Karoubi.lean