Commit 2023-04-06 14:19 e9d9a6f5

View on Github →

feat: port CategoryTheory.Idempotents.Karoubi (#3291)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Idempotents/Karoubi.lean

added structure CategoryTheory.Idempotents.Karoubi.Hom

added theorem CategoryTheory.Idempotents.Karoubi.coe_X

added theorem CategoryTheory.Idempotents.Karoubi.coe_p

added theorem CategoryTheory.Idempotents.Karoubi.comp_f

added theorem CategoryTheory.Idempotents.Karoubi.comp_p

added theorem CategoryTheory.Idempotents.Karoubi.comp_proof

added theorem CategoryTheory.Idempotents.Karoubi.decompId

added def CategoryTheory.Idempotents.Karoubi.decompId_i

added theorem CategoryTheory.Idempotents.Karoubi.decompId_i_naturality

added theorem CategoryTheory.Idempotents.Karoubi.decompId_i_toKaroubi

added def CategoryTheory.Idempotents.Karoubi.decompId_p

added theorem CategoryTheory.Idempotents.Karoubi.decompId_p_naturality

added theorem CategoryTheory.Idempotents.Karoubi.decompId_p_toKaroubi

added theorem CategoryTheory.Idempotents.Karoubi.decomp_p

added theorem CategoryTheory.Idempotents.Karoubi.eqToHom_f

added theorem CategoryTheory.Idempotents.Karoubi.ext

added theorem CategoryTheory.Idempotents.Karoubi.hom_eq_zero_iff

added theorem CategoryTheory.Idempotents.Karoubi.hom_ext

added theorem CategoryTheory.Idempotents.Karoubi.hom_ext_iff

added theorem CategoryTheory.Idempotents.Karoubi.id_eq

added def CategoryTheory.Idempotents.Karoubi.inclusionHom

added theorem CategoryTheory.Idempotents.Karoubi.p_comm

added theorem CategoryTheory.Idempotents.Karoubi.p_comp

added theorem CategoryTheory.Idempotents.Karoubi.sum_hom

added theorem CategoryTheory.Idempotents.Karoubi.zsmul_hom

added structure CategoryTheory.Idempotents.Karoubi

added def CategoryTheory.Idempotents.toKaroubi

added def CategoryTheory.Idempotents.toKaroubi_equivalence

added def CategoryTheory.Idempotents.toKaroubi_isEquivalence