Karoubi

📁 Source: Mathlib/CategoryTheory/Idempotents/Karoubi.lean

Statistics

Metric	Count
Definitions Karoubi, f, X, decompId_i, decompId_p, inclusionHom, instCategory, instInhabitedHomOfPreadditive, p, retract, instAdd, instAddCommGroupHom, instNeg, instPreadditiveKaroubi, instZero, toKaroubi, toKaroubiEquivalence	17
Theorems comm, ext, ext_iff, coe_X, coe_p, comp_f, comp_p, comp_p_assoc, comp_proof, decompId, decompId_assoc, decompId_i_f, decompId_i_naturality, decompId_i_toKaroubi, decompId_p_f, decompId_p_naturality, decompId_p_toKaroubi, decomp_p, eqToHom_f, ext, hom_eq_zero_iff, hom_ext, hom_ext_iff, id_f, idem, idem_assoc, inclusionHom_apply, p_comm, p_comm_assoc, p_comp, p_comp_assoc, retract_i_f, retract_r_f, sum_hom, zsmul_hom, add_def, instAdditiveKaroubiToKaroubi, instEssSurjKaroubiToKaroubiOfIsIdempotentComplete, instFaithfulKaroubiToKaroubi, instFullKaroubiToKaroubi, instIsIdempotentCompleteKaroubi, instPreservesEpimorphismsKaroubiToKaroubi, instPreservesMonomorphismsKaroubiToKaroubi, neg_def, toKaroubiEquivalence_functor_additive, toKaroubi_isEquivalence, toKaroubi_map_f, toKaroubi_obj_X, toKaroubi_obj_p, zero_def	50
Total	67

CategoryTheory.Idempotents

Definitions

