KaroubiKaroubi

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

Statistics

Metric	Count
Definitions counitIso, equivalence, inverse, unitIso	4
Theorems counitIso_hom_app_f_f, counitIso_inv_app_f_f, additive_functor, additive_inverse, equivalence_counitIso, equivalence_functor, equivalence_inverse, equivalence_unitIso, idem_f, idem_f_assoc, instAdditiveKaroubiInverse, inverse_map_f, inverse_obj_X, inverse_obj_p, p_comm_f, p_comm_f_assoc, unitIso_hom_app_f, unitIso_inv_app_f	18
Total	22

CategoryTheory.Idempotents.KaroubiKaroubi

Definitions

Name	Category	Theorems
counitIso 📖	CompOp	3 math math: equivalence_counitIso, counitIso_inv_app_f_f, counitIso_hom_app_f_f
equivalence 📖	CompOp	7 math math: equivalence_counitIso, equivalence.additive_inverse, AlgebraicTopology.DoldKan.compatibility_N₂_N₁_karoubi, equivalence_inverse, equivalence_unitIso, equivalence_functor, equivalence.additive_functor
inverse 📖	CompOp	9 math math: counitIso_inv_app_f_f, equivalence_inverse, inverse_map_f, inverse_obj_p, unitIso_hom_app_f, counitIso_hom_app_f_f, instAdditiveKaroubiInverse, inverse_obj_X, unitIso_inv_app_f
unitIso 📖	CompOp	3 math math: equivalence_unitIso, unitIso_hom_app_f, unitIso_inv_app_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
counitIso_hom_app_f_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.comp inverse CategoryTheory.Idempotents.toKaroubi CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.Idempotents.Karoubi.p	—	—
counitIso_inv_app_f_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.id CategoryTheory.Functor.comp inverse CategoryTheory.Idempotents.toKaroubi CategoryTheory.NatTrans.app CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category counitIso CategoryTheory.Idempotents.Karoubi.p	—	—
equivalence_counitIso 📖	mathematical	—	CategoryTheory.Equivalence.counitIso CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory equivalence counitIso	—	—
equivalence_functor 📖	mathematical	—	CategoryTheory.Equivalence.functor CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory equivalence CategoryTheory.Idempotents.toKaroubi	—	—
equivalence_inverse 📖	mathematical	—	CategoryTheory.Equivalence.inverse CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory equivalence inverse	—	—
equivalence_unitIso 📖	mathematical	—	CategoryTheory.Equivalence.unitIso CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory equivalence unitIso	—	—
idem_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Idempotents.Karoubi.p	—	CategoryTheory.Idempotents.Karoubi.idem
idem_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Idempotents.Karoubi.p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' idem_f
instAdditiveKaroubiInverse 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.instPreadditiveKaroubi inverse	—	—
inverse_map_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.Karoubi.p CategoryTheory.Functor.map inverse	—	—
inverse_obj_X 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory inverse	—	—
inverse_obj_p 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.p CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory inverse CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Idempotents.Karoubi.X	—	—
p_comm_f 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Idempotents.Karoubi.p	—	CategoryTheory.Idempotents.Karoubi.p_comm
p_comm_f_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Idempotents.Karoubi.p	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' p_comm_f
unitIso_hom_app_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp CategoryTheory.Idempotents.toKaroubi inverse CategoryTheory.NatTrans.app CategoryTheory.Functor.id CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.Functor.category unitIso CategoryTheory.Idempotents.Karoubi.p	—	—
unitIso_inv_app_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Functor.comp CategoryTheory.Idempotents.toKaroubi inverse CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.Functor.category unitIso CategoryTheory.Idempotents.Karoubi.p	—	—

CategoryTheory.Idempotents.KaroubiKaroubi.equivalence

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
additive_functor 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.instPreadditiveKaroubi CategoryTheory.Equivalence.functor CategoryTheory.Idempotents.KaroubiKaroubi.equivalence	—	—
additive_inverse 📖	mathematical	—	CategoryTheory.Functor.Additive CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Idempotents.instPreadditiveKaroubi CategoryTheory.Equivalence.inverse CategoryTheory.Idempotents.KaroubiKaroubi.equivalence	—	—

---

← Back to Index