Shift

📁 Source: Mathlib/CategoryTheory/ObjectProperty/Shift.lean

Statistics

Metric	Count
Definitions `IsStableUnderShift`, `IsStableUnderShiftBy`, `commShiftι`, `hasShift`, `instCommShiftFullSubcategoryLift`, `shift`, `shiftClosure`	7
Theorems `isStableUnderShiftBy`, `le_shift`, `instCommShiftHomFunctorLiftCompιIso`, `instIsClosedUnderIsomorphismsShift`, `instIsClosedUnderIsomorphismsShiftClosure`, `instIsStableUnderShiftBot`, `instIsStableUnderShiftByBot`, `instIsStableUnderShiftByIsoClosure`, `instIsStableUnderShiftByMin`, `instIsStableUnderShiftByShiftClosure`, `instIsStableUnderShiftByTop`, `instIsStableUnderShiftISupShiftOfIsClosedUnderIsomorphisms`, `instIsStableUnderShiftInverseImageOfIsClosedUnderIsomorphismsOfCommShift`, `instIsStableUnderShiftIsoClosure`, `instIsStableUnderShiftMin`, `instIsStableUnderShiftShiftClosure`, `instIsStableUnderShiftTop`, `isStableUnderShift_iff_shiftClosure_eq_self`, `le_shift`, `le_shiftClosure`, `monotone_shiftClosure`, `prop_shiftClosure_iff`, `prop_shift_iff`, `prop_shift_iff_of_isStableUnderShift`, `shiftClosure_bot`, `shiftClosure_eq_iSup`, `shiftClosure_eq_self`, `shiftClosure_le_iff`, `shiftClosure_top`, `shift_iSup`, `shift_shift`, `shift_sup`, `shift_zero`	33
Total	40

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`IsStableUnderShift` 📖	CompData	18 math math: `isStableUnderShift_iff_shiftClosure_eq_self`, `CategoryTheory.Triangulated.TStructure.instIsStableUnderShiftBoundedInt`, `IsTriangulated.toIsStableUnderShift`, `instIsStableUnderShiftInverseImageOfIsClosedUnderIsomorphismsOfCommShift`, `instIsStableUnderShiftRightOrthogonal`, `CategoryTheory.Triangulated.TStructure.instIsStableUnderShiftPlusInt`, `instIsStableUnderShiftExtensionProductIterInt_1`, `instIsStableUnderShiftBot`, `instIsStableUnderShiftTop`, `instIsStableUnderShiftMin`, `instIsStableUnderShiftShiftClosure`, `CategoryTheory.Triangulated.TStructure.instIsStableUnderShiftMinusInt`, `instIsStableUnderShiftIsoClosure`, `instIsStableUnderShiftExtensionProductInt`, `instIsStableUnderShiftExtensionProductIterInt`, `instIsStableUnderShiftISupShiftOfIsClosedUnderIsomorphisms`, `instIsStableUnderShiftLeftOrthogonal`, `CochainComplex.Plus.instIsStableUnderShiftIntPlus`
`IsStableUnderShiftBy` 📖	CompData	6 math math: `instIsStableUnderShiftByShiftClosure`, `instIsStableUnderShiftByBot`, `instIsStableUnderShiftByMin`, `instIsStableUnderShiftByTop`, `instIsStableUnderShiftByIsoClosure`, `IsStableUnderShift.isStableUnderShiftBy`
`commShiftι` 📖	CompOp	2 math math: `instCommShiftHomFunctorLiftCompιIso`, `instIsTriangulatedFullSubcategoryι`
`hasShift` 📖	CompOp	7 math math: `instCommShiftHomFunctorLiftCompιIso`, `tStructure_isGE_iff`, `instAdditiveFullSubcategoryShiftFunctor`, `instIsTriangulatedFullSubcategoryι`, `tStructure_isLE_iff`, `instIsTriangulatedFullSubcategory`, `isTriangulated_lift`
`instCommShiftFullSubcategoryLift` 📖	CompOp	2 math math: `instCommShiftHomFunctorLiftCompιIso`, `isTriangulated_lift`
`shift` 📖	CompOp	12 math math: `prop_shift_iff`, `shift_zero`, `shiftClosure_eq_iSup`, `CategoryTheory.Triangulated.TStructure.shift_le`, `instIsClosedUnderIsomorphismsShift`, `CategoryTheory.Triangulated.TStructure.shift_ge`, `shift_shift`, `IsStableUnderShiftBy.le_shift`, `instIsStableUnderShiftISupShiftOfIsClosedUnderIsomorphisms`, `shift_sup`, `shift_iSup`, `le_shift`
`shiftClosure` 📖	CompOp	12 math math: `isStableUnderShift_iff_shiftClosure_eq_self`, `shiftClosure_eq_self`, `le_shiftClosure`, `shiftClosure_bot`, `instIsStableUnderShiftByShiftClosure`, `shiftClosure_eq_iSup`, `shiftClosure_top`, `shiftClosure_le_iff`, `monotone_shiftClosure`, `instIsStableUnderShiftShiftClosure`, `instIsClosedUnderIsomorphismsShiftClosure`, `prop_shiftClosure_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instCommShiftHomFunctorLiftCompιIso` 📖	mathematical	`CategoryTheory.Functor.obj`	`CategoryTheory.NatTrans.CommShift` `CategoryTheory.Functor.comp` `FullSubcategory` `FullSubcategory.category` `lift` `ι` `CategoryTheory.Iso.hom` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `liftCompιIso` `CategoryTheory.Functor.CommShift.comp` `hasShift` `instCommShiftFullSubcategoryLift` `commShiftι`	—	`CategoryTheory.Functor.CommShift.ofComp_compatibility` `full_ι` `faithful_ι`
`instIsClosedUnderIsomorphismsShift` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `shift`	—	`prop_of_iso`
`instIsClosedUnderIsomorphismsShiftClosure` 📖	mathematical	—	`IsClosedUnderIsomorphisms` `shiftClosure`	—	—
`instIsStableUnderShiftBot` 📖	mathematical	—	`IsStableUnderShift` `Bot.bot` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instBotForall` `BooleanAlgebra.toBot` `Prop.instBooleanAlgebra`	—	`instIsStableUnderShiftByBot`
`instIsStableUnderShiftByBot` 📖	mathematical	—	`IsStableUnderShiftBy` `Bot.bot` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instBotForall` `BooleanAlgebra.toBot` `Prop.instBooleanAlgebra`	—	—
`instIsStableUnderShiftByIsoClosure` 📖	mathematical	—	`IsStableUnderShiftBy` `isoClosure`	—	`le_shift`
`instIsStableUnderShiftByMin` 📖	mathematical	—	`IsStableUnderShiftBy` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder`	—	`le_shift`
`instIsStableUnderShiftByShiftClosure` 📖	mathematical	—	`IsStableUnderShiftBy` `shiftClosure`	—	—
`instIsStableUnderShiftByTop` 📖	mathematical	—	`IsStableUnderShiftBy` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	—
`instIsStableUnderShiftISupShiftOfIsClosedUnderIsomorphisms` 📖	mathematical	—	`IsStableUnderShift` `iSup` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.supSet` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder` `shift` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`shift_iSup` `prop_iSup_iff` `shift_shift` `add_neg_cancel_left`
`instIsStableUnderShiftInverseImageOfIsClosedUnderIsomorphismsOfCommShift` 📖	mathematical	—	`IsStableUnderShift` `inverseImage`	—	`prop_of_iso` `le_shift` `IsStableUnderShift.isStableUnderShiftBy`
`instIsStableUnderShiftIsoClosure` 📖	mathematical	—	`IsStableUnderShift` `isoClosure`	—	`instIsStableUnderShiftByIsoClosure` `IsStableUnderShift.isStableUnderShiftBy`
`instIsStableUnderShiftMin` 📖	mathematical	—	`IsStableUnderShift` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder`	—	`instIsStableUnderShiftByMin` `IsStableUnderShift.isStableUnderShiftBy`
`instIsStableUnderShiftShiftClosure` 📖	mathematical	—	`IsStableUnderShift` `shiftClosure`	—	`instIsStableUnderShiftByShiftClosure`
`instIsStableUnderShiftTop` 📖	mathematical	—	`IsStableUnderShift` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	`instIsStableUnderShiftByTop`
`isStableUnderShift_iff_shiftClosure_eq_self` 📖	mathematical	—	`IsStableUnderShift` `shiftClosure`	—	`shiftClosure_eq_self` `instIsStableUnderShiftShiftClosure`
`le_shift` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `shift`	—	`IsStableUnderShiftBy.le_shift`
`le_shiftClosure` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `shiftClosure`	—	—
`monotone_shiftClosure` 📖	mathematical	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le`	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `shiftClosure`	—	—
`prop_shiftClosure_iff` 📖	mathematical	—	`shiftClosure` `CategoryTheory.Iso` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor`	—	—
`prop_shift_iff` 📖	mathematical	—	`shift` `CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor`	—	—
`prop_shift_iff_of_isStableUnderShift` 📖	mathematical	—	`CategoryTheory.Functor.obj` `CategoryTheory.shiftFunctor` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`shift_zero` `shift_shift` `add_neg_cancel` `le_shift` `IsStableUnderShift.isStableUnderShiftBy`
`shiftClosure_bot` 📖	mathematical	—	`shiftClosure` `Bot.bot` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instBotForall` `BooleanAlgebra.toBot` `Prop.instBooleanAlgebra`	—	`shiftClosure_eq_self` `instIsClosedUnderIsomorphismsBot` `instIsStableUnderShiftBot`
`shiftClosure_eq_iSup` 📖	mathematical	—	`shiftClosure` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `iSup` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.supSet` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder` `shift`	—	`le_antisymm` `shiftClosure_le_iff` `instIsClosedUnderIsomorphismsISup` `instIsClosedUnderIsomorphismsShift` `instIsStableUnderShiftISupShiftOfIsClosedUnderIsomorphisms` `shift_zero` `le_iSup` `prop_iSup_iff`
`shiftClosure_eq_self` 📖	mathematical	—	`shiftClosure`	—	`le_antisymm` `prop_of_iso` `le_shift` `IsStableUnderShift.isStableUnderShiftBy` `le_shiftClosure`
`shiftClosure_le_iff` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `shiftClosure`	—	`LE.le.trans` `le_shiftClosure` `monotone_shiftClosure` `shiftClosure_eq_self` `le_refl`
`shiftClosure_top` 📖	mathematical	—	`shiftClosure` `Top.top` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	`shiftClosure_eq_self` `instIsClosedUnderIsomorphismsTop` `instIsStableUnderShiftTop`
`shift_iSup` 📖	mathematical	—	`shift` `iSup` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.supSet` `ConditionallyCompletePartialOrderSup.toSupSet` `ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup` `ConditionallyCompleteLattice.toConditionallyCompletePartialOrder` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder`	—	—
`shift_shift` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`shift`	—	`prop_iff_of_iso`
`shift_sup` 📖	mathematical	—	`shift` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMaxForall_mathlib` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `ConditionallyCompleteLattice.toLattice` `ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice` `ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder` `CompleteLinearOrder.toConditionallyCompleteLinearOrderBot` `Prop.instCompleteLinearOrder`	—	—
`shift_zero` 📖	mathematical	—	`shift` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`prop_iff_of_iso`

CategoryTheory.ObjectProperty.IsStableUnderShift

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isStableUnderShiftBy` 📖	mathematical	—	`CategoryTheory.ObjectProperty.IsStableUnderShiftBy`	—	—

CategoryTheory.ObjectProperty.IsStableUnderShiftBy

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_shift` 📖	mathematical	—	`CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.hasLe` `Prop.le` `CategoryTheory.ObjectProperty.shift`	—	—

---

← Back to Index