Structures · Category theory
CategoryTheory.IsIdempotentComplete
A category is idempotent complete iff all idempotent endomorphisms p
split as a composition p = e ≫ i with i ≫ e = 𝟙 _
- Defined in
- Mathlib.CategoryTheory.Idempotents.Basic
- Shape
- One type argument · adds idempotents_split
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- CategoryTheory.Functor
- HomologicalComplex
- CategoryTheory.Idempotents.Karoubi
- CategoryTheory.CosimplicialObject
- CategoryTheory.SimplicialObject
- Opposite
How is a type an instance?
Loading the hierarchy index…
Assumed by47
- CategoryTheory.Idempotents.toKaroubiEquivalence
- CategoryTheory.Idempotents.DoldKan.Γ
- CategoryTheory.Idempotents.DoldKan.N
- CategoryTheory.Idempotents.DoldKan.equivalence
- CategoryTheory.Idempotents.functorExtension
- CategoryTheory.Idempotents.DoldKan.isoN₁
- CategoryTheory.IsIdempotentComplete.idempotents_split
- CategoryTheory.Idempotents.DoldKan.η
- CategoryTheory.Idempotents.DoldKan.isoΓ₀
- CategoryTheory.Idempotents.whiskeringLeft_obj_preimage_app
- CategoryTheory.Idempotents.DoldKan.hη
- CategoryTheory.Idempotents.karoubiUniversal
- CategoryTheory.Idempotents.DoldKan.ε
- CategoryTheory.Idempotents.DoldKan.N₂_map_isoΓ₀_hom_app_f
- CategoryTheory.Idempotents.karoubiUniversal₂
- CategoryTheory.Idempotents.DoldKan.hε
- CategoryTheory.Idempotents.DoldKan.Γ_obj_map
- CategoryTheory.Idempotents.instIsIdempotentCompleteSimplicialObject
- CategoryTheory.Idempotents.DoldKan.η_hom_app_f
- CategoryTheory.Idempotents.functorExtension_map_app
- CategoryTheory.Idempotents.instEssSurjKaroubiToKaroubiOfIsIdempotentComplete
- CategoryTheory.Idempotents.instIsIdempotentCompleteOpposite
- CategoryTheory.Idempotents.functorExtension_obj_map
- CategoryTheory.Idempotents.DoldKan.η_inv_app_f
- CategoryTheory.Idempotents.toKaroubi_isEquivalence
- CategoryTheory.Idempotents.functorExtension_obj_obj
- CategoryTheory.Idempotents.DoldKan.equivalence_inverse
- CategoryTheory.Idempotents.toKaroubiEquivalence.congr_simp
- CategoryTheory.Idempotents.DoldKan.N_map
- CategoryTheory.Idempotents.instIsIdempotentCompleteHomologicalComplex
- CategoryTheory.Idempotents.instIsIdempotentCompleteCosimplicialObject
- CategoryTheory.Idempotents.DoldKan.isoN₁_hom_app_f
- CategoryTheory.Idempotents.karoubiUniversal_functor_eq
- CategoryTheory.Idempotents.DoldKan.equivalence_functor
- CategoryTheory.Idempotents.DoldKan.Γ_obj_obj
- CategoryTheory.Idempotents.DoldKan.N_obj
- CategoryTheory.Idempotents.karoubiUniversal₂_functor_eq
- CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiObjWhiskeringLeftToKaroubi
- CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiFunctorExtension
- CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsFReduced
- CategoryTheory.Idempotents.functor_category_isIdempotentComplete
- CategoryTheory.Idempotents.DoldKan.equivalence_unitIso
- CategoryTheory.Idempotents.DoldKan.equivalence_counitIso
- CategoryTheory.Idempotents.toKaroubiEquivalence_functor_additive
- CategoryTheory.Idempotents.DoldKan.Γ_map_app
- CategoryTheory.Abelian.LeftResolution.reduced
- CategoryTheory.Idempotents.instIsEquivalenceFunctorKaroubiFunctorExtension₂
Ancestors0
No ancestors.