TStructure

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

Statistics

Metric	Count
Definitions	0
Theorems hasSmallLocalizedShiftedHom_of_isLE_of_isGE, instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat	2
Total	2

CategoryTheory.HasExt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasSmallLocalizedShiftedHom_of_isLE_of_isGE 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Localization.HasSmallLocalizedShiftedHom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.quasiIso CategoryTheory.categoryWithHomology_of_abelian Int.instAddMonoid CochainComplex.instHasShiftInt	—	AddRightCancelSemigroup.toIsRightCancelAdd CategoryTheory.categoryWithHomology_of_abelian DerivedCategory.exists_iso_singleFunctor_obj_of_isGE_of_isLE DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE CategoryTheory.Localization.hasSmallLocalizedShiftedHom_iff DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp small_of_injective CategoryTheory.instSmallHomDerivedCategoryObjSingleFunctorOfHasExt add_sub_cancel CategoryTheory.epi_of_effectiveEpi CategoryTheory.instEffectiveEpiOfIsIso CategoryTheory.NatIso.inv_app_isIso CategoryTheory.Functor.map_epi CategoryTheory.Functor.instPreservesEpimorphisms DerivedCategory.instHasZeroObject CategoryTheory.Functor.preservesZeroMorphisms_of_additive DerivedCategory.instAdditiveShiftFunctorInt CategoryTheory.Functor.preservesHomologyOfExact CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits CategoryTheory.Functor.instPreservesLimitsOfSizeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.instIsEquivalenceShiftFunctor CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.Functor.instPreservesColimitsOfSizeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Iso.isIso_inv CategoryTheory.mono_comp CategoryTheory.Functor.map_mono CategoryTheory.Functor.instPreservesMonomorphisms CategoryTheory.mono_of_strongMono CategoryTheory.instStrongMonoOfIsRegularMono CategoryTheory.instIsRegularMonoOfIsSplitMono CategoryTheory.IsSplitMono.of_iso CategoryTheory.Iso.isIso_hom CategoryTheory.Functor.instIsSplitMonoApp
instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat 📖	mathematical	CategoryTheory.HasExt	CategoryTheory.Localization.HasSmallLocalizedShiftedHom HomologicalComplex CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.Abelian.toPreadditive ComplexShape.up AddRightCancelSemigroup.toIsRightCancelAdd AddRightCancelMonoid.toAddRightCancelSemigroup AddCancelMonoid.toAddRightCancelMonoid AddGroup.toAddCancelMonoid Int.instAddGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Int.instRing HomologicalComplex.instCategory HomologicalComplex.quasiIso CategoryTheory.categoryWithHomology_of_abelian Int.instAddMonoid CochainComplex.instHasShiftInt	—	hasSmallLocalizedShiftedHom_of_isLE_of_isGE

---

← Back to Index