Name	Category	Theorems
Karoubi 📖	CompData	210 math math: KaroubiFunctorCategoryEmbedding.obj_map_f, Karoubi.karoubi_hasFiniteBiproducts, CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_p, karoubiChainComplexEquivalence_inverse_obj_X_d, toKaroubi_comp_karoubiFunctorCategoryEmbedding, KaroubiKaroubi.equivalence_counitIso, AlgebraicTopology.DoldKan.N₁_map_f, karoubiChainComplexEquivalence_functor_obj_X_X, neg_def, toKaroubi_isEquivalence, instIsEquivalenceFunctorKaroubiFunctorExtension₂, KaroubiKaroubi.equivalence.additive_inverse, karoubiCochainComplexEquivalence_functor_map_f_f, functorExtension₁CompWhiskeringLeftToKaroubiIso_inv_app_app_f, KaroubiHomologicalComplexEquivalence.Inverse.map_f_f, functorExtension₂_map_app_f, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.identity_N₂, instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi, karoubiHomologicalComplexEquivalence_functor, KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_f, CategoryTheory.Preadditive.DoldKan.equivalence_unitIso, AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans, CategoryTheory.Abelian.LeftResolution.karoubi.π_app_toKaroubi_obj, CategoryTheory.Abelian.LeftResolution.karoubi.F'_map_f, karoubiCochainComplexEquivalence_inverse_obj_p_f, CategoryTheory.Preadditive.DoldKan.equivalence_functor, karoubiUniversal_functor_eq, functorExtension_map_app, Karoubi.Biproducts.bicone_ι_f, KaroubiKaroubi.counitIso_inv_app_f_f, add_def, karoubiUniversal₁_functor, karoubiChainComplexEquivalence_functor_obj_X_p, Karoubi.decompId_p_naturality, AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans, Karoubi.hom_eq_zero_iff, AlgebraicTopology.DoldKan.N₁_obj_p, CategoryTheory.Preadditive.DoldKan.equivalence_counitIso, Karoubi.inclusionHom_apply, karoubiChainComplexEquivalence_inverse_obj_p_f, Karoubi.eqToHom_f, instIsEquivalenceFunctorKaroubiFunctorExtension, toKaroubiEquivalence_functor_additive, Karoubi.retract_r_f, functorExtension₂CompWhiskeringLeftToKaroubiIso_hom_app_app_f, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, CategoryTheory.Abelian.LeftResolution.karoubi_π, functorExtension₁CompWhiskeringLeftToKaroubiIso_hom_app_app_f, karoubiHomologicalComplexEquivalence_unitIso, karoubiHomologicalComplexEquivalence_inverse, KaroubiHomologicalComplexEquivalence.counitIso_inv, DoldKan.hε, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, DoldKan.N₂_map_isoΓ₀_hom_app_f, FunctorExtension₁.obj_obj_X, karoubiCochainComplexEquivalence_unitIso_hom_app_f_f, karoubiChainComplexEquivalence_functor_map_f_f, functorExtension₂_obj_map_f, CategoryTheory.Abelian.LeftResolution.karoubi.F_map_f, instFaithfulKaroubiToKaroubi, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, instFullKaroubiToKaroubi, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, Karoubi.decomp_p, functorExtension_obj_obj, instIsIdempotentCompleteKaroubi, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app, CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_p, CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiF, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ', Karoubi.id_f, FunctorExtension₁.obj_obj_p, KaroubiHomologicalComplexEquivalence.inverse_map, KaroubiHomologicalComplexEquivalence.Functor.map_f_f, Karoubi.comp_f, KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f, zero_def, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, instEssSurjKaroubiToKaroubiOfIsIdempotentComplete, KaroubiHomologicalComplexEquivalence.functor_obj, toKaroubi_map_f, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, karoubiFunctorCategoryEmbedding_obj, karoubiChainComplexEquivalence_functor_obj_d_f, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app, instAdditiveKaroubiToKaroubi, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, instFullKaroubiFunctorKaroubiFunctorCategoryEmbedding, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, CategoryTheory.Abelian.LeftResolution.karoubi_F, AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀, KaroubiKaroubi.equivalence_inverse, KaroubiKaroubi.equivalence_unitIso, KaroubiFunctorCategoryEmbedding.obj_obj_X, whiskeringLeft_obj_preimage_app, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπObjToKaroubi, AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom, functorExtension₂_obj_obj_X, KaroubiHomologicalComplexEquivalence.Inverse.obj_X_d, DoldKan.N_obj, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app, karoubiChainComplexEquivalence_inverse_obj_X_X, karoubiCochainComplexEquivalence_counitIso_hom, functorExtension₂_obj_obj_p, Karoubi.decompId, Karoubi.sum_hom, DoldKan.η_inv_app_f, KaroubiUniversal₁.counitIso_hom_app_app_f, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app, KaroubiUniversal₁.counitIso_inv_app_app_f, KaroubiKaroubi.inverse_map_f, karoubiCochainComplexEquivalence_functor_obj_X_p, karoubiCochainComplexEquivalence_inverse_map_f_f, AlgebraicTopology.DoldKan.N₁_obj_X, karoubiChainComplexEquivalence_inverse_map_f_f, Karoubi.retract_i_f, KaroubiFunctorCategoryEmbedding.obj_obj_p, Karoubi.decompId_i_toKaroubi, KaroubiKaroubi.idem_f, karoubiUniversal₁_counitIso, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app, FunctorExtension₁.obj_map_f, AlgebraicTopology.DoldKan.instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁, functorExtension₂CompWhiskeringLeftToKaroubiIso_inv_app_app_f, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ, Karoubi.Biproducts.bicone_pt_X, CategoryTheory.Preadditive.DoldKan.equivalence_inverse, Karoubi.zsmul_hom, AlgebraicTopology.DoldKan.N₂_obj_p_f, KaroubiHomologicalComplexEquivalence.Inverse.obj_X_X, Karoubi.decompId_assoc, KaroubiKaroubi.inverse_obj_p, KaroubiHomologicalComplexEquivalence.unitIso_hom_app_f_f, KaroubiKaroubi.unitIso_hom_app_f, AlgebraicTopology.DoldKan.N₂_obj_X_X, DoldKan.isoN₁_hom_app_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, karoubiCochainComplexEquivalence_functor_obj_d_f, natTrans_eq, functorExtension_obj_map, karoubiUniversal₁_unitIso, karoubiUniversal₂_functor_eq, karoubiFunctorCategoryEmbedding_map, karoubiChainComplexEquivalence_counitIso_inv, KaroubiHomologicalComplexEquivalence.inverse_obj, karoubiUniversal₁_inverse, AlgebraicTopology.DoldKan.N₂_obj_X_d, AlgebraicTopology.DoldKan.karoubi_PInfty_f, CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiFKaroubi, KaroubiHomologicalComplexEquivalence.Functor.obj_X_p, KaroubiKaroubi.counitIso_hom_app_f_f, instPreservesMonomorphismsKaroubiToKaroubi, KaroubiKaroubi.instAdditiveKaroubiInverse, KaroubiKaroubi.idem_f_assoc, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, karoubiCochainComplexEquivalence_inverse_obj_X_X, KaroubiKaroubi.equivalence_functor, karoubiChainComplexEquivalence_unitIso_inv_app_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, Karoubi.Biproducts.bicone_π_f, KaroubiKaroubi.inverse_obj_X, KaroubiKaroubi.unitIso_inv_app_f, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, karoubiHomologicalComplexEquivalence_counitIso, Karoubi.instHasBinaryBiproductComplement, instFaithfulKaroubiFunctorKaroubiFunctorCategoryEmbedding, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_X, Karoubi.decompId_p_toKaroubi, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, KaroubiKaroubi.equivalence.additive_functor, AlgebraicTopology.DoldKan.Γ₂_map_f_app, KaroubiHomologicalComplexEquivalence.counitIso_hom, KaroubiKaroubi.p_comm_f, FunctorExtension₁.map_app_f, CategoryTheory.Abelian.LeftResolution.karoubi.π'_app_f, karoubiCochainComplexEquivalence_counitIso_inv, AlgebraicTopology.DoldKan.Γ₂N₁_inv, KaroubiHomologicalComplexEquivalence.Functor.obj_d_f, AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂, KaroubiHomologicalComplexEquivalence.Functor.obj_X_X, toKaroubi_obj_X, AlgebraicTopology.DoldKan.identity_N₂_objectwise, DoldKan.hη, karoubiCochainComplexEquivalence_unitIso_inv_app_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_X, karoubiCochainComplexEquivalence_functor_obj_X_X, KaroubiHomologicalComplexEquivalence.functor_map, KaroubiKaroubi.p_comm_f_assoc, karoubiCochainComplexEquivalence_inverse_obj_X_d, AlgebraicTopology.DoldKan.N₂_map_f_f, Karoubi.decompId_i_naturality, Karoubi.Biproducts.bicone_pt_p, karoubiChainComplexEquivalence_unitIso_hom_app_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_app, DoldKan.N_map, instPreservesEpimorphismsKaroubiToKaroubi, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, functorExtension₁_obj, KaroubiFunctorCategoryEmbedding.map_app_f, toKaroubi_obj_p, AlgebraicTopology.DoldKan.Γ₂N₂_inv, DoldKan.η_hom_app_f, functorExtension₁_map, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app, karoubiChainComplexEquivalence_counitIso_hom
instAdd 📖	CompOp	1 math math: add_def
instAddCommGroupHom 📖	CompOp	3 math math: Karoubi.inclusionHom_apply, Karoubi.sum_hom, Karoubi.zsmul_hom
instNeg 📖	CompOp	1 math math: neg_def
instPreadditiveKaroubi 📖	CompOp	60 math math: Karoubi.karoubi_hasFiniteBiproducts, karoubiChainComplexEquivalence_inverse_obj_X_d, karoubiChainComplexEquivalence_functor_obj_X_X, KaroubiKaroubi.equivalence.additive_inverse, karoubiCochainComplexEquivalence_functor_map_f_f, KaroubiHomologicalComplexEquivalence.Inverse.map_f_f, karoubiHomologicalComplexEquivalence_functor, KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_f, karoubiCochainComplexEquivalence_inverse_obj_p_f, Karoubi.Biproducts.bicone_ι_f, karoubiChainComplexEquivalence_functor_obj_X_p, karoubiChainComplexEquivalence_inverse_obj_p_f, toKaroubiEquivalence_functor_additive, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, karoubiHomologicalComplexEquivalence_unitIso, karoubiHomologicalComplexEquivalence_inverse, KaroubiHomologicalComplexEquivalence.counitIso_inv, karoubiCochainComplexEquivalence_unitIso_hom_app_f_f, karoubiChainComplexEquivalence_functor_map_f_f, CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiF, KaroubiHomologicalComplexEquivalence.inverse_map, KaroubiHomologicalComplexEquivalence.Functor.map_f_f, KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f, KaroubiHomologicalComplexEquivalence.functor_obj, karoubiChainComplexEquivalence_functor_obj_d_f, instAdditiveKaroubiToKaroubi, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, KaroubiHomologicalComplexEquivalence.Inverse.obj_X_d, karoubiChainComplexEquivalence_inverse_obj_X_X, karoubiCochainComplexEquivalence_counitIso_hom, karoubiCochainComplexEquivalence_functor_obj_X_p, karoubiCochainComplexEquivalence_inverse_map_f_f, karoubiChainComplexEquivalence_inverse_map_f_f, Karoubi.Biproducts.bicone_pt_X, KaroubiHomologicalComplexEquivalence.Inverse.obj_X_X, KaroubiHomologicalComplexEquivalence.unitIso_hom_app_f_f, karoubiCochainComplexEquivalence_functor_obj_d_f, karoubiChainComplexEquivalence_counitIso_inv, KaroubiHomologicalComplexEquivalence.inverse_obj, AlgebraicTopology.DoldKan.karoubi_PInfty_f, CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiFKaroubi, KaroubiHomologicalComplexEquivalence.Functor.obj_X_p, KaroubiKaroubi.instAdditiveKaroubiInverse, karoubiCochainComplexEquivalence_inverse_obj_X_X, karoubiChainComplexEquivalence_unitIso_inv_app_f_f, Karoubi.Biproducts.bicone_π_f, karoubiHomologicalComplexEquivalence_counitIso, Karoubi.instHasBinaryBiproductComplement, KaroubiKaroubi.equivalence.additive_functor, KaroubiHomologicalComplexEquivalence.counitIso_hom, karoubiCochainComplexEquivalence_counitIso_inv, KaroubiHomologicalComplexEquivalence.Functor.obj_d_f, KaroubiHomologicalComplexEquivalence.Functor.obj_X_X, karoubiCochainComplexEquivalence_unitIso_inv_app_f_f, karoubiCochainComplexEquivalence_functor_obj_X_X, KaroubiHomologicalComplexEquivalence.functor_map, karoubiCochainComplexEquivalence_inverse_obj_X_d, Karoubi.Biproducts.bicone_pt_p, karoubiChainComplexEquivalence_unitIso_hom_app_f_f, karoubiChainComplexEquivalence_counitIso_hom
instZero 📖	CompOp	2 math math: Karoubi.hom_eq_zero_iff, zero_def
toKaroubi 📖	CompOp	63 math math: toKaroubi_comp_karoubiFunctorCategoryEmbedding, toKaroubi_isEquivalence, functorExtension₁CompWhiskeringLeftToKaroubiIso_inv_app_app_f, functorExtension₂_map_app_f, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app, instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi, AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans, CategoryTheory.Abelian.LeftResolution.karoubi.π_app_toKaroubi_obj, KaroubiKaroubi.counitIso_inv_app_f_f, Karoubi.retract_r_f, functorExtension₂CompWhiskeringLeftToKaroubiIso_hom_app_app_f, functorExtension₁CompWhiskeringLeftToKaroubiIso_hom_app_app_f, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, functorExtension₂_obj_map_f, instFaithfulKaroubiToKaroubi, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, instFullKaroubiToKaroubi, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, Karoubi.decomp_p, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ', SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, instEssSurjKaroubiToKaroubiOfIsIdempotentComplete, toKaroubi_map_f, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app, instAdditiveKaroubiToKaroubi, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀, whiskeringLeft_obj_preimage_app, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπObjToKaroubi, AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app, KaroubiUniversal₁.counitIso_hom_app_app_f, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app, KaroubiUniversal₁.counitIso_inv_app_app_f, Karoubi.retract_i_f, Karoubi.decompId_i_toKaroubi, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app, functorExtension₂CompWhiskeringLeftToKaroubiIso_inv_app_app_f, KaroubiKaroubi.unitIso_hom_app_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, karoubiUniversal₁_unitIso, karoubiUniversal₁_inverse, KaroubiKaroubi.counitIso_hom_app_f_f, instPreservesMonomorphismsKaroubiToKaroubi, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, KaroubiKaroubi.equivalence_functor, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, KaroubiKaroubi.unitIso_inv_app_f, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, Karoubi.decompId_p_toKaroubi, AlgebraicTopology.DoldKan.Γ₂_map_f_app, CategoryTheory.Abelian.LeftResolution.karoubi.π'_app_f, AlgebraicTopology.DoldKan.Γ₂N₁_inv, toKaroubi_obj_X, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_app, instPreservesEpimorphismsKaroubiToKaroubi, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, toKaroubi_obj_p, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app
toKaroubiEquivalence 📖	CompOp	14 math math: functorExtension_map_app, toKaroubiEquivalence_functor_additive, DoldKan.hε, DoldKan.N₂_map_isoΓ₀_hom_app_f, functorExtension_obj_obj, DoldKan.N_obj, DoldKan.η_inv_app_f, DoldKan.isoN₁_hom_app_f, functorExtension_obj_map, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, DoldKan.hη, DoldKan.N_map, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, DoldKan.η_hom_app_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_def 📖	mathematical	—	Quiver.Hom Karoubi CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Karoubi.instCategory instAdd Karoubi.X AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup Karoubi.Hom.f	—	—
instAdditiveKaroubiToKaroubi 📖	mathematical	—	CategoryTheory.Functor.Additive Karoubi Karoubi.instCategory instPreadditiveKaroubi toKaroubi	—	—
instEssSurjKaroubiToKaroubiOfIsIdempotentComplete 📖	mathematical	—	CategoryTheory.Functor.EssSurj Karoubi Karoubi.instCategory toKaroubi	—	CategoryTheory.IsIdempotentComplete.idempotents_split Karoubi.idem CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Category.assoc
instFaithfulKaroubiToKaroubi 📖	mathematical	—	CategoryTheory.Functor.Faithful Karoubi Karoubi.instCategory toKaroubi	—	—
instFullKaroubiToKaroubi 📖	mathematical	—	CategoryTheory.Functor.Full Karoubi Karoubi.instCategory toKaroubi	—	—
instIsIdempotentCompleteKaroubi 📖	mathematical	—	CategoryTheory.IsIdempotentComplete Karoubi Karoubi.instCategory	—	Karoubi.comp_p Karoubi.p_comp
instPreservesEpimorphismsKaroubiToKaroubi 📖	mathematical	—	CategoryTheory.Functor.PreservesEpimorphisms Karoubi Karoubi.instCategory toKaroubi	—	Karoubi.hom_ext CategoryTheory.cancel_epi
instPreservesMonomorphismsKaroubiToKaroubi 📖	mathematical	—	CategoryTheory.Functor.PreservesMonomorphisms Karoubi Karoubi.instCategory toKaroubi	—	Karoubi.hom_ext CategoryTheory.cancel_mono
neg_def 📖	mathematical	—	Quiver.Hom Karoubi CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Karoubi.instCategory instNeg Karoubi.X NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid CategoryTheory.Preadditive.homGroup Karoubi.Hom.f	—	—
toKaroubiEquivalence_functor_additive 📖	mathematical	—	CategoryTheory.Functor.Additive Karoubi Karoubi.instCategory instPreadditiveKaroubi CategoryTheory.Equivalence.functor toKaroubiEquivalence	—	instAdditiveKaroubiToKaroubi
toKaroubi_isEquivalence 📖	mathematical	—	CategoryTheory.Functor.IsEquivalence Karoubi Karoubi.instCategory toKaroubi	—	instFaithfulKaroubiToKaroubi instFullKaroubiToKaroubi instEssSurjKaroubiToKaroubiOfIsIdempotentComplete
toKaroubi_map_f 📖	mathematical	—	Karoubi.Hom.f CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map Karoubi Karoubi.instCategory toKaroubi	—	—
toKaroubi_obj_X 📖	mathematical	—	Karoubi.X CategoryTheory.Functor.obj Karoubi Karoubi.instCategory toKaroubi	—	—
toKaroubi_obj_p 📖	mathematical	—	Karoubi.p CategoryTheory.Functor.obj Karoubi Karoubi.instCategory toKaroubi CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
zero_def 📖	mathematical	—	Quiver.Hom Karoubi CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Karoubi.instCategory instZero Karoubi.X CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—

