Properties of objects on categories equipped with shift

Given a predicate P : ObjectProperty C on objects of a category equipped with a shift by A, we define shifted properties of objects P.shift a for all a : A. We also introduce a typeclass P.IsStableUnderShift A to say that P X implies P (X⟦a⟧) for all a : A.

def CategoryTheory.ObjectProperty.shift {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) : ObjectProperty C

Given a predicate P : C → Prop on objects of a category equipped with a shift by A, this is the predicate which is satisfied by X if P (X⟦a⟧).

Equations

• P.shift a X = P ((CategoryTheory.shiftFunctor C a).obj X)

theorem CategoryTheory.ObjectProperty.prop_shift_iff {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) (X : C) : P.shift a X ↔ P ((shiftFunctor C a).obj X)

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsShift {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) [P.IsClosedUnderIsomorphisms] : (P.shift a).IsClosedUnderIsomorphisms

@[simp]

theorem CategoryTheory.ObjectProperty.shift_zero {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) (A : Type u_2) [AddMonoid A] [HasShift C A] [P.IsClosedUnderIsomorphisms] : P.shift 0 = P

theorem CategoryTheory.ObjectProperty.shift_shift {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a b c : A) (h : a + b = c) [P.IsClosedUnderIsomorphisms] : (P.shift b).shift a = P.shift c

class CategoryTheory.ObjectProperty.IsStableUnderShiftBy {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) : Prop

P : ObjectProperty C is stable under the shift by a : A if P X implies P X⟦a⟧.

• le_shift : P ≤ P.shift a

theorem CategoryTheory.ObjectProperty.le_shift {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) [P.IsStableUnderShiftBy a] : P ≤ P.shift a

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftByIsoClosure {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) [P.IsStableUnderShiftBy a] : P.isoClosure.IsStableUnderShiftBy a

class CategoryTheory.ObjectProperty.IsStableUnderShift {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) (A : Type u_2) [AddMonoid A] [HasShift C A] : Prop

P : ObjectProperty C is stable under the shift by A if P X implies P X⟦a⟧ for any a : A.

• isStableUnderShiftBy (a : A) : P.IsStableUnderShiftBy a

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftIsoClosure {C : Type u_1} [Category.{u_3, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] [P.IsStableUnderShift A] : P.isoClosure.IsStableUnderShift A

theorem CategoryTheory.ObjectProperty.prop_shift_iff_of_isStableUnderShift {C : Type u_1} [Category.{u_4, u_1} C] (P : ObjectProperty C) {G : Type u_3} [AddGroup G] [HasShift C G] [P.IsStableUnderShift G] [P.IsClosedUnderIsomorphisms] (X : C) (g : G) : P ((shiftFunctor C g).obj X) ↔ P X