Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-06 09:40 631175a8

View on Github →

feat(category_theory/idempotents): universal property of karoubi (#17603)

Estimated changes

Modified src/category_theory/idempotents/functor_extension.lean

added theorem category_theory.idempotents.functor_extension₁_comp

added def category_theory.idempotents.functor_extension₁_comp_whiskering_left_to_karoubi_iso

added def category_theory.idempotents.functor_extension₂

added theorem category_theory.idempotents.functor_extension₂_comp_whiskering_left_to_karoubi

added def category_theory.idempotents.functor_extension₂_comp_whiskering_left_to_karoubi_iso

added theorem category_theory.idempotents.karoubi_universal_functor_eq

added def category_theory.idempotents.karoubi_universal₁.counit_iso

added def category_theory.idempotents.karoubi_universal₁

added theorem category_theory.idempotents.karoubi_universal₂_functor_eq