Subcategory

📁 Source: Mathlib/CategoryTheory/Triangulated/Subcategory.lean

Statistics

Metric	Count
Definitions IsTriangulated, IsTriangulatedClosed₁, IsTriangulatedClosed₂, IsTriangulatedClosed₃, extensionProduct, extensionProductIter, instPretriangulatedFullSubcategory, trW	8
Theorems toContainsZero, toIsStableUnderShift, toIsTriangulatedClosed₂, ext₁', mk', ext₂', mk', ext₃', mk', ext_of_isTriangulatedClosed₁, ext_of_isTriangulatedClosed₁', ext_of_isTriangulatedClosed₂, ext_of_isTriangulatedClosed₂', ext_of_isTriangulatedClosed₃, ext_of_isTriangulatedClosed₃', extensionProductIter_add, extensionProductIter_add', extensionProductIter_bot, extensionProductIter_le_of_isTriangulatedClosed₂, extensionProductIter_le_of_isTriangulatedClosed₂', extensionProductIter_retractClosure_le, extensionProductIter_succ, extensionProductIter_succ', extensionProductIter_top, extensionProductIter_zero, extensionProduct_assoc, extensionProduct_bot_left, extensionProduct_bot_right, extensionProduct_iff, extensionProduct_isoClosure_left, extensionProduct_isoClosure_right, extensionProduct_le_of_isTriangulatedClosed₂, extensionProduct_le_of_isTriangulatedClosed₂', extensionProduct_retractClosure_retractClosure_le, instContainsIdentitiesTrWOfContainsZero, instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated, instHasRightCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated, instIsClosedUnderBinaryProductsOfIsTriangulatedOfIsClosedUnderIsomorphisms, instIsClosedUnderFiniteProductsOfIsTriangulatedOfIsClosedUnderIsomorphisms, instIsClosedUnderIsomorphismsExtensionProduct, instIsCompatibleWithShiftTrWIntOfIsStableUnderShift, instIsCompatibleWithTriangulationTrWOfIsTriangulatedOfIsTriangulated, instIsMultiplicativeTrWOfIsTriangulatedOfIsTriangulated, instIsStableUnderFiniteProductsTrWOfIsTriangulated, instIsStableUnderShiftExtensionProductInt, instIsStableUnderShiftExtensionProductIterInt, instIsStableUnderShiftExtensionProductIterInt_1, instIsTriangulatedClosed₁OfIsTriangulated, instIsTriangulatedClosed₂IsoClosure, instIsTriangulatedClosed₂MinOfIsClosedUnderIsomorphisms, instIsTriangulatedClosed₃OfIsTriangulated, instIsTriangulatedEssImageOfIsTriangulatedOfFull, instIsTriangulatedFullSubcategory, instIsTriangulatedFullSubcategoryι, instIsTriangulatedInverseImage, instIsTriangulatedIsoClosure, instIsTriangulatedMapOfIsTriangulatedOfFull, instIsTriangulatedMinOfIsClosedUnderIsomorphisms, instRespectsIsoTrW, inverseImage_trW_iff, inverseImage_trW_isInverted, isTriangulated_lift, le_extensionProductIter, le_extensionProduct_left, le_extensionProduct_right, monotone'_extensionProductIter, monotone_extensionProductIter, monotone_extensionProduct_left, monotone_extensionProduct_right, retractClosure_extensionProductIter_retractClosure, retractClosure_extensionProduct_retractClosure_retractClosure, smul_mem_trW_iff, mk, mk', shift, unshift, trW_iff, trW_iff', trW_iff_of_distinguished, trW_iff_of_distinguished', trW_isoClosure, trW_of_isIso	82
Total	90

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
IsTriangulated 📖	CompData	12 math math: instIsTriangulatedIsoClosure, CategoryTheory.Functor.instIsTriangulatedHomologicalKernel, instIsTriangulatedEssImageOfIsTriangulatedOfFull, instIsTriangulatedLeftOrthogonalOfIsStableUnderShiftInt, instIsTriangulatedRightOrthogonalOfIsStableUnderShiftInt, CategoryTheory.Triangulated.TStructure.instIsTriangulatedBounded, HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic, instIsTriangulatedMapOfIsTriangulatedOfFull, CategoryTheory.Triangulated.TStructure.instIsTriangulatedPlus, instIsTriangulatedMinOfIsClosedUnderIsomorphisms, instIsTriangulatedInverseImage, CategoryTheory.Triangulated.TStructure.instIsTriangulatedMinus
IsTriangulatedClosed₁ 📖	CompData	2 math math: instIsTriangulatedClosed₁OfIsTriangulated, IsTriangulatedClosed₁.mk'
IsTriangulatedClosed₂ 📖	CompData	6 math math: IsTriangulated.toIsTriangulatedClosed₂, instIsTriangulatedClosed₂RightOrthogonal, instIsTriangulatedClosed₂MinOfIsClosedUnderIsomorphisms, instIsTriangulatedClosed₂LeftOrthogonal, IsTriangulatedClosed₂.mk', instIsTriangulatedClosed₂IsoClosure
IsTriangulatedClosed₃ 📖	CompData	2 math math: IsTriangulatedClosed₃.mk', instIsTriangulatedClosed₃OfIsTriangulated
extensionProduct 📖	CompOp	20 math math: le_extensionProduct_left, monotone_extensionProduct_right, extensionProduct_bot_right, extensionProduct_isoClosure_left, extensionProduct_assoc, extensionProductIter_add', extensionProduct_bot_left, extensionProductIter_succ', extensionProduct_le_of_isTriangulatedClosed₂, extensionProduct_isoClosure_right, extensionProduct_iff, monotone_extensionProduct_left, extensionProduct_le_of_isTriangulatedClosed₂', retractClosure_extensionProduct_retractClosure_retractClosure, extensionProductIter_succ, instIsStableUnderShiftExtensionProductInt, extensionProduct_retractClosure_retractClosure_le, le_extensionProduct_right, extensionProductIter_add, instIsClosedUnderIsomorphismsExtensionProduct
extensionProductIter 📖	CompOp	16 math math: extensionProductIter_le_of_isTriangulatedClosed₂', le_extensionProductIter, extensionProductIter_le_of_isTriangulatedClosed₂, instIsStableUnderShiftExtensionProductIterInt_1, extensionProductIter_top, extensionProductIter_add', extensionProductIter_succ', extensionProductIter_succ, extensionProductIter_retractClosure_le, monotone_extensionProductIter, instIsStableUnderShiftExtensionProductIterInt, monotone'_extensionProductIter, extensionProductIter_bot, extensionProductIter_add, retractClosure_extensionProductIter_retractClosure, extensionProductIter_zero
instPretriangulatedFullSubcategory 📖	CompOp	5 math math: tStructure_isGE_iff, instIsTriangulatedFullSubcategoryι, tStructure_isLE_iff, instIsTriangulatedFullSubcategory, isTriangulated_lift
trW 📖	CompOp	26 math math: inverseImage_trW_isInverted, trW.unshift, instIsMultiplicativeTrWOfIsTriangulatedOfIsTriangulated, instIsCompatibleWithTriangulationTrWOfIsTriangulatedOfIsTriangulated, instHasRightCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated, trW_iff_of_distinguished, instIsCompatibleWithShiftTrWIntOfIsStableUnderShift, trW.mk', trW_iff', trW_of_isIso, instRespectsIsoTrW, trW_iff_of_distinguished', isColocal_trW, HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W, inverseImage_trW_iff, trW.mk, instContainsIdentitiesTrWOfContainsZero, instIsStableUnderFiniteProductsTrWOfIsTriangulated, instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated, trW_isoClosure, trW.shift, CategoryTheory.Functor.mem_homologicalKernel_trW_iff, isLocal_trW, smul_mem_trW_iff, trW_iff, DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext_of_isTriangulatedClosed₁ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃	CategoryTheory.Pretriangulated.Triangle.obj₁	—	isoClosure_eq_self ext_of_isTriangulatedClosed₁'
ext_of_isTriangulatedClosed₁' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃	isoClosure CategoryTheory.Pretriangulated.Triangle.obj₁	—	IsTriangulatedClosed₁.ext₁'
ext_of_isTriangulatedClosed₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₃	CategoryTheory.Pretriangulated.Triangle.obj₂	—	isoClosure_eq_self ext_of_isTriangulatedClosed₂'
ext_of_isTriangulatedClosed₂' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₃	isoClosure CategoryTheory.Pretriangulated.Triangle.obj₂	—	IsTriangulatedClosed₂.ext₂'
ext_of_isTriangulatedClosed₃ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂	CategoryTheory.Pretriangulated.Triangle.obj₃	—	isoClosure_eq_self ext_of_isTriangulatedClosed₃'
ext_of_isTriangulatedClosed₃' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂	isoClosure CategoryTheory.Pretriangulated.Triangle.obj₃	—	IsTriangulatedClosed₃.ext₃'
extensionProductIter_add 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProductIter extensionProduct	—	add_zero extensionProductIter_zero extensionProductIter_succ' add_assoc extensionProduct_assoc
extensionProductIter_add' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProductIter extensionProduct	—	zero_add extensionProductIter_zero extensionProductIter_succ add_assoc add_comm extensionProduct_assoc
extensionProductIter_bot 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProductIter Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	extensionProductIter_zero extensionProductIter_succ extensionProduct_bot_left
extensionProductIter_le_of_isTriangulatedClosed₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProductIter	—	extensionProductIter_le_of_isTriangulatedClosed₂' isoClosure_eq_self
extensionProductIter_le_of_isTriangulatedClosed₂' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProductIter isoClosure	—	extensionProductIter_zero LE.le.trans le_isoClosure extensionProductIter_succ extensionProduct_le_of_isTriangulatedClosed₂ instIsTriangulatedClosed₂IsoClosure instIsClosedUnderIsomorphismsIsoClosure
extensionProductIter_retractClosure_le 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProductIter retractClosure	—	instReflLe extensionProductIter_succ le_imp_le_of_le_of_le monotone_extensionProduct_right le_refl extensionProduct_retractClosure_retractClosure_le
extensionProductIter_succ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProductIter extensionProduct	—	Function.iterate_succ_apply'
extensionProductIter_succ' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProductIter extensionProduct	—	extensionProductIter_succ extensionProduct_assoc
extensionProductIter_top 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProductIter Top.top CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	—	eq_top_iff le_extensionProductIter instContainsZeroTopOfHasZeroObject
extensionProductIter_zero 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProductIter	—	—
extensionProduct_assoc 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProduct	—	CategoryTheory.Pretriangulated.distinguished_cocone_triangle CategoryTheory.Triangulated.Octahedron.mem CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁ CategoryTheory.Triangulated.Octahedron'.mem
extensionProduct_bot_left 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProduct Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	eq_bot_iff
extensionProduct_bot_right 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProduct Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	eq_bot_iff
extensionProduct_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProduct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	—	—
extensionProduct_isoClosure_left 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProduct isoClosure	—	le_antisymm CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Iso.map_hom_inv_id monotone_extensionProduct_left le_isoClosure
extensionProduct_isoClosure_right 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	extensionProduct isoClosure	—	le_antisymm CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Functor.map_id monotone_extensionProduct_right le_isoClosure
extensionProduct_le_of_isTriangulatedClosed₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProduct	—	ext_of_isTriangulatedClosed₂
extensionProduct_le_of_isTriangulatedClosed₂' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProduct isoClosure	—	ext_of_isTriangulatedClosed₂'
extensionProduct_retractClosure_retractClosure_le 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProduct retractClosure	—	CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂ CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₂ CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Pretriangulated.isIso₂_of_isIso₁₃ CategoryTheory.IsIso.id
instContainsIdentitiesTrWOfContainsZero 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.MorphismProperty.ContainsIdentities trW	—	trW_isoClosure CategoryTheory.Pretriangulated.contractible_distinguished prop_zero instContainsZeroIsoClosure instIsClosedUnderIsomorphismsIsoClosure
instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions trW	—	instIsMultiplicativeTrWOfIsTriangulatedOfIsTriangulated CategoryTheory.MorphismProperty.RightFraction.hs CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂ CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₂ CategoryTheory.Category.id_comp CategoryTheory.Preadditive.comp_sub sub_self CategoryTheory.Pretriangulated.Triangle.yoneda_exact₂ CategoryTheory.Pretriangulated.distinguished_cocone_triangle CategoryTheory.Pretriangulated.rot_of_distTriang le_shift IsStableUnderShift.isStableUnderShiftBy IsTriangulated.toIsStableUnderShift CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂ sub_eq_zero CategoryTheory.Preadditive.sub_comp CategoryTheory.Category.assoc CategoryTheory.Limits.comp_zero
instHasRightCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.MorphismProperty.HasRightCalculusOfFractions trW	—	instIsMultiplicativeTrWOfIsTriangulatedOfIsTriangulated CategoryTheory.MorphismProperty.LeftFraction.hs CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁ CategoryTheory.Pretriangulated.complete_distinguished_triangle_morphism₁ CategoryTheory.Category.comp_id trW_iff' IsTriangulated.toIsStableUnderShift CategoryTheory.Preadditive.sub_comp sub_self CategoryTheory.Pretriangulated.Triangle.coyoneda_exact₂ CategoryTheory.Pretriangulated.comp_distTriang_mor_zero₁₂ sub_eq_zero CategoryTheory.Preadditive.comp_sub CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' CategoryTheory.Limits.zero_comp
instIsClosedUnderBinaryProductsOfIsTriangulatedOfIsClosedUnderIsomorphisms 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsClosedUnderBinaryProducts	—	prop_of_iso CategoryTheory.Limits.HasBinaryBiproduct.hasLimit_pair CategoryTheory.Limits.HasBinaryBiproducts.has_binary_biproduct CategoryTheory.Pretriangulated.instHasBinaryBiproducts ext_of_isTriangulatedClosed₂ IsTriangulated.toIsTriangulatedClosed₂ CategoryTheory.Pretriangulated.binaryProductTriangle_distinguished LimitOfShape.prop_diag_obj
instIsClosedUnderFiniteProductsOfIsTriangulatedOfIsClosedUnderIsomorphisms 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsClosedUnderFiniteProducts	—	IsClosedUnderFiniteProducts.mk' CategoryTheory.Pretriangulated.instHasFiniteProducts instIsClosedUnderLimitsOfShapeDiscretePEmptyOfContainsZeroOfIsClosedUnderIsomorphisms IsTriangulated.toContainsZero instIsClosedUnderBinaryProductsOfIsTriangulatedOfIsClosedUnderIsomorphisms
instIsClosedUnderIsomorphismsExtensionProduct 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsClosedUnderIsomorphisms extensionProduct	—	CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id
instIsCompatibleWithShiftTrWIntOfIsStableUnderShift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.MorphismProperty.IsCompatibleWithShift trW Int.instAddMonoid	—	CategoryTheory.MorphismProperty.ext trW.unshift trW.shift
instIsCompatibleWithTriangulationTrWOfIsTriangulatedOfIsTriangulated 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.MorphismProperty.IsCompatibleWithTriangulation trW	—	instIsCompatibleWithShiftTrWIntOfIsStableUnderShift IsTriangulated.toIsStableUnderShift CategoryTheory.Pretriangulated.distinguished_cocone_triangle CategoryTheory.MorphismProperty.comp_mem CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeTrWOfIsTriangulatedOfIsTriangulated CategoryTheory.Triangulated.Octahedron.mem trW.mk' CategoryTheory.Category.comp_id CategoryTheory.Pretriangulated.TriangleMorphism.comm₂ CategoryTheory.Category.assoc CategoryTheory.Category.id_comp CategoryTheory.Pretriangulated.TriangleMorphism.comm₃
instIsMultiplicativeTrWOfIsTriangulatedOfIsTriangulated 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.MorphismProperty.IsMultiplicative trW	—	instContainsIdentitiesTrWOfContainsZero IsTriangulated.toContainsZero trW_isoClosure CategoryTheory.Pretriangulated.distinguished_cocone_triangle ext_of_isTriangulatedClosed₂ instIsTriangulatedClosed₂IsoClosure IsTriangulated.toIsTriangulatedClosed₂ instIsClosedUnderIsomorphismsIsoClosure CategoryTheory.Triangulated.Octahedron.mem
instIsStableUnderFiniteProductsTrWOfIsTriangulated 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.MorphismProperty.IsStableUnderFiniteProducts trW	—	trW_isoClosure instRespectsIsoTrW CategoryTheory.Limits.hasProduct_of_hasBiproduct CategoryTheory.Limits.HasBiproductsOfShape.has_biproduct CategoryTheory.Limits.hasBiproductsOfShape_finite CategoryTheory.Pretriangulated.instHasFiniteBiproducts CategoryTheory.Functor.hasBiproduct_of_preserves' CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Limits.PreservesBiproductsOfShape.preserves CategoryTheory.Limits.PreservesFiniteBiproducts.preserves CategoryTheory.Functor.preservesFiniteBiproductsOfAdditive CategoryTheory.Pretriangulated.productTriangle_distinguished prop_pi instIsClosedUnderLimitsOfShapeDiscreteOfIsClosedUnderFiniteProductsOfFinite instIsClosedUnderFiniteProductsOfIsTriangulatedOfIsClosedUnderIsomorphisms instIsTriangulatedIsoClosure instIsClosedUnderIsomorphismsIsoClosure
instIsStableUnderShiftExtensionProductInt 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsStableUnderShift extensionProduct Int.instAddMonoid	—	CategoryTheory.Pretriangulated.Triangle.shift_distinguished IsStableUnderShiftBy.le_shift IsStableUnderShift.isStableUnderShiftBy
instIsStableUnderShiftExtensionProductIterInt 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsStableUnderShift extensionProductIter Int.instAddMonoid	—	extensionProductIter_succ instIsStableUnderShiftExtensionProductInt
instIsStableUnderShiftExtensionProductIterInt_1 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsStableUnderShift extensionProductIter Int.instAddMonoid	—	extensionProductIter_zero extensionProductIter_succ instIsStableUnderShiftExtensionProductInt
instIsTriangulatedClosed₁OfIsTriangulated 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulatedClosed₁	—	ext_of_isTriangulatedClosed₂' IsTriangulated.toIsTriangulatedClosed₂ CategoryTheory.Pretriangulated.inv_rot_of_distTriang le_shift IsStableUnderShift.isStableUnderShiftBy IsTriangulated.toIsStableUnderShift
instIsTriangulatedClosed₂IsoClosure 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulatedClosed₂ isoClosure	—	le_isoClosure ext_of_isTriangulatedClosed₂' CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_id
instIsTriangulatedClosed₂MinOfIsClosedUnderIsomorphisms 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulatedClosed₂ CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instMinForall_mathlib SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Prop.instCompleteLinearOrder	—	ext_of_isTriangulatedClosed₂' prop_of_iso ext_of_isTriangulatedClosed₂
instIsTriangulatedClosed₃OfIsTriangulated 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulatedClosed₃	—	ext_of_isTriangulatedClosed₂' IsTriangulated.toIsTriangulatedClosed₂ CategoryTheory.Pretriangulated.rot_of_distTriang le_shift IsStableUnderShift.isStableUnderShiftBy IsTriangulated.toIsStableUnderShift
instIsTriangulatedEssImageOfIsTriangulatedOfFull 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulated CategoryTheory.Functor.essImage	—	IsTriangulatedClosed₂.mk' CategoryTheory.Functor.instIsClosedUnderIsomorphismsEssImage CategoryTheory.Functor.map_surjective CategoryTheory.Pretriangulated.distinguished_cocone_triangle₂ CategoryTheory.Functor.map_distinguished CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_app CategoryTheory.Category.comp_id CategoryTheory.Iso.inv_hom_id CategoryTheory.Functor.map_id CategoryTheory.Limits.isZero_zero CategoryTheory.Functor.IsTriangulated.instPreservesZeroMorphisms
instIsTriangulatedFullSubcategory 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.IsTriangulated FullSubcategory FullSubcategory.category CategoryTheory.Preadditive.fullSubcategory instHasZeroObjectFullSubcategoryOfContainsZero IsTriangulated.toContainsZero hasShift Int.instAddMonoid IsTriangulated.toIsStableUnderShift instAdditiveFullSubcategoryShiftFunctor instPretriangulatedFullSubcategory	—	CategoryTheory.IsTriangulated.of_fully_faithful_triangulated_functor IsTriangulated.toIsStableUnderShift instHasZeroObjectFullSubcategoryOfContainsZero IsTriangulated.toContainsZero instAdditiveFullSubcategoryShiftFunctor instIsTriangulatedFullSubcategoryι full_ι faithful_ι
instIsTriangulatedFullSubcategoryι 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.Functor.IsTriangulated FullSubcategory FullSubcategory.category hasShift Int.instAddMonoid IsTriangulated.toIsStableUnderShift ι commShiftι instHasZeroObjectFullSubcategoryOfContainsZero IsTriangulated.toContainsZero CategoryTheory.Preadditive.fullSubcategory instAdditiveFullSubcategoryShiftFunctor instPretriangulatedFullSubcategory	—	IsTriangulated.toIsStableUnderShift instHasZeroObjectFullSubcategoryOfContainsZero IsTriangulated.toContainsZero instAdditiveFullSubcategoryShiftFunctor
instIsTriangulatedInverseImage 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulated inverseImage	—	IsTriangulatedClosed₂.mk' instIsClosedUnderIsomorphismsInverseImage ext_of_isTriangulatedClosed₂ IsTriangulated.toIsTriangulatedClosed₂ CategoryTheory.Functor.map_distinguished instContainsZeroInverseImageOfIsClosedUnderIsomorphismsOfPreservesZeroMorphismsOfHasZeroObject IsTriangulated.toContainsZero CategoryTheory.Functor.IsTriangulated.instPreservesZeroMorphisms instIsStableUnderShiftInverseImageOfIsClosedUnderIsomorphismsOfCommShift IsTriangulated.toIsStableUnderShift
instIsTriangulatedIsoClosure 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulated isoClosure	—	instContainsZeroIsoClosure IsTriangulated.toContainsZero instIsStableUnderShiftIsoClosure IsTriangulated.toIsStableUnderShift instIsTriangulatedClosed₂IsoClosure IsTriangulated.toIsTriangulatedClosed₂
instIsTriangulatedMapOfIsTriangulatedOfFull 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulated map	—	CategoryTheory.Functor.essImage_ι_comp instIsTriangulatedEssImageOfIsTriangulatedOfFull instHasZeroObjectFullSubcategoryOfContainsZero IsTriangulated.toContainsZero IsTriangulated.toIsStableUnderShift instAdditiveFullSubcategoryShiftFunctor CategoryTheory.Functor.IsTriangulated.instComp instIsTriangulatedFullSubcategoryι CategoryTheory.Functor.Full.comp full_ι
instIsTriangulatedMinOfIsClosedUnderIsomorphisms 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	IsTriangulated CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instMinForall_mathlib SemilatticeInf.toMin Lattice.toSemilatticeInf ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder CompleteLinearOrder.toConditionallyCompleteLinearOrderBot Prop.instCompleteLinearOrder	—	instContainsZeroMinOfIsClosedUnderIsomorphisms IsTriangulated.toContainsZero instIsStableUnderShiftMin IsTriangulated.toIsStableUnderShift instIsTriangulatedClosed₂MinOfIsClosedUnderIsomorphisms IsTriangulated.toIsTriangulatedClosed₂
instRespectsIsoTrW 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.MorphismProperty.RespectsIso trW	—	CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Functor.map_isIso CategoryTheory.Functor.map_inv CategoryTheory.Category.assoc CategoryTheory.IsIso.inv_hom_id CategoryTheory.IsIso.hom_inv_id CategoryTheory.Functor.map_id
inverseImage_trW_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	trW inverseImage CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.Pretriangulated.distinguished_cocone_triangle trW_iff_of_distinguished instIsClosedUnderIsomorphismsInverseImage CategoryTheory.Functor.map_distinguished prop_inverseImage_iff
inverseImage_trW_isInverted 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.MorphismProperty.IsInvertedBy trW inverseImage CategoryTheory.Functor.comp	—	CategoryTheory.Localization.inverts
isTriangulated_lift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.obj	CategoryTheory.Functor.IsTriangulated FullSubcategory FullSubcategory.category hasShift Int.instAddMonoid IsTriangulated.toIsStableUnderShift lift instCommShiftFullSubcategoryLift instHasZeroObjectFullSubcategoryOfContainsZero IsTriangulated.toContainsZero CategoryTheory.Preadditive.fullSubcategory instAdditiveFullSubcategoryShiftFunctor instPretriangulatedFullSubcategory	—	IsTriangulated.toIsStableUnderShift instHasZeroObjectFullSubcategoryOfContainsZero IsTriangulated.toContainsZero instAdditiveFullSubcategoryShiftFunctor CategoryTheory.Functor.isTriangulated_iff_comp_right instCommShiftHomFunctorLiftCompιIso instIsTriangulatedFullSubcategoryι full_ι faithful_ι
le_extensionProductIter 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProductIter	—	monotone'_extensionProductIter
le_extensionProduct_left 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProduct	—	extensionProduct_isoClosure_right exists_prop_of_containsZero CategoryTheory.Pretriangulated.contractible_distinguished CategoryTheory.Limits.isZero_zero
le_extensionProduct_right 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProduct	—	extensionProduct_isoClosure_left exists_prop_of_containsZero CategoryTheory.Pretriangulated.inv_rot_of_distTriang CategoryTheory.Pretriangulated.contractible_distinguished CategoryTheory.Functor.map_isZero CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.Limits.isZero_zero
monotone'_extensionProductIter 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProductIter	—	Nat.le_induction le_refl le_trans extensionProductIter_succ le_extensionProduct_right
monotone_extensionProductIter 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProductIter	—	extensionProductIter_succ le_imp_le_of_le_of_le monotone_extensionProduct_left le_refl monotone_extensionProduct_right
monotone_extensionProduct_left 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProduct	—	—
monotone_extensionProduct_right 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le extensionProduct	—	—
retractClosure_extensionProductIter_retractClosure 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	retractClosure extensionProductIter	—	le_antisymm retractClosure_le_iff instIsStableUnderRetractsRetractClosure extensionProductIter_retractClosure_le monotone_retractClosure monotone_extensionProductIter le_retractClosure
retractClosure_extensionProduct_retractClosure_retractClosure 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	retractClosure extensionProduct	—	le_antisymm retractClosure_le_iff instIsStableUnderRetractsRetractClosure extensionProduct_retractClosure_retractClosure_le monotone_retractClosure le_imp_le_of_le_of_le monotone_extensionProduct_right le_retractClosure le_refl monotone_extensionProduct_left
smul_mem_trW_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	trW Units Int.instMonoid Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Units.instSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup CategoryTheory.Preadditive.homGroup	—	CategoryTheory.MorphismProperty.arrow_mk_iso_iff instRespectsIsoTrW CategoryTheory.Linear.units_smul_comp CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
trW_iff 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	trW Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	—	—
trW_iff' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	trW Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	—	trW_iff CategoryTheory.Pretriangulated.inv_rot_of_distTriang le_shift IsStableUnderShift.isStableUnderShiftBy CategoryTheory.Pretriangulated.rot_of_distTriang
trW_iff_of_distinguished 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	trW CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.mor₁ CategoryTheory.Pretriangulated.Triangle.obj₃	—	CategoryTheory.Pretriangulated.exists_iso_of_arrow_iso prop_of_iso
trW_iff_of_distinguished' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles	trW CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.mor₂ CategoryTheory.Pretriangulated.Triangle.obj₁	—	prop_shift_iff_of_isStableUnderShift trW_iff_of_distinguished CategoryTheory.Pretriangulated.rot_of_distTriang
trW_isoClosure 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	trW isoClosure	—	CategoryTheory.MorphismProperty.ext CategoryTheory.Pretriangulated.isomorphic_distinguished CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Category.assoc CategoryTheory.Iso.hom_inv_id CategoryTheory.Functor.map_id le_isoClosure
trW_of_isIso 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	trW	—	CategoryTheory.MorphismProperty.arrow_mk_iso_iff instRespectsIsoTrW CategoryTheory.MorphismProperty.id_mem instContainsIdentitiesTrWOfContainsZero

