Functor

📁 Source: Mathlib/Algebra/Homology/Functor.lean

Statistics

Metric	Count
Definitions asFunctor, complexOfFunctorsToFunctorToComplex	2
Theorems quasiIso_iff_evaluation, asFunctor_map_f, asFunctor_obj_X, asFunctor_obj_d, complexOfFunctorsToFunctorToComplex_map_app_f, complexOfFunctorsToFunctorToComplex_obj, quasiIsoAt_iff_evaluation, quasiIso_iff_evaluation	8
Total	10

CategoryTheory.ShortComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quasiIso_iff_evaluation 📖	mathematical	—	QuasiIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.functorCategoryAbelian CategoryTheory.Functor.obj CategoryTheory.ShortComplex instCategory CategoryTheory.Functor.mapShortComplex CategoryTheory.evaluation CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj hasHomology_of_preserves' CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Limits.instPreservesFiniteLimitsFunctorObjEvaluationOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.Limits.instPreservesFiniteColimitsFunctorObjEvaluationOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf CategoryTheory.Functor.map	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj hasHomology_of_preserves' CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Limits.instPreservesFiniteLimitsFunctorObjEvaluationOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.Limits.instPreservesFiniteColimitsFunctorObjEvaluationOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf quasiIso_map_of_preservesRightHomology quasiIso_iff CategoryTheory.NatTrans.isIso_iff_isIso_app CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.MorphismProperty.RespectsIso.isomorphisms

HomologicalComplex

Definitions

Name	Category	Theorems
asFunctor 📖	CompOp	5 math math: asFunctor_obj_X, complexOfFunctorsToFunctorToComplex_obj, complexOfFunctorsToFunctorToComplex_map_app_f, asFunctor_obj_d, asFunctor_map_f
complexOfFunctorsToFunctorToComplex 📖	CompOp	2 math math: complexOfFunctorsToFunctorToComplex_obj, complexOfFunctorsToFunctorToComplex_map_app_f

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asFunctor_map_f 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj X CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.NatTrans.app d CategoryTheory.Functor.map HomologicalComplex instCategory asFunctor	—	—
asFunctor_obj_X 📖	mathematical	—	X CategoryTheory.Functor.obj HomologicalComplex instCategory asFunctor CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor	—	—
asFunctor_obj_d 📖	mathematical	—	d CategoryTheory.Functor.obj HomologicalComplex instCategory asFunctor CategoryTheory.NatTrans.app X CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor	—	—
complexOfFunctorsToFunctorToComplex_map_app_f 📖	mathematical	—	Hom.f CategoryTheory.Functor.obj HomologicalComplex instCategory asFunctor CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor complexOfFunctorsToFunctorToComplex X	—	—
complexOfFunctorsToFunctorToComplex_obj 📖	mathematical	—	CategoryTheory.Functor.obj HomologicalComplex CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor instCategory complexOfFunctorsToFunctorToComplex asFunctor	—	—
quasiIsoAt_iff_evaluation 📖	mathematical	—	QuasiIsoAt CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.functorCategoryAbelian sc CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.evaluation CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj CategoryTheory.Functor.map	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj CategoryTheory.ShortComplex.hasHomology_of_preserves' CategoryTheory.Functor.PreservesHomology.preservesLeftHomologyOf CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Limits.instPreservesFiniteLimitsFunctorObjEvaluationOfHasFiniteLimits CategoryTheory.Abelian.hasFiniteLimits CategoryTheory.Limits.instPreservesFiniteColimitsFunctorObjEvaluationOfHasFiniteColimits CategoryTheory.Abelian.hasFiniteColimits CategoryTheory.Functor.PreservesHomology.preservesRightHomologyOf
quasiIso_iff_evaluation 📖	mathematical	—	QuasiIso CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.instHasZeroMorphismsFunctor CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Abelian.functorCategoryAbelian sc CategoryTheory.Functor.obj HomologicalComplex instCategory CategoryTheory.Functor.mapHomologicalComplex CategoryTheory.evaluation CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj CategoryTheory.Functor.map	—	CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Functor.preservesZeroMorphisms_evaluation_obj

---

← Back to Index