ExactFunctor

📁 Source: Mathlib/Algebra/Homology/DerivedCategory/ExactFunctor.lean

Statistics

Metric	Count
Definitions instCommShiftDerivedCategoryMapDerivedCategoryInt, instCommShiftHomologicalComplexIntUpFunctorQuasiIsoMapHomologicalComplexUpToQuasiIsoLocalizerMorphism, instLiftingCochainComplexIntDerivedCategoryQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory, instLiftingHomotopyCategoryIntUpDerivedCategoryQhQuasiIsoCompMapHomotopyCategoryMapDerivedCategory, mapDerivedCategory, mapDerivedCategoryFactors, mapDerivedCategoryFactorsh, mapDerivedCategorySingleFunctor	8
Theorems instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, instIsTriangulatedDerivedCategoryMapDerivedCategory, instLinearDerivedCategoryMapDerivedCategory, mapDerivedCategoryFactorsh_hom_app	5
Total	13

CategoryTheory.Functor

Definitions

Name	Category	Theorems
instCommShiftDerivedCategoryMapDerivedCategoryInt 📖	CompOp	4 math math: instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, CategoryTheory.Abelian.Ext.mapExactFunctor_hom, instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, instIsTriangulatedDerivedCategoryMapDerivedCategory
instCommShiftHomologicalComplexIntUpFunctorQuasiIsoMapHomologicalComplexUpToQuasiIsoLocalizerMorphism 📖	CompOp	—
instLiftingCochainComplexIntDerivedCategoryQQuasiIsoUpCompHomologicalComplexMapHomologicalComplexMapDerivedCategory 📖	CompOp	—
instLiftingHomotopyCategoryIntUpDerivedCategoryQhQuasiIsoCompMapHomotopyCategoryMapDerivedCategory 📖	CompOp	—
mapDerivedCategory 📖	CompOp	6 math math: instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, CategoryTheory.Abelian.Ext.mapExactFunctor_hom, instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, instIsTriangulatedDerivedCategoryMapDerivedCategory, instLinearDerivedCategoryMapDerivedCategory, mapDerivedCategoryFactorsh_hom_app
mapDerivedCategoryFactors 📖	CompOp	2 math math: instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors, mapDerivedCategoryFactorsh_hom_app
mapDerivedCategoryFactorsh 📖	CompOp	2 math math: instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh, mapDerivedCategoryFactorsh_hom_app
mapDerivedCategorySingleFunctor 📖	CompOp	1 math math: CategoryTheory.Abelian.Ext.mapExactFunctor_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors 📖	mathematical	—	CategoryTheory.NatTrans.CommShift CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DerivedCategory HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd DerivedCategory.instCategory comp DerivedCategory.Q mapDerivedCategory HomologicalComplex mapHomologicalComplex preservesZeroMorphisms_of_additive CategoryTheory.Iso.hom CategoryTheory.Functor category mapDerivedCategoryFactors Int.instAddMonoid CochainComplex.instHasShiftInt DerivedCategory.instHasShiftInt CommShift.comp DerivedCategory.instCommShiftCochainComplexIntQ instCommShiftDerivedCategoryMapDerivedCategoryInt commShiftMapCochainComplex	—	CategoryTheory.NatTrans.CommShift.verticalComposition AddRightCancelSemigroup.toIsRightCancelAdd preservesZeroMorphisms_of_additive CategoryTheory.NatTrans.CommShift.of_iso_inv DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh CategoryTheory.NatTrans.ext' mapDerivedCategoryFactorsh_hom_app CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app map_id CategoryTheory.Category.comp_id
instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh 📖	mathematical	—	CategoryTheory.NatTrans.CommShift HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing DerivedCategory instCategoryHomotopyCategory DerivedCategory.instCategory comp DerivedCategory.Qh mapDerivedCategory mapHomotopyCategory CategoryTheory.Iso.hom CategoryTheory.Functor category mapDerivedCategoryFactorsh Int.instAddMonoid HomotopyCategory.hasShift DerivedCategory.instHasShiftInt CommShift.comp DerivedCategory.instCommShiftHomotopyCategoryIntUpQh instCommShiftDerivedCategoryMapDerivedCategoryInt HomotopyCategory.instCommShiftIntUpMapHomotopyCategory	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.NatTrans.commShift_iso_hom_of_localization DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso
instIsTriangulatedDerivedCategoryMapDerivedCategory 📖	mathematical	—	IsTriangulated DerivedCategory DerivedCategory.instCategory DerivedCategory.instHasShiftInt mapDerivedCategory instCommShiftDerivedCategoryMapDerivedCategoryInt DerivedCategory.instHasZeroObject DerivedCategory.instPreadditive DerivedCategory.instAdditiveShiftFunctorInt DerivedCategory.instPretriangulated	—	isTriangulated_of_precomp_iso AddRightCancelSemigroup.toIsRightCancelAdd HomotopyCategory.instHasZeroObject CategoryTheory.Abelian.hasZeroObject DerivedCategory.instHasZeroObject HomotopyCategory.instAdditiveIntUpShiftFunctor DerivedCategory.instAdditiveShiftFunctorInt CategoryTheory.Abelian.hasBinaryBiproducts IsTriangulated.instComp HomotopyCategory.instIsTriangulatedIntUpMapHomotopyCategory DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh DerivedCategory.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh
instLinearDerivedCategoryMapDerivedCategory 📖	mathematical	—	Linear Ring.toSemiring DerivedCategory DerivedCategory.instCategory DerivedCategory.instPreadditive DerivedCategory.instLinear mapDerivedCategory	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Localization.functor_linear_iff CategoryTheory.categoryWithHomology_of_abelian DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso DerivedCategory.instLinearHomotopyCategoryIntUpQh instLinearComp CategoryTheory.instLinearHomotopyCategoryMapHomotopyCategory
mapDerivedCategoryFactorsh_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app HomotopyCategory CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing instCategoryHomotopyCategory DerivedCategory DerivedCategory.instCategory comp DerivedCategory.Qh mapDerivedCategory mapHomotopyCategory CategoryTheory.Iso.hom CategoryTheory.Functor category mapDerivedCategoryFactorsh obj HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms HomologicalComplex.instCategory HomotopyCategory.quotient CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct DerivedCategory.Q map DerivedCategory.quotientCompQhIso CochainComplex AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup mapHomologicalComplex preservesZeroMorphisms_of_additive mapDerivedCategoryFactors CategoryTheory.Iso.inv mapHomotopyCategoryFactors	—	mapHomologicalComplexUpToQuasiIsoFactorsh_hom_app AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian preservesHomologyOfExact preservesZeroMorphisms_of_additive instQFactorsThroughHomotopyIntUp CategoryTheory.Abelian.hasBinaryBiproducts instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences

---

← Back to Index