Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-08-08 21:44 e75326d4

View on Github →

feat(category/idempotents): extension of functors to the idempotent completion (#15746) This PR show that functors C ⥤ karoubi D can be canonically extended to functors karoubi C ⥤ karoubi D.

Estimated changes

Modified src/category_theory/eq_to_hom.lean

added theorem category_theory.functor.congr_map

Modified src/category_theory/idempotents/functor_categories.lean

added theorem category_theory.idempotents.app_comp_p

added theorem category_theory.idempotents.app_idem

added theorem category_theory.idempotents.app_p_comm

added theorem category_theory.idempotents.app_p_comp

Created src/category_theory/idempotents/functor_extension.lean

added def category_theory.idempotents.functor_extension₁.map

added def category_theory.idempotents.functor_extension₁.obj

added def category_theory.idempotents.functor_extension₁

added theorem category_theory.idempotents.functor_extension₁_comp_whiskering_left_to_karoubi

added theorem category_theory.idempotents.nat_trans_eq