Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-09 07:16 78c39752

View on Github →

feat(category_theory/pseudoabelian/basic): basic facts and contructions about pseudoabelian categories (#11817)

Estimated changes

Created src/category_theory/idempotents/basic.lean

added theorem category_theory.idempotents.equivalence.is_idempotent_complete

added theorem category_theory.idempotents.idempotence_of_id_sub_idempotent

added theorem category_theory.idempotents.is_idempotent_complete_iff_has_equalizer_of_id_and_idempotent

added theorem category_theory.idempotents.is_idempotent_complete_iff_idempotents_have_kernels

added theorem category_theory.idempotents.is_idempotent_complete_iff_of_equivalence

added theorem category_theory.idempotents.is_idempotent_complete_iff_opposite

added theorem category_theory.idempotents.is_idempotent_complete_of_is_idempotent_complete_opposite

added theorem category_theory.idempotents.split_iff_of_iso

added theorem category_theory.idempotents.split_imp_of_iso

Created src/category_theory/idempotents/karoubi.lean

added theorem category_theory.idempotents.karoubi.coe_X

added theorem category_theory.idempotents.karoubi.coe_p

added theorem category_theory.idempotents.karoubi.comp

added theorem category_theory.idempotents.karoubi.comp_p

added theorem category_theory.idempotents.karoubi.comp_proof

added theorem category_theory.idempotents.karoubi.decomp_id

added def category_theory.idempotents.karoubi.decomp_id_i

added theorem category_theory.idempotents.karoubi.decomp_id_i_naturality

added theorem category_theory.idempotents.karoubi.decomp_id_i_to_karoubi

added def category_theory.idempotents.karoubi.decomp_id_p

added theorem category_theory.idempotents.karoubi.decomp_id_p_naturality

added theorem category_theory.idempotents.karoubi.decomp_id_p_to_karoubi

added theorem category_theory.idempotents.karoubi.decomp_p

added theorem category_theory.idempotents.karoubi.eq_to_hom_f

added theorem category_theory.idempotents.karoubi.ext

added structure category_theory.idempotents.karoubi.hom

added theorem category_theory.idempotents.karoubi.hom_eq_zero_iff

added theorem category_theory.idempotents.karoubi.hom_ext

added theorem category_theory.idempotents.karoubi.id_eq

added def category_theory.idempotents.karoubi.inclusion_hom

added theorem category_theory.idempotents.karoubi.p_comm

added theorem category_theory.idempotents.karoubi.p_comp

added theorem category_theory.idempotents.karoubi.sum_hom

added structure category_theory.idempotents.karoubi

added def category_theory.idempotents.to_karoubi

added def category_theory.idempotents.to_karoubi_is_equivalence

Modified src/category_theory/preadditive/default.lean

added theorem category_theory.preadditive.has_kernel_of_has_equalizer