Subcategory

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

Statistics

Metric	Count
Definitions IsTriangulated, IsTriangulatedClosed₁, IsTriangulatedClosed₂, IsTriangulatedClosed₃, instPretriangulatedFullSubcategory, trW	6
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₃', instContainsIdentitiesTrWOfContainsZero, instHasLeftCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated, instHasRightCalculusOfFractionsTrWOfIsTriangulatedOfIsTriangulated, instIsClosedUnderBinaryProductsOfIsTriangulatedOfIsClosedUnderIsomorphisms, instIsClosedUnderFiniteProductsOfIsTriangulatedOfIsClosedUnderIsomorphisms, instIsCompatibleWithShiftTrWIntOfIsStableUnderShift, instIsCompatibleWithTriangulationTrWOfIsTriangulatedOfIsTriangulated, instIsMultiplicativeTrWOfIsTriangulatedOfIsTriangulated, instIsStableUnderFiniteProductsTrWOfIsTriangulated, instIsTriangulatedClosed₁OfIsTriangulated, instIsTriangulatedClosed₂IsoClosure, instIsTriangulatedClosed₂MinOfIsClosedUnderIsomorphisms, instIsTriangulatedClosed₃OfIsTriangulated, instIsTriangulatedEssImageOfIsTriangulatedOfFull, instIsTriangulatedFullSubcategory, instIsTriangulatedFullSubcategoryι, instIsTriangulatedInverseImage, instIsTriangulatedIsoClosure, instIsTriangulatedMapOfIsTriangulatedOfFull, instIsTriangulatedMinOfIsClosedUnderIsomorphisms, instRespectsIsoTrW, inverseImage_trW_iff, inverseImage_trW_isInverted, isTriangulated_lift, 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	50
Total	56

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
IsTriangulated 📖	CompData	9 math math: instIsTriangulatedIsoClosure, CategoryTheory.Functor.instIsTriangulatedHomologicalKernel, instIsTriangulatedEssImageOfIsTriangulatedOfFull, instIsTriangulatedLeftOrthogonalOfIsStableUnderShiftInt, instIsTriangulatedRightOrthogonalOfIsStableUnderShiftInt, HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic, instIsTriangulatedMapOfIsTriangulatedOfFull, instIsTriangulatedMinOfIsClosedUnderIsomorphisms, instIsTriangulatedInverseImage
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
instPretriangulatedFullSubcategory 📖	CompOp	3 math math: instIsTriangulatedFullSubcategoryι, instIsTriangulatedFullSubcategory, isTriangulated_lift
trW 📖	CompOp	24 math math: inverseImage_trW_isInverted, 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, 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₃'
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
instIsCompatibleWithShiftTrWIntOfIsStableUnderShift 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	CategoryTheory.MorphismProperty.IsCompatibleWithShift trW	—	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
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 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 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 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_ι
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	—	—
trW_iff' 📖	mathematical	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid	trW	—	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	—	—
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.Functor.obj CategoryTheory.Functor.map	—	CategoryTheory.ObjectProperty.smul_mem_trW_iff CategoryTheory.Pretriangulated.Triangle.shift_distinguished CategoryTheory.ObjectProperty.le_shift CategoryTheory.ObjectProperty.IsStableUnderShift.isStableUnderShiftBy
unshift 📖	—	CategoryTheory.Functor.Additive CategoryTheory.shiftFunctor Int.instAddMonoid CategoryTheory.ObjectProperty.trW CategoryTheory.Functor.obj CategoryTheory.Functor.map	—	—	CategoryTheory.MorphismProperty.arrow_mk_iso_iff CategoryTheory.ObjectProperty.instRespectsIsoTrW shift

---

← Back to Index