CategoryTheory.ObjectProperty.IsTriangulated

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toContainsZero 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.ContainsZero	—	—
toIsStableUnderShift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsStableUnderShift Int.instAddMonoid	—	—
toIsTriangulatedClosed₂ 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.ObjectProperty.IsTriangulatedClosed₂	—	—

CategoryTheory.ObjectProperty.IsTriangulatedClosed₁

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext₁' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃	CategoryTheory.ObjectProperty.isoClosure CategoryTheory.Pretriangulated.Triangle.obj₁	—	—
mk' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.obj₁	CategoryTheory.ObjectProperty.IsTriangulatedClosed₁	—	CategoryTheory.ObjectProperty.isoClosure_eq_self

CategoryTheory.ObjectProperty.IsTriangulatedClosed₂

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext₂' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₃	CategoryTheory.ObjectProperty.isoClosure CategoryTheory.Pretriangulated.Triangle.obj₂	—	—
mk' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.obj₂	CategoryTheory.ObjectProperty.IsTriangulatedClosed₂	—	CategoryTheory.ObjectProperty.isoClosure_eq_self

CategoryTheory.ObjectProperty.IsTriangulatedClosed₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext₃' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂	CategoryTheory.ObjectProperty.isoClosure CategoryTheory.Pretriangulated.Triangle.obj₃	—	—
mk' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle.obj₃	CategoryTheory.ObjectProperty.IsTriangulatedClosed₃	—	CategoryTheory.ObjectProperty.isoClosure_eq_self