CategoryTheory.Idempotents.Karoubi

Definitions

Name	Category	Theorems
X 📖	CompOp	138 math math: CategoryTheory.Idempotents.app_idem_assoc, CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_map_f, CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_p, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d, AlgebraicTopology.DoldKan.N₁_map_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_X, CategoryTheory.Idempotents.neg_def, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map_f_f, CategoryTheory.Idempotents.functorExtension₂_map_app_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_f, CategoryTheory.Abelian.LeftResolution.karoubi.F'_map_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f, HomologicalComplex.comp_p_d, idem_assoc, Biproducts.bicone_ι_f, CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_inv_app_f_f, CategoryTheory.Idempotents.app_p_comp, CategoryTheory.Idempotents.add_def, comp_p, CategoryTheory.Idempotents.app_p_comm, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p, decompId_p_naturality, hom_eq_zero_iff, HomologicalComplex.p_comm_f_assoc, inclusionHom_apply, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f, eqToHom_f, retract_r_f, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, HomologicalComplex.p_comp_d_assoc, HomologicalComplex.comp_p_d_assoc, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, CategoryTheory.Idempotents.FunctorExtension₁.obj_obj_X, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f, CategoryTheory.Idempotents.functorExtension₂_obj_map_f, CategoryTheory.Abelian.LeftResolution.karoubi.F_map_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, decomp_p, CategoryTheory.Idempotents.FunctorExtension₁.obj_obj_p, p_comm_assoc, CategoryTheory.Idempotents.app_p_comp_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map_f_f, comp_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f, CategoryTheory.Idempotents.zero_def, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app, decompId_i_f, p_comp, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, comp_proof, CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_obj_X, Hom.comm, CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app, CategoryTheory.Idempotents.functorExtension₂_obj_obj_X, CategoryTheory.Idempotents.app_p_comm_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_d, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_X, HomologicalComplex.p_idem, CategoryTheory.Idempotents.functorExtension₂_obj_obj_p, decompId, sum_hom, CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_hom_app_app_f, CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_inv_app_app_f, HomologicalComplex.p_comp_d, CategoryTheory.Idempotents.KaroubiKaroubi.inverse_map_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f, AlgebraicTopology.DoldKan.N₁_obj_X, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f, retract_i_f, CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_obj_p, CategoryTheory.Idempotents.KaroubiKaroubi.idem_f, p_comp_assoc, CategoryTheory.Idempotents.FunctorExtension₁.obj_map_f, CategoryTheory.Idempotents.app_comp_p, Biproducts.bicone_pt_X, complement_p, HomologicalComplex.p_idem_assoc, zsmul_hom, idem, AlgebraicTopology.DoldKan.N₂_obj_p_f, CategoryTheory.Idempotents.app_comp_p_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_X, decompId_assoc, CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_p, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_hom_app_f_f, AlgebraicTopology.DoldKan.N₂_obj_X_X, CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f, CategoryTheory.Idempotents.natTrans_eq, AlgebraicTopology.DoldKan.N₂_obj_X_d, coe_X, AlgebraicTopology.DoldKan.karoubi_PInfty_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_p, CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_hom_app_f_f, CategoryTheory.Idempotents.KaroubiKaroubi.idem_f_assoc, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_X, HomologicalComplex.p_comm_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f, decompId_p_f, Biproducts.bicone_π_f, CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_X, complement_X, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_X, decompId_p_toKaroubi, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, comp_p_assoc, AlgebraicTopology.DoldKan.Γ₂_map_f_app, CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f, CategoryTheory.Idempotents.FunctorExtension₁.map_app_f, CategoryTheory.Idempotents.app_idem, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_d_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_X, CategoryTheory.Idempotents.toKaroubi_obj_X, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_X, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_X, CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d, AlgebraicTopology.DoldKan.N₂_map_f_f, decompId_i_naturality, Biproducts.bicone_pt_p, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map_app_f, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app, p_comm
decompId_i 📖	CompOp	10 math math: decomp_p, decompId_i_f, CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app, decompId, CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_inv_app_app_f, decompId_i_toKaroubi, decompId_assoc, CategoryTheory.Idempotents.natTrans_eq, decompId_i_naturality, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app
decompId_p 📖	CompOp	10 math math: decompId_p_naturality, decomp_p, CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app, decompId, CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_hom_app_app_f, decompId_assoc, CategoryTheory.Idempotents.natTrans_eq, decompId_p_f, decompId_p_toKaroubi, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app
inclusionHom 📖	CompOp	1 math math: inclusionHom_apply
instCategory 📖	CompOp	210 math math: CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_map_f, karoubi_hasFiniteBiproducts, CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_p, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d, CategoryTheory.Idempotents.toKaroubi_comp_karoubiFunctorCategoryEmbedding, CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_counitIso, AlgebraicTopology.DoldKan.N₁_map_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_X, CategoryTheory.Idempotents.neg_def, CategoryTheory.Idempotents.toKaroubi_isEquivalence, CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiFunctorExtension₂, CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_inverse, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f, CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso_inv_app_app_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map_f_f, CategoryTheory.Idempotents.functorExtension₂_map_app_f, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app, AlgebraicTopology.DoldKan.identity_N₂, CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_functor, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_f, CategoryTheory.Preadditive.DoldKan.equivalence_unitIso, AlgebraicTopology.DoldKan.instIsIsoFunctorSimplicialObjectKaroubiNatTrans, CategoryTheory.Abelian.LeftResolution.karoubi.π_app_toKaroubi_obj, CategoryTheory.Abelian.LeftResolution.karoubi.F'_map_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f, CategoryTheory.Preadditive.DoldKan.equivalence_functor, CategoryTheory.Idempotents.karoubiUniversal_functor_eq, CategoryTheory.Idempotents.functorExtension_map_app, Biproducts.bicone_ι_f, CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_inv_app_f_f, CategoryTheory.Idempotents.add_def, CategoryTheory.Idempotents.karoubiUniversal₁_functor, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p, decompId_p_naturality, AlgebraicTopology.DoldKan.instIsIsoFunctorKaroubiSimplicialObjectNatTrans, hom_eq_zero_iff, AlgebraicTopology.DoldKan.N₁_obj_p, CategoryTheory.Preadditive.DoldKan.equivalence_counitIso, inclusionHom_apply, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f, eqToHom_f, CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiFunctorExtension, CategoryTheory.Idempotents.toKaroubiEquivalence_functor_additive, retract_r_f, CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso_hom_app_app_f, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, CategoryTheory.Abelian.LeftResolution.karoubi_π, CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso_hom_app_app_f, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_unitIso, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_inverse, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_inv, CategoryTheory.Idempotents.DoldKan.hε, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, CategoryTheory.Idempotents.FunctorExtension₁.obj_obj_X, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f, CategoryTheory.Idempotents.functorExtension₂_obj_map_f, CategoryTheory.Abelian.LeftResolution.karoubi.F_map_f, CategoryTheory.Idempotents.instFaithfulKaroubiToKaroubi, AlgebraicTopology.DoldKan.compatibility_Γ₂N₁_Γ₂N₂_natTrans, CategoryTheory.Idempotents.instFullKaroubiToKaroubi, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, decomp_p, CategoryTheory.Idempotents.functorExtension_obj_obj, CategoryTheory.Idempotents.instIsIdempotentCompleteKaroubi, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_hom_app, CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_p, CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiF, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ', id_f, CategoryTheory.Idempotents.FunctorExtension₁.obj_obj_p, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse_map, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map_f_f, comp_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f, CategoryTheory.Idempotents.zero_def, AlgebraicTopology.DoldKan.Γ₂_obj_X_map, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, CategoryTheory.Idempotents.instEssSurjKaroubiToKaroubiOfIsIdempotentComplete, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor_obj, CategoryTheory.Idempotents.toKaroubi_map_f, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding_obj, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app, CategoryTheory.Idempotents.instAdditiveKaroubiToKaroubi, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, CategoryTheory.Idempotents.instFullKaroubiFunctorKaroubiFunctorCategoryEmbedding, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, CategoryTheory.Abelian.LeftResolution.karoubi_F, AlgebraicTopology.DoldKan.N₂Γ₂_compatible_with_N₁Γ₀, CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_inverse, CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_unitIso, CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_obj_X, CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπObjToKaroubi, AlgebraicTopology.DoldKan.whiskerLeft_toKaroubi_N₂Γ₂_hom, CategoryTheory.Idempotents.functorExtension₂_obj_obj_X, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_d, CategoryTheory.Idempotents.DoldKan.N_obj, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_X, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_hom, CategoryTheory.Idempotents.functorExtension₂_obj_obj_p, decompId, sum_hom, CategoryTheory.Idempotents.DoldKan.η_inv_app_f, CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_hom_app_app_f, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app, CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_inv_app_app_f, CategoryTheory.Idempotents.KaroubiKaroubi.inverse_map_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f, AlgebraicTopology.DoldKan.N₁_obj_X, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f, retract_i_f, CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_obj_p, decompId_i_toKaroubi, CategoryTheory.Idempotents.KaroubiKaroubi.idem_f, CategoryTheory.Idempotents.karoubiUniversal₁_counitIso, AlgebraicTopology.DoldKan.Γ₂N₂ToKaroubiIso_inv_app, CategoryTheory.Idempotents.FunctorExtension₁.obj_map_f, AlgebraicTopology.DoldKan.instReflectsIsomorphismsSimplicialObjectKaroubiChainComplexNatN₁, CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso_inv_app_app_f, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ, Biproducts.bicone_pt_X, CategoryTheory.Preadditive.DoldKan.equivalence_inverse, zsmul_hom, AlgebraicTopology.DoldKan.N₂_obj_p_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_X, decompId_assoc, CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_p, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_hom_app_f_f, CategoryTheory.Idempotents.KaroubiKaroubi.unitIso_hom_app_f, AlgebraicTopology.DoldKan.N₂_obj_X_X, CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f, CategoryTheory.Idempotents.natTrans_eq, CategoryTheory.Idempotents.functorExtension_obj_map, CategoryTheory.Idempotents.karoubiUniversal₁_unitIso, CategoryTheory.Idempotents.karoubiUniversal₂_functor_eq, CategoryTheory.Idempotents.karoubiFunctorCategoryEmbedding_map, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_inv, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse_obj, CategoryTheory.Idempotents.karoubiUniversal₁_inverse, AlgebraicTopology.DoldKan.N₂_obj_X_d, AlgebraicTopology.DoldKan.karoubi_PInfty_f, CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiFKaroubi, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_p, CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_hom_app_f_f, CategoryTheory.Idempotents.instPreservesMonomorphismsKaroubiToKaroubi, CategoryTheory.Idempotents.KaroubiKaroubi.instAdditiveKaroubiInverse, CategoryTheory.Idempotents.KaroubiKaroubi.idem_f_assoc, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_X, CategoryTheory.Idempotents.KaroubiKaroubi.equivalence_functor, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app, Biproducts.bicone_π_f, CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_X, CategoryTheory.Idempotents.KaroubiKaroubi.unitIso_inv_app_f, CategoryTheory.Abelian.DoldKan.comparisonN_hom_app_f, CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_counitIso, instHasBinaryBiproductComplement, CategoryTheory.Idempotents.instFaithfulKaroubiFunctorKaroubiFunctorCategoryEmbedding, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_X, decompId_p_toKaroubi, AlgebraicTopology.DoldKan.Γ₂_obj_X_obj, CategoryTheory.Idempotents.KaroubiKaroubi.equivalence.additive_functor, AlgebraicTopology.DoldKan.Γ₂_map_f_app, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_hom, CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f, CategoryTheory.Idempotents.FunctorExtension₁.map_app_f, CategoryTheory.Abelian.LeftResolution.karoubi.π'_app_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_inv, AlgebraicTopology.DoldKan.Γ₂N₁_inv, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_d_f, AlgebraicTopology.DoldKan.instReflectsIsomorphismsKaroubiSimplicialObjectChainComplexNatN₂, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_X, CategoryTheory.Idempotents.toKaroubi_obj_X, AlgebraicTopology.DoldKan.identity_N₂_objectwise, CategoryTheory.Idempotents.DoldKan.hη, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_X, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_X, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor_map, CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d, AlgebraicTopology.DoldKan.N₂_map_f_f, decompId_i_naturality, Biproducts.bicone_pt_p, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_app, CategoryTheory.Idempotents.DoldKan.N_map, CategoryTheory.Idempotents.instPreservesEpimorphismsKaroubiToKaroubi, CategoryTheory.Abelian.DoldKan.comparisonN_inv_app_f, CategoryTheory.Idempotents.functorExtension₁_obj, CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map_app_f, CategoryTheory.Idempotents.toKaroubi_obj_p, AlgebraicTopology.DoldKan.Γ₂N₂_inv, CategoryTheory.Idempotents.DoldKan.η_hom_app_f, CategoryTheory.Idempotents.functorExtension₁_map, AlgebraicTopology.DoldKan.Γ₂N₂.natTrans_app_f_app, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_hom
instInhabitedHomOfPreadditive 📖	CompOp	—
p 📖	CompOp	85 math math: CategoryTheory.Idempotents.app_idem_assoc, CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_map_f, CategoryTheory.Abelian.LeftResolution.karoubi.F_obj_p, CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso_inv_app_app_f, CategoryTheory.Idempotents.functorExtension₂_map_app_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f, HomologicalComplex.comp_p_d, idem_assoc, Biproducts.bicone_ι_f, CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_inv_app_f_f, CategoryTheory.Idempotents.app_p_comp, comp_p, CategoryTheory.Idempotents.app_p_comm, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p, AlgebraicTopology.DoldKan.N₁_obj_p, HomologicalComplex.p_comm_f_assoc, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f, eqToHom_f, retract_r_f, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso_hom_app_app_f, HomologicalComplex.p_comp_d_assoc, HomologicalComplex.comp_p_d_assoc, AlgebraicTopology.DoldKan.Γ₂_obj_p_app, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.Idempotents.functorExtension₂_obj_map_f, CategoryTheory.Abelian.LeftResolution.karoubi.F_map_f, decomp_p, CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_p, id_f, CategoryTheory.Idempotents.FunctorExtension₁.obj_obj_p, p_comm_assoc, CategoryTheory.Idempotents.app_p_comp_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f, decompId_i_f, p_comp, comp_proof, Hom.comm, CategoryTheory.Idempotents.app_p_comm_assoc, HomologicalComplex.p_idem, CategoryTheory.Idempotents.functorExtension₂_obj_obj_p, HomologicalComplex.p_comp_d, coe_p, CategoryTheory.Idempotents.KaroubiKaroubi.inverse_map_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p, retract_i_f, CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_obj_p, CategoryTheory.Idempotents.KaroubiKaroubi.idem_f, p_comp_assoc, CategoryTheory.Idempotents.FunctorExtension₁.obj_map_f, CategoryTheory.Idempotents.app_comp_p, complement_p, HomologicalComplex.p_idem_assoc, idem, AlgebraicTopology.DoldKan.N₂_obj_p_f, CategoryTheory.Idempotents.app_comp_p_assoc, CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_p, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_hom_app_f_f, CategoryTheory.Idempotents.KaroubiKaroubi.unitIso_hom_app_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f, AlgebraicTopology.DoldKan.karoubi_PInfty_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_p, CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_hom_app_f_f, CategoryTheory.Idempotents.KaroubiKaroubi.idem_f_assoc, HomologicalComplex.p_comm_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f, decompId_p_f, Biproducts.bicone_π_f, CategoryTheory.Idempotents.KaroubiKaroubi.unitIso_inv_app_f, comp_p_assoc, AlgebraicTopology.DoldKan.Γ₂_map_f_app, CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f, CategoryTheory.Idempotents.FunctorExtension₁.map_app_f, CategoryTheory.Idempotents.app_idem, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_d_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f, CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f_assoc, AlgebraicTopology.DoldKan.N₂_map_f_f, Biproducts.bicone_pt_p, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.Idempotents.toKaroubi_obj_p, p_comm
retract 📖	CompOp	2 math math: retract_r_f, retract_i_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_X 📖	mathematical	—	X CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
coe_p 📖	mathematical	—	p CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
comp_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.comp CategoryTheory.Idempotents.Karoubi CategoryTheory.Category.toCategoryStruct instCategory X	—	—
comp_p 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.f p	—	Hom.comm CategoryTheory.Category.assoc idem
comp_p_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X Hom.f p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' comp_p
comp_proof 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X p Hom.f	—	CategoryTheory.Category.assoc comp_p p_comp_assoc
decompId 📖	mathematical	—	CategoryTheory.CategoryStruct.id CategoryTheory.Idempotents.Karoubi CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.CategoryStruct.comp X decompId_i decompId_p	—	hom_ext idem
decompId_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Idempotents.Karoubi CategoryTheory.Category.toCategoryStruct instCategory X CategoryTheory.CategoryStruct.id decompId_i decompId_p	—	CategoryTheory.Category.id_comp CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' decompId
decompId_i_f 📖	mathematical	—	Hom.f X CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct decompId_i p	—	—
decompId_i_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Idempotents.Karoubi CategoryTheory.Category.toCategoryStruct instCategory X CategoryTheory.CategoryStruct.id decompId_i Hom.f	—	comp_p p_comp
decompId_i_toKaroubi 📖	mathematical	—	decompId_i CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi instCategory CategoryTheory.Idempotents.toKaroubi CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
decompId_p_f 📖	mathematical	—	Hom.f X CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct decompId_p p	—	—
decompId_p_naturality 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Idempotents.Karoubi CategoryTheory.Category.toCategoryStruct instCategory X CategoryTheory.CategoryStruct.id decompId_p Hom.f	—	p_comp comp_p
decompId_p_toKaroubi 📖	mathematical	—	decompId_p CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi instCategory CategoryTheory.Idempotents.toKaroubi CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct X	—	—
decomp_p 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.Idempotents.Karoubi instCategory CategoryTheory.Idempotents.toKaroubi X p CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id decompId_p decompId_i	—	hom_ext idem
eqToHom_f 📖	mathematical	—	Hom.f CategoryTheory.eqToHom CategoryTheory.Idempotents.Karoubi CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.CategoryStruct.comp X p	—	CategoryTheory.Category.comp_id
ext 📖	—	X CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct p CategoryTheory.eqToHom	—	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp
hom_eq_zero_iff 📖	mathematical	—	Quiver.Hom CategoryTheory.Idempotents.Karoubi CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Idempotents.instZero Hom.f X CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	hom_ext_iff
hom_ext 📖	—	Hom.f	—	—	—
hom_ext_iff 📖	mathematical	—	Hom.f	—	Hom.ext
id_f 📖	mathematical	—	Hom.f CategoryTheory.CategoryStruct.id CategoryTheory.Idempotents.Karoubi CategoryTheory.Category.toCategoryStruct instCategory p	—	—
idem 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X p	—	—
idem_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' idem
inclusionHom_apply 📖	mathematical	—	DFunLike.coe AddMonoidHom Quiver.Hom CategoryTheory.Idempotents.Karoubi CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory X AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Idempotents.instAddCommGroupHom CategoryTheory.Preadditive.homGroup AddMonoidHom.instFunLike inclusionHom Hom.f	—	—
p_comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X p Hom.f	—	p_comp comp_p
p_comm_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X p Hom.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_comm
p_comp 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X p Hom.f	—	Hom.comm CategoryTheory.Category.assoc idem
p_comp_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X p Hom.f	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_comp
retract_i_f 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi instCategory CategoryTheory.Idempotents.toKaroubi X CategoryTheory.Retract.i retract p	—	—
retract_r_f 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi instCategory CategoryTheory.Idempotents.toKaroubi X CategoryTheory.Retract.r retract p	—	—
sum_hom 📖	mathematical	—	Hom.f Finset.sum Quiver.Hom CategoryTheory.Idempotents.Karoubi CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory AddCommGroup.toAddCommMonoid CategoryTheory.Idempotents.instAddCommGroupHom X CategoryTheory.Preadditive.homGroup	—	map_sum AddMonoidHom.instAddMonoidHomClass
zsmul_hom 📖	mathematical	—	Hom.f Quiver.Hom CategoryTheory.Idempotents.Karoubi CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Idempotents.instAddCommGroupHom X CategoryTheory.Preadditive.homGroup	—	map_zsmul AddMonoidHom.instAddMonoidHomClass

