Documentation

Mathlib.CategoryTheory.ObjectProperty.Shift

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 ((CategoryTheory.shiftFunctor C a).obj X)

Instances For

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 ((shiftFunctor C a).obj X)

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

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) :

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

le_shift : P ≤ P.shift a

Instances

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.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] :

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

Instances

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

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 ((shiftFunctor C g).obj X) ↔ 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 ≅ (CategoryTheory.shiftFunctor C a).obj Y), P Y

Instances For

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 ≅ (shiftFunctor C a).obj Y), 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

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

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

@[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.instCommShiftFullSubcategoryLift {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.instCommShiftFullSubcategoryLift F hF = CategoryTheory.Functor.CommShift.ofComp (P.liftCompιIso F hF) A

instance CategoryTheory.ObjectProperty.instCommShiftHomFunctorLiftCompιIso {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