CategoryTheory.ObjectProperty.trW

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.obj₃	CategoryTheory.ObjectProperty.trW CategoryTheory.Pretriangulated.Triangle.obj₁ CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.mor₁	—	—
mk' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Pretriangulated.Triangle Set Set.instMembership CategoryTheory.Pretriangulated.distinguishedTriangles CategoryTheory.Pretriangulated.Triangle.obj₁	CategoryTheory.ObjectProperty.trW CategoryTheory.Pretriangulated.Triangle.obj₂ CategoryTheory.Pretriangulated.Triangle.obj₃ CategoryTheory.Pretriangulated.Triangle.mor₂	—	CategoryTheory.ObjectProperty.trW_iff'
shift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.ObjectProperty.trW	CategoryTheory.ObjectProperty.trW CategoryTheory.Functor.obj CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.Functor.map	—	CategoryTheory.ObjectProperty.smul_mem_trW_iff CategoryTheory.Pretriangulated.Triangle.shift_distinguished CategoryTheory.ObjectProperty.le_shift CategoryTheory.ObjectProperty.IsStableUnderShift.isStableUnderShiftBy
unshift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.ObjectProperty.trW CategoryTheory.Functor.obj CategoryTheory.Functor.map	CategoryTheory.ObjectProperty.trW	—	CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.ObjectProperty.instRespectsIsoTrW shift

---

← Back to Index