Reduced

📁 Source: Mathlib/Algebra/Homology/LeftResolution/Reduced.lean

Statistics

Metric	Count
Definitions karoubi, F, F', retractArrow, π, π', reduced	7
Theorems instEpiKaroubiAppπ, instEpiKaroubiAppπ', instEpiKaroubiAppπObjToKaroubi, instPreservesZeroMorphismsFReduced, instPreservesZeroMorphismsKaroubiF, instPreservesZeroMorphismsKaroubiFKaroubi, F'_map_f, F'_obj_X, F'_obj_p, F_map_f, F_obj_X, F_obj_p, π'_app_f, π_app_toKaroubi_obj, karoubi_F, karoubi_π	16
Total	23

CategoryTheory.Abelian.LeftResolution

Definitions

Name	Category	Theorems
karoubi 📖	CompOp	3 math math: karoubi_π, karoubi_F, instPreservesZeroMorphismsKaroubiFKaroubi
reduced 📖	CompOp	1 math math: instPreservesZeroMorphismsFReduced

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEpiKaroubiAppπ 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.comp karoubi.F CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Idempotents.functorExtension₂ CategoryTheory.Functor.id CategoryTheory.NatTrans.app karoubi.π	—	CategoryTheory.MorphismProperty.of_retract CategoryTheory.MorphismProperty.IsStableUnderRetracts.epimorphisms CategoryTheory.MorphismProperty.epimorphisms.infer_property instEpiKaroubiAppπObjToKaroubi
instEpiKaroubiAppπ' 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Idempotents.toKaroubi karoubi.F CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Idempotents.functorExtension₂ CategoryTheory.NatTrans.app karoubi.π'	—	CategoryTheory.MorphismProperty.of_retract CategoryTheory.MorphismProperty.IsStableUnderRetracts.epimorphisms CategoryTheory.MorphismProperty.epimorphisms.infer_property CategoryTheory.Functor.map_epi CategoryTheory.Idempotents.instPreservesEpimorphismsKaroubiToKaroubi epi_π_app
instEpiKaroubiAppπObjToKaroubi 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor.comp karoubi.F CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Idempotents.functorExtension₂ CategoryTheory.Idempotents.toKaroubi CategoryTheory.Functor.id CategoryTheory.NatTrans.app karoubi.π	—	karoubi.π_app_toKaroubi_obj instEpiKaroubiAppπ'
instPreservesZeroMorphismsFReduced 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Preadditive.preadditiveHasZeroMorphisms F reduced	—	CategoryTheory.Functor.preservesZeroMorphisms_comp CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Idempotents.toKaroubiEquivalence_functor_additive instPreservesZeroMorphismsKaroubiF CategoryTheory.Equivalence.inverse_additive
instPreservesZeroMorphismsKaroubiF 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Idempotents.instPreadditiveKaroubi karoubi.F	—	sub_self
instPreservesZeroMorphismsKaroubiFKaroubi 📖	mathematical	—	CategoryTheory.Functor.PreservesZeroMorphisms CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Idempotents.instPreadditiveKaroubi F CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Idempotents.functorExtension₂ karoubi	—	sub_self
karoubi_F 📖	mathematical	—	F CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Idempotents.functorExtension₂ karoubi karoubi.F	—	—
karoubi_π 📖	mathematical	—	π CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Idempotents.functorExtension₂ karoubi karoubi.π	—	—

CategoryTheory.Abelian.LeftResolution.karoubi

Definitions

Name	Category	Theorems
F 📖	CompOp	10 math math: F_obj_p, π_app_toKaroubi_obj, F_map_f, CategoryTheory.Abelian.LeftResolution.instPreservesZeroMorphismsKaroubiF, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ', CategoryTheory.Abelian.LeftResolution.karoubi_F, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπObjToKaroubi, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ, π'_app_f, F_obj_X
F' 📖	CompOp	4 math math: F'_map_f, F_map_f, F'_obj_p, F'_obj_X
retractArrow 📖	CompOp	—
π 📖	CompOp	4 math math: π_app_toKaroubi_obj, CategoryTheory.Abelian.LeftResolution.karoubi_π, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπObjToKaroubi, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ
π' 📖	CompOp	3 math math: π_app_toKaroubi_obj, CategoryTheory.Abelian.LeftResolution.instEpiKaroubiAppπ', π'_app_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
F'_map_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Functor.obj CategoryTheory.Abelian.LeftResolution.F Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory F' CategoryTheory.Idempotents.Karoubi.X	—	—
F'_obj_X 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory F' CategoryTheory.Abelian.LeftResolution.F	—	—
F'_obj_p 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.p CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory F' Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.LeftResolution.F SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.CategoryStruct.id CategoryTheory.Functor.map CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
F_map_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory F' CategoryTheory.Functor.map CategoryTheory.Idempotents.Karoubi.p F Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.LeftResolution.F SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
F_obj_X 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.X CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory F CategoryTheory.Abelian.LeftResolution.F	—	—
F_obj_p 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.p CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory F Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Abelian.LeftResolution.F CategoryTheory.Idempotents.Karoubi.X SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup CategoryTheory.Functor.map CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms	—	—
π'_app_f 📖	mathematical	—	CategoryTheory.Idempotents.Karoubi.Hom.f CategoryTheory.Functor.obj CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp CategoryTheory.Idempotents.toKaroubi F CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Idempotents.functorExtension₂ CategoryTheory.NatTrans.app π' CategoryTheory.Abelian.LeftResolution.F CategoryTheory.Functor.id CategoryTheory.Abelian.LeftResolution.π	—	—
π_app_toKaroubi_obj 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Idempotents.Karoubi CategoryTheory.Idempotents.Karoubi.instCategory CategoryTheory.Functor.comp F CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Idempotents.functorExtension₂ CategoryTheory.Functor.id π CategoryTheory.Idempotents.toKaroubi π'	—	CategoryTheory.Functor.map_id CategoryTheory.Functor.map_sub CategoryTheory.Category.comp_id CategoryTheory.Preadditive.sub_comp CategoryTheory.Category.id_comp CategoryTheory.Abelian.LeftResolution.π_naturality CategoryTheory.Limits.comp_zero sub_zero

---

← Back to Index