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.{v_1, 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 (X⟦a⟧)

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

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsShift {C : Type u_1} [Category.{v_1, 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.{v_1, 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.{v_1, 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

theorem CategoryTheory.ObjectProperty.shift_sup {C : Type u_1} [Category.{v_1, u_1} C] (P Q : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) : (P ⊔ Q).shift a = P.shift a ⊔ Q.shift a

theorem CategoryTheory.ObjectProperty.shift_iSup {C : Type u_1} [Category.{v_1, u_1} C] {A : Type u_2} [AddMonoid A] [HasShift C A] {ι : Sort u_4} (P : ι → ObjectProperty C) (a : A) : (⨆ (i : ι), P i).shift a = ⨆ (i : ι), (P i).shift a

class CategoryTheory.ObjectProperty.IsStableUnderShiftBy {C : Type u_1} [Category.{v_1, 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.{v_1, 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.instNonemptyShiftOfIsStableUnderShiftBy {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) [P.IsStableUnderShiftBy a] [P.Nonempty] : (P.shift a).Nonempty

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftByBot {C : Type u_1} [Category.{v_1, u_1} C] {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) : ⊥.IsStableUnderShiftBy a

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftByTop {C : Type u_1} [Category.{v_1, u_1} C] {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) : ⊤.IsStableUnderShiftBy a

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

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftByMin {C : Type u_1} [Category.{v_1, u_1} C] (P Q : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) [P.IsStableUnderShiftBy a] [Q.IsStableUnderShiftBy a] : (P ⊓ Q).IsStableUnderShiftBy a

class CategoryTheory.ObjectProperty.IsStableUnderShift {C : Type u_1} [Category.{v_1, 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.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] [P.IsStableUnderShift A] : P.isoClosure.IsStableUnderShift A

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftMin {C : Type u_1} [Category.{v_1, u_1} C] (P Q : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] [P.IsStableUnderShift A] [Q.IsStableUnderShift A] : (P ⊓ Q).IsStableUnderShift A

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftBot {C : Type u_1} [Category.{v_1, u_1} C] {A : Type u_2} [AddMonoid A] [HasShift C A] : ⊥.IsStableUnderShift A

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftTop {C : Type u_1} [Category.{v_1, u_1} C] {A : Type u_2} [AddMonoid A] [HasShift C A] : ⊤.IsStableUnderShift A

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

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

The closure by shifts and isomorphism of a predicate on objects in a category.

Equations

• P.shiftClosure A X = ∃ (Y : C) (a : A) (x : X ≅ Y⟦a⟧), P Y

theorem CategoryTheory.ObjectProperty.prop_shiftClosure_iff {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (X : C) : P.shiftClosure A X ↔ ∃ (Y : C) (a : A) (x : X ≅ Y⟦a⟧), P Y

theorem CategoryTheory.ObjectProperty.le_shiftClosure {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] : P ≤ P.shiftClosure A

instance CategoryTheory.ObjectProperty.instNonemptyShiftClosure {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] [P.Nonempty] : (P.shiftClosure A).Nonempty

theorem CategoryTheory.ObjectProperty.monotone_shiftClosure {C : Type u_1} [Category.{v_1, u_1} C] {P Q : ObjectProperty C} {A : Type u_2} [AddMonoid A] [HasShift C A] (h : P ≤ Q) : P.shiftClosure A ≤ Q.shiftClosure A

theorem CategoryTheory.ObjectProperty.shiftClosure_eq_self {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] [P.IsClosedUnderIsomorphisms] [P.IsStableUnderShift A] : P.shiftClosure A = P

@[simp]

theorem CategoryTheory.ObjectProperty.shiftClosure_bot {C : Type u_1} [Category.{v_1, u_1} C] {A : Type u_2} [AddMonoid A] [HasShift C A] : ⊥.shiftClosure A = ⊥

@[simp]

theorem CategoryTheory.ObjectProperty.shiftClosure_top {C : Type u_1} [Category.{v_1, u_1} C] {A : Type u_2} [AddMonoid A] [HasShift C A] : ⊤.shiftClosure A = ⊤

theorem CategoryTheory.ObjectProperty.shiftClosure_le_iff {C : Type u_1} [Category.{v_1, u_1} C] (P Q : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] [Q.IsClosedUnderIsomorphisms] [Q.IsStableUnderShift A] : P.shiftClosure A ≤ Q ↔ P ≤ Q

instance CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsShiftClosure {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] : (P.shiftClosure A).IsClosedUnderIsomorphisms

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftByShiftClosure {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] (a : A) : (P.shiftClosure A).IsStableUnderShiftBy a

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftShiftClosure {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] : (P.shiftClosure A).IsStableUnderShift A

theorem CategoryTheory.ObjectProperty.isStableUnderShift_iff_shiftClosure_eq_self {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] [P.IsClosedUnderIsomorphisms] : P.IsStableUnderShift A ↔ P.shiftClosure A = P

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftISupShiftOfIsClosedUnderIsomorphisms {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] (G : Type u_4) [AddGroup G] [HasShift C G] : (⨆ (a : G), P.shift a).IsStableUnderShift G

theorem CategoryTheory.ObjectProperty.shiftClosure_eq_iSup {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) [P.IsClosedUnderIsomorphisms] (G : Type u_4) [AddGroup G] [HasShift C G] : P.shiftClosure G = ⨆ (x : G), P.shift x

@[irreducible]

noncomputable instance CategoryTheory.ObjectProperty.hasShift {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] : HasShift P.FullSubcategory A

Equations

• P.hasShift = P.fullyFaithfulι.hasShift (fun (n : A) => P.lift (P.ι.comp (CategoryTheory.shiftFunctor C n)) ⋯) fun (x : A) => P.liftCompιIso (P.ι.comp (CategoryTheory.shiftFunctor C x)) ⋯

@[irreducible]

instance CategoryTheory.ObjectProperty.commShiftι {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] : P.ι.CommShift A

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance CategoryTheory.ObjectProperty.commShiftLift {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] {E : Type u_3} [Category.{v_2, u_3} E] [HasShift E A] [P.IsStableUnderShift A] (F : Functor E C) (hF : ∀ (X : E), P (F.obj X)) [F.CommShift A] : (P.lift F hF).CommShift A

Equations

• P.commShiftLift F hF = CategoryTheory.Functor.CommShift.ofComp (P.liftCompιIso F hF) A

instance CategoryTheory.ObjectProperty.commShift_liftCompιIso_hom {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] {E : Type u_3} [Category.{v_2, u_3} E] [HasShift E A] [P.IsStableUnderShift A] (F : Functor E C) (hF : ∀ (X : E), P (F.obj X)) [F.CommShift A] : NatTrans.CommShift (P.liftCompιIso F hF).hom A

instance CategoryTheory.ObjectProperty.instIsStableUnderShiftInverseImageOfIsClosedUnderIsomorphismsOfCommShift {C : Type u_1} [Category.{v_1, u_1} C] (P : ObjectProperty C) {A : Type u_2} [AddMonoid A] [HasShift C A] {E : Type u_3} [Category.{v_2, u_3} E] [HasShift E A] [P.IsStableUnderShift A] [P.IsClosedUnderIsomorphisms] (F : Functor E C) [F.CommShift A] : (P.inverseImage F).IsStableUnderShift A