Closure operators and shifts #
In this file, we collect facts relating being stable under shifts with closure properties of object properties.
instance CategoryTheory.ObjectProperty.instIsStableUnderShiftRetractClosure {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] [P.IsStableUnderShift A] :
instance CategoryTheory.ObjectProperty.instIsStableUnderShiftLimitsClosure {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddGroup A] [HasShift C A] {α : Type u_3} {J : α → Type u_4} [(i : α) → Category.{u_5, u_4} (J i)] [P.IsStableUnderShift A] :
(P.limitsClosure J).IsStableUnderShift A