CategoryTheory.Idempotents.Karoubi.Hom

Definitions

Name	Category	Theorems
f 📖	CompOp	106 math math: CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.obj_map_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d, AlgebraicTopology.DoldKan.N₁_map_f, CategoryTheory.Idempotents.neg_def, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f, CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso_inv_app_app_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map_f_f, CategoryTheory.Idempotents.functorExtension₂_map_app_f, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_inv_app, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_f, CategoryTheory.Abelian.LeftResolution.karoubi.F'_map_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d, CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_ι_f, CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_inv_app_f_f, CategoryTheory.Idempotents.app_p_comp, CategoryTheory.Idempotents.add_def, CategoryTheory.Idempotents.Karoubi.comp_p, CategoryTheory.Idempotents.app_p_comm, CategoryTheory.Idempotents.Karoubi.decompId_p_naturality, CategoryTheory.Idempotents.Karoubi.hom_eq_zero_iff, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f_assoc, CategoryTheory.Idempotents.Karoubi.inclusionHom_apply, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f, CategoryTheory.Idempotents.Karoubi.eqToHom_f, CategoryTheory.Idempotents.Karoubi.retract_r_f, CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso_hom_app_app_f, ext_iff, AlgebraicTopology.karoubi_alternatingFaceMapComplex_d, CategoryTheory.Idempotents.functorExtension₁CompWhiskeringLeftToKaroubiIso_hom_app_app_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d_assoc, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d_assoc, CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f, CategoryTheory.Idempotents.functorExtension₂_obj_map_f, CategoryTheory.Abelian.LeftResolution.karoubi.F_map_f, AlgebraicTopology.DoldKan.N₁Γ₀_hom_app_f_f, CategoryTheory.Idempotents.Karoubi.id_f, CategoryTheory.Idempotents.FunctorExtension₁.obj_obj_p, CategoryTheory.Idempotents.Karoubi.p_comm_assoc, CategoryTheory.Idempotents.app_p_comp_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map_f_f, CategoryTheory.Idempotents.Karoubi.comp_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_inv_f_f, CategoryTheory.Idempotents.toKaroubi_map_f, AlgebraicTopology.DoldKan.N₂Γ₂_inv_app_f_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f, AlgebraicTopology.DoldKan.N₂Γ₂ToKaroubiIso_hom_app, CategoryTheory.Idempotents.Karoubi.decompId_i_f, CategoryTheory.Idempotents.Karoubi.p_comp, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_hom_app_f_f, CategoryTheory.Idempotents.Karoubi.comp_proof, comm, CategoryTheory.Idempotents.app_p_comm_assoc, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_d, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_hom_app, CategoryTheory.Idempotents.Karoubi.sum_hom, CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_hom_app_app_f, AlgebraicTopology.DoldKan.toKaroubiCompN₂IsoN₁_inv_app, CategoryTheory.Idempotents.KaroubiUniversal₁.counitIso_inv_app_app_f, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d, CategoryTheory.Idempotents.KaroubiKaroubi.inverse_map_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f, CategoryTheory.Idempotents.Karoubi.retract_i_f, CategoryTheory.Idempotents.KaroubiKaroubi.idem_f, CategoryTheory.Idempotents.Karoubi.p_comp_assoc, CategoryTheory.Idempotents.FunctorExtension₁.obj_map_f, CategoryTheory.Idempotents.app_comp_p, CategoryTheory.Idempotents.functorExtension₂CompWhiskeringLeftToKaroubiIso_inv_app_app_f, CategoryTheory.Idempotents.Karoubi.zsmul_hom, CategoryTheory.Idempotents.app_comp_p_assoc, CategoryTheory.Idempotents.KaroubiKaroubi.inverse_obj_p, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_hom_app_f_f, CategoryTheory.Idempotents.KaroubiKaroubi.unitIso_hom_app_f, CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f, AlgebraicTopology.DoldKan.karoubi_PInfty_f, CategoryTheory.Idempotents.KaroubiKaroubi.counitIso_hom_app_f_f, CategoryTheory.Idempotents.KaroubiKaroubi.idem_f_assoc, AlgebraicTopology.DoldKan.Γ₂N₁.natTrans_app_f_app, CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f, CategoryTheory.Idempotents.Karoubi.decompId_p_f, CategoryTheory.Idempotents.Karoubi.Biproducts.bicone_π_f, CategoryTheory.Idempotents.KaroubiKaroubi.unitIso_inv_app_f, SimplicialObject.Split.toKaroubiNondegComplexFunctorIsoN₁_inv_app_f_f, CategoryTheory.Idempotents.Karoubi.comp_p_assoc, AlgebraicTopology.DoldKan.Γ₂_map_f_app, CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f, CategoryTheory.Idempotents.FunctorExtension₁.map_app_f, CategoryTheory.Abelian.LeftResolution.karoubi.π'_app_f, CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_d_f, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f, AlgebraicTopology.DoldKan.N₁Γ₀_inv_app_f_f, SimplicialObject.Splitting.toKaroubiNondegComplexIsoN₁_hom_f_f, CategoryTheory.Idempotents.KaroubiKaroubi.p_comm_f_assoc, CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d, AlgebraicTopology.DoldKan.N₂_map_f_f, CategoryTheory.Idempotents.Karoubi.decompId_i_naturality, CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f, CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map_app_f, CategoryTheory.Idempotents.Karoubi.hom_ext_iff, CategoryTheory.Idempotents.Karoubi.p_comm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comm 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Idempotents.Karoubi.p f	—	—
ext 📖	—	f	—	—	—
ext_iff 📖	mathematical	—	f	—	ext

---

← Back to Index