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`, `instIsStableUnderShiftByIsoClosure`, `instIsStableUnderShiftByMin`, `instIsStableUnderShiftByShiftClosure`, `instIsStableUnderShiftInverseImageOfIsClosedUnderIsomorphismsOfCommShift`, `instIsStableUnderShiftIsoClosure`, `instIsStableUnderShiftMin`, `instIsStableUnderShiftShiftClosure`, `isStableUnderShift_iff_shiftClosure_eq_self`, `le_shift`, `le_shiftClosure`, `monotone_shiftClosure`, `prop_shiftClosure_iff`, `prop_shift_iff`, `prop_shift_iff_of_isStableUnderShift`, `shiftClosure_eq_self`, `shiftClosure_le_iff`, `shift_shift`, `shift_zero`	23
Total	30

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
`IsStableUnderShift` 📖	CompData	11 math math: `isStableUnderShift_iff_shiftClosure_eq_self`, `CategoryTheory.Triangulated.TStructure.instIsStableUnderShiftBoundedInt`, `IsTriangulated.toIsStableUnderShift`, `instIsStableUnderShiftInverseImageOfIsClosedUnderIsomorphismsOfCommShift`, `instIsStableUnderShiftRightOrthogonal`, `CategoryTheory.Triangulated.TStructure.instIsStableUnderShiftPlusInt`, `instIsStableUnderShiftMin`, `instIsStableUnderShiftShiftClosure`, `CategoryTheory.Triangulated.TStructure.instIsStableUnderShiftMinusInt`, `instIsStableUnderShiftIsoClosure`, `instIsStableUnderShiftLeftOrthogonal`
`IsStableUnderShiftBy` 📖	CompData	4 math math: `instIsStableUnderShiftByShiftClosure`, `instIsStableUnderShiftByMin`, `instIsStableUnderShiftByIsoClosure`, `IsStableUnderShift.isStableUnderShiftBy`
`commShiftι` 📖	CompOp	2 math math: `instCommShiftHomFunctorLiftCompιIso`, `instIsTriangulatedFullSubcategoryι`
`hasShift` 📖	CompOp	5 math math: `instCommShiftHomFunctorLiftCompιIso`, `instAdditiveFullSubcategoryShiftFunctor`, `instIsTriangulatedFullSubcategoryι`, `instIsTriangulatedFullSubcategory`, `isTriangulated_lift`
`instCommShiftFullSubcategoryLift` 📖	CompOp	2 math math: `instCommShiftHomFunctorLiftCompιIso`, `isTriangulated_lift`
`shift` 📖	CompOp	8 math math: `prop_shift_iff`, `shift_zero`, `CategoryTheory.Triangulated.TStructure.shift_le`, `instIsClosedUnderIsomorphismsShift`, `CategoryTheory.Triangulated.TStructure.shift_ge`, `shift_shift`, `IsStableUnderShiftBy.le_shift`, `le_shift`
`shiftClosure` 📖	CompOp	9 math math: `isStableUnderShift_iff_shiftClosure_eq_self`, `shiftClosure_eq_self`, `le_shiftClosure`, `instIsStableUnderShiftByShiftClosure`, `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`	—	—
`instIsStableUnderShiftByIsoClosure` 📖	mathematical	—	`IsStableUnderShiftBy` `isoClosure`	—	`le_shift`
`instIsStableUnderShiftByMin` 📖	mathematical	—	`IsStableUnderShiftBy` `CategoryTheory.ObjectProperty` `CategoryTheory.Category.toCategoryStruct` `Pi.instMinForall_mathlib` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `Prop.instCompleteLattice`	—	`le_shift`
`instIsStableUnderShiftByShiftClosure` 📖	mathematical	—	`IsStableUnderShiftBy` `shiftClosure`	—	—
`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` `CompleteLattice.toLattice` `Prop.instCompleteLattice`	—	`instIsStableUnderShiftByMin` `IsStableUnderShift.isStableUnderShiftBy`
`instIsStableUnderShiftShiftClosure` 📖	mathematical	—	`IsStableUnderShift` `shiftClosure`	—	`instIsStableUnderShiftByShiftClosure`
`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`	`shiftClosure`	—	—
`prop_shiftClosure_iff` 📖	mathematical	—	`shiftClosure`	—	—
`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_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`
`shift_shift` 📖	mathematical	`AddSemigroup.toAdd` `AddMonoid.toAddSemigroup`	`shift`	—	`prop_iff_of_iso`
`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