SpectralObject

📁 Source: Mathlib/Algebra/Homology/HomotopyCategory/SpectralObject.lean

Statistics

Metric	Count
Definitions composableArrowsFunctor, spectralObjectMappingCone	2
Theorems composableArrowsFunctor_map, composableArrowsFunctor_obj, spectralObjectMappingCone_δ'_app, spectralObjectMappingCone_ω₁	4
Total	6

HomotopyCategory

Definitions

Name	Category	Theorems
composableArrowsFunctor 📖	CompOp	4 math math: spectralObjectMappingCone_δ'_app, composableArrowsFunctor_obj, composableArrowsFunctor_map, spectralObjectMappingCone_ω₁
spectralObjectMappingCone 📖	CompOp	2 math math: spectralObjectMappingCone_δ'_app, spectralObjectMappingCone_ω₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
composableArrowsFunctor_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.ComposableArrows CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder composableArrowsFunctor CochainComplex.mappingCone.map CategoryTheory.Functor.obj CategoryTheory.ComposableArrows.map' CategoryTheory.NatTrans.app	—	AddRightCancelSemigroup.toIsRightCancelAdd CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct
composableArrowsFunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.ComposableArrows CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder composableArrowsFunctor CochainComplex.mappingCone CategoryTheory.ComposableArrows.map'	—	AddRightCancelSemigroup.toIsRightCancelAdd
spectralObjectMappingCone_δ'_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.ComposableArrows CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory ComplexShape.up AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder HomotopyCategory instCategoryHomotopyCategory CategoryTheory.Functor.comp CategoryTheory.ComposableArrows.functorArrows composableArrowsFunctor quotient CategoryTheory.shiftFunctor Int.instAddMonoid hasShift CategoryTheory.Triangulated.SpectralObject.δ' AddRightCancelSemigroup.toIsRightCancelAdd instHasZeroObject instPreadditive instAdditiveIntUpShiftFunctor instPretriangulatedIntUp spectralObjectMappingCone CategoryTheory.Pretriangulated.Triangle.mor₃ CategoryTheory.Functor.obj CategoryTheory.Pretriangulated.Triangle HomologicalComplex CochainComplex.instHasShiftInt CategoryTheory.Pretriangulated.triangleCategory CategoryTheory.Functor.mapTriangle commShiftQuotient CochainComplex.mappingConeCompTriangle CategoryTheory.ComposableArrows.map'	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasZeroObject instAdditiveIntUpShiftFunctor
spectralObjectMappingCone_ω₁ 📖	mathematical	—	CategoryTheory.Triangulated.SpectralObject.ω₁ HomotopyCategory ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instCategoryHomotopyCategory HomologicalComplex.instCategory AddSemigroup.toAdd AddRightCancelSemigroup.toAddSemigroup instHasZeroObject hasShift instPreadditive instAdditiveIntUpShiftFunctor instPretriangulatedIntUp spectralObjectMappingCone CategoryTheory.Functor.comp CategoryTheory.ComposableArrows CategoryTheory.Functor.category Preorder.smallCategory PartialOrder.toPreorder Fin.instPartialOrder composableArrowsFunctor quotient	—	AddRightCancelSemigroup.toIsRightCancelAdd instHasZeroObject instAdditiveIntUpShiftFunctor

---

← Back to Index