Basic

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

Statistics

Metric	Count
Definitions IsIdempotentComplete	1
Theorems isIdempotentComplete, idem_of_id_sub_idem, instIsIdempotentCompleteOpposite, isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent, isIdempotentComplete_iff_idempotents_have_kernels, isIdempotentComplete_iff_of_equivalence, isIdempotentComplete_iff_opposite, isIdempotentComplete_of_abelian, isIdempotentComplete_of_isIdempotentComplete_opposite, split_iff_of_iso, split_imp_of_iso, idempotents_split	12
Total	13

CategoryTheory

Definitions

Name	Category	Theorems
IsIdempotentComplete 📖	CompData	13 math math: Idempotents.instIsIdempotentCompleteCosimplicialObject, Idempotents.Equivalence.isIdempotentComplete, Idempotents.instIsIdempotentCompleteHomologicalComplex, Idempotents.isIdempotentComplete_iff_of_equivalence, Idempotents.instIsIdempotentCompleteSimplicialObject, Idempotents.instIsIdempotentCompleteKaroubi, Idempotents.isIdempotentComplete_of_isIdempotentComplete_opposite, Idempotents.isIdempotentComplete_iff_opposite, Idempotents.isIdempotentComplete_of_abelian, Idempotents.isIdempotentComplete_iff_idempotents_have_kernels, Idempotents.isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent, Idempotents.instIsIdempotentCompleteOpposite, Idempotents.functor_category_isIdempotentComplete

CategoryTheory.Idempotents

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
idem_of_id_sub_idem 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	Quiver.Hom CategoryTheory.CategoryStruct.toQuiver SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.id	—	CategoryTheory.Preadditive.comp_sub CategoryTheory.Category.comp_id CategoryTheory.Preadditive.sub_comp CategoryTheory.Category.id_comp sub_self sub_zero
instIsIdempotentCompleteOpposite 📖	mathematical	—	CategoryTheory.IsIdempotentComplete Opposite CategoryTheory.Category.opposite	—	isIdempotentComplete_iff_opposite
isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent 📖	mathematical	—	CategoryTheory.IsIdempotentComplete CategoryTheory.Limits.HasEqualizer CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.IsIdempotentComplete.idempotents_split CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.Limits.Fork.condition CategoryTheory.Limits.Fork.ι_ofι CategoryTheory.Limits.equalizer.hom_ext CategoryTheory.Limits.limit.lift_π CategoryTheory.Limits.equalizer.condition CategoryTheory.Limits.equalizer.lift_ι
isIdempotentComplete_iff_idempotents_have_kernels 📖	mathematical	—	CategoryTheory.IsIdempotentComplete CategoryTheory.Limits.HasKernel CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent sub_sub_cancel CategoryTheory.Preadditive.hasKernel_of_hasEqualizer idem_of_id_sub_idem CategoryTheory.Preadditive.hasEqualizer_of_hasKernel
isIdempotentComplete_iff_of_equivalence 📖	mathematical	—	CategoryTheory.IsIdempotentComplete	—	Equivalence.isIdempotentComplete
isIdempotentComplete_iff_opposite 📖	mathematical	—	CategoryTheory.IsIdempotentComplete Opposite CategoryTheory.Category.opposite	—	isIdempotentComplete_of_isIdempotentComplete_opposite isIdempotentComplete_iff_of_equivalence
isIdempotentComplete_of_abelian 📖	mathematical	—	CategoryTheory.IsIdempotentComplete	—	isIdempotentComplete_iff_idempotents_have_kernels CategoryTheory.Limits.HasKernels.has_limit CategoryTheory.Abelian.has_kernels
isIdempotentComplete_of_isIdempotentComplete_opposite 📖	mathematical	—	CategoryTheory.IsIdempotentComplete	—	CategoryTheory.IsIdempotentComplete.idempotents_split CategoryTheory.op_comp
split_iff_of_iso 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom	CategoryTheory.CategoryStruct.id	—	split_imp_of_iso CategoryTheory.Category.comp_id CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc
split_imp_of_iso 📖	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.CategoryStruct.id	—	—	—

CategoryTheory.Idempotents.Equivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isIdempotentComplete 📖	mathematical	—	CategoryTheory.IsIdempotentComplete	—	CategoryTheory.Idempotents.split_iff_of_iso CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.id_comp CategoryTheory.IsIdempotentComplete.idempotents_split CategoryTheory.Functor.map_comp CategoryTheory.Functor.map_id CategoryTheory.Equivalence.fun_inv_map

CategoryTheory.IsIdempotentComplete

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
idempotents_split 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct	CategoryTheory.CategoryStruct.id	—	—

---

← Back to Index