TStructure

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

Statistics

Metric	Count
Definitions TStructure, IsGE, IsLE, t	4
Theorems exists_iso_Q_obj_of_isGE, exists_iso_Q_obj_of_isGE_of_isLE, exists_iso_Q_obj_of_isLE, exists_iso_singleFunctor_obj_of_isGE_of_isLE, instIsGEObjCochainComplexIntQOfIsGE, instIsGEObjSingleFunctor, instIsLEObjCochainComplexIntQOfIsLE, instIsLEObjSingleFunctor, isGE_Q_obj_iff, isGE_iff, isLE_Q_obj_iff, isLE_iff, isZero_of_isGE, isZero_of_isLE	14
Total	18

CategoryTheory.Triangulated

Definitions

Name	Category	Theorems
TStructure 📖	CompData	—

DerivedCategory

Definitions

Name	Category	Theorems
IsGE 📖	MathDef	4 math math: isGE_Q_obj_iff, isGE_iff, instIsGEObjCochainComplexIntQOfIsGE, instIsGEObjSingleFunctor
IsLE 📖	MathDef	4 math math: isLE_iff, isLE_Q_obj_iff, instIsLEObjSingleFunctor, instIsLEObjCochainComplexIntQOfIsLE

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_iso_Q_obj_of_isGE 📖	mathematical	—	CategoryTheory.Iso DerivedCategory instCategory CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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 Q	—	instHasZeroObject instAdditiveShiftFunctorInt AddRightCancelSemigroup.toIsRightCancelAdd
exists_iso_Q_obj_of_isGE_of_isLE 📖	mathematical	—	CategoryTheory.Iso DerivedCategory instCategory CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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 Q	—	AddRightCancelSemigroup.toIsRightCancelAdd exists_iso_Q_obj_of_isLE isGE_Q_obj_iff CategoryTheory.Triangulated.TStructure.isGE_of_iso instHasZeroObject instAdditiveShiftFunctorInt CategoryTheory.Abelian.hasZeroObject CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.instIsStrictlySupportedTruncGE ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE HomologicalComplex.instIsStrictlySupportedTruncGE_1 instIsIsoMapCochainComplexIntQ CochainComplex.instQuasiIsoIntπTruncGEOfIsGE
exists_iso_Q_obj_of_isLE 📖	mathematical	—	CategoryTheory.Iso DerivedCategory instCategory CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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 Q	—	instHasZeroObject instAdditiveShiftFunctorInt AddRightCancelSemigroup.toIsRightCancelAdd
exists_iso_singleFunctor_obj_of_isGE_of_isLE 📖	mathematical	—	CategoryTheory.Iso DerivedCategory instCategory CategoryTheory.Functor.obj singleFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd exists_iso_Q_obj_of_isGE_of_isLE CategoryTheory.Abelian.hasZeroObject CochainComplex.exists_iso_single
instIsGEObjCochainComplexIntQOfIsGE 📖	mathematical	—	IsGE CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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 DerivedCategory instCategory Q	—	AddRightCancelSemigroup.toIsRightCancelAdd isGE_Q_obj_iff
instIsGEObjSingleFunctor 📖	mathematical	—	IsGE CategoryTheory.Functor.obj DerivedCategory instCategory singleFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject CategoryTheory.Triangulated.TStructure.isGE_of_iso instHasZeroObject instAdditiveShiftFunctorInt instIsGEObjCochainComplexIntQOfIsGE HomologicalComplex.instIsSupportedOfIsStrictlySupported CochainComplex.instIsStrictlyGEObjIntSingleFunctor
instIsLEObjCochainComplexIntQOfIsLE 📖	mathematical	—	IsLE CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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 DerivedCategory instCategory Q	—	AddRightCancelSemigroup.toIsRightCancelAdd isLE_Q_obj_iff
instIsLEObjSingleFunctor 📖	mathematical	—	IsLE CategoryTheory.Functor.obj DerivedCategory instCategory singleFunctor	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.Abelian.hasZeroObject CategoryTheory.Triangulated.TStructure.isLE_of_iso instHasZeroObject instAdditiveShiftFunctorInt instIsLEObjCochainComplexIntQOfIsLE HomologicalComplex.instIsSupportedOfIsStrictlySupported CochainComplex.instIsStrictlyLEObjIntSingleFunctor
isGE_Q_obj_iff 📖	mathematical	—	IsGE CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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 DerivedCategory instCategory Q CochainComplex.IsGE	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.isZero_iff CategoryTheory.CategoryWithHomology.hasHomology
isGE_iff 📖	mathematical	—	IsGE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj DerivedCategory instCategory homologyFunctor	—	instHasZeroObject instAdditiveShiftFunctorInt CategoryTheory.Limits.IsZero.of_iso AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.ExactAt.isZero_homology CochainComplex.exactAt_of_isGE HomologicalComplex.instIsSupportedOfIsStrictlySupported instEssSurjCochainComplexIntQ CochainComplex.isGE_iff HomologicalComplex.exactAt_iff_isZero_homology CategoryTheory.Abelian.hasZeroObject instIsIsoMapCochainComplexIntQ CochainComplex.instQuasiIsoIntπTruncGEOfIsGE HomologicalComplex.instIsStrictlySupportedTruncGE ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE
isLE_Q_obj_iff 📖	mathematical	—	IsLE CategoryTheory.Functor.obj CochainComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive 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 DerivedCategory instCategory Q CochainComplex.IsLE	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian CategoryTheory.Iso.isZero_iff CategoryTheory.CategoryWithHomology.hasHomology
isLE_iff 📖	mathematical	—	IsLE CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj DerivedCategory instCategory homologyFunctor	—	instHasZeroObject instAdditiveShiftFunctorInt CategoryTheory.Limits.IsZero.of_iso AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.CategoryWithHomology.hasHomology CategoryTheory.categoryWithHomology_of_abelian HomologicalComplex.ExactAt.isZero_homology CochainComplex.exactAt_of_isLE HomologicalComplex.instIsSupportedOfIsStrictlySupported instEssSurjCochainComplexIntQ CochainComplex.isLE_iff HomologicalComplex.exactAt_iff_isZero_homology CategoryTheory.Abelian.hasZeroObject instIsIsoMapCochainComplexIntQ CochainComplex.instQuasiIsoIntιTruncLEOfIsLE HomologicalComplex.instIsStrictlySupportedTruncLE ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE
isZero_of_isGE 📖	mathematical	—	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj DerivedCategory instCategory homologyFunctor	—	isGE_iff
isZero_of_isLE 📖	mathematical	—	CategoryTheory.Limits.IsZero CategoryTheory.Functor.obj DerivedCategory instCategory homologyFunctor	—	isLE_iff

DerivedCategory.TStructure

Definitions

Name	Category	Theorems
t 📖	CompOp	—

---

← Back to Index