The pointwise shift on a functor category

A shift on Y induces one on X ⥤ Y, by postcomposition: G⟦n⟧ = G ⋙ Y⟦n⟧. Mathlib does not carry this instance at the pinned revision, and this file adds it.

Why the construction is short

Every comparison the shift needs is already an identity of functors in Mathlib, not merely an isomorphism: whiskeringRight_obj_id and whiskeringRight_obj_comp are both rfl. So the zero and add isomorphisms are the images of shiftFunctorZero Y and shiftFunctorAdd Y under whiskeringRight, with no transport, and the three coherence axioms of ShiftMkCore reduce componentwise to their counterparts on Y.

The evaluation functors commute with the shift on the nose

(evaluation X Y).obj E sends G to G.obj E, so it sends G ⋙ Y⟦n⟧ to (G.obj E)⟦n⟧: the two sides of its commutation isomorphism are equal, and Iso.refl is a CommShift structure for it. This is what lets a functor K ⥤ (X ⥤ Y) that commutes with the shift be evaluated at a source object and still commute with the shift, by Mathlib's composition instance alone.

Naturality of a whole family, for free

A family of functors F : K ⥤ (X ⥤ Y) equipped with F.CommShift A carries one isomorphism shiftFunctor K n ⋙ F ≅ F ⋙ shiftFunctor (X ⥤ Y) n in the functor category, so its components at a source object are natural in that object by construction, and the zero and addition laws are Mathlib's.

Triangulated/ExactFunctorFamily.lean therefore extends this ordinary CommShift instead of storing evaluated structures and their naturality by hand.

For F : K ⥤ X ⥤ Y carrying Mathlib's CommShift₂, the two explicit adapters below assemble the shift data in either variable into a CommShift on F or F.flip. Composing those structures with strict evaluation gives exactly the partial structures selected by CommShift₂; the equality is a theorem, not an instance, so consumers can transport data without creating a typeclass diamond.

def CategoryTheory.functorCategoryShiftMkCore (X : Type u) [Category.{v, u} X] (Y : Type u') [Category.{v', u'} Y] (A : Type w) [AddMonoid A] [HasShift Y A] : ShiftMkCore (Functor X Y) A

The pointwise shift on X ⥤ Y: shifting by n is postcomposition with Y⟦n⟧.

The three coherence fields are the coherences of the shift on Y, applied at G.obj E; the whiskering comparisons contribute nothing because they are identities.

Equations

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

@[implicit_reducible]

instance CategoryTheory.functorCategoryHasShift (X : Type u) [Category.{v, u} X] (Y : Type u') [Category.{v', u'} Y] (A : Type w) [AddMonoid A] [HasShift Y A] : HasShift (Functor X Y) A

A functor category inherits the shift of its target, pointwise.

Equations

• CategoryTheory.functorCategoryHasShift X Y A = CategoryTheory.hasShiftMk (CategoryTheory.Functor X Y) A (CategoryTheory.functorCategoryShiftMkCore X Y A)

@[simp]

theorem CategoryTheory.functorCategory_shiftFunctor_obj {X : Type u} [Category.{v, u} X] {Y : Type u'} [Category.{v', u'} Y] {A : Type w} [AddMonoid A] [HasShift Y A] (n : A) (G : Functor X Y) : (shiftFunctor (Functor X Y) n).obj G = G.comp (shiftFunctor Y n)

theorem CategoryTheory.functorCategory_shiftFunctor_obj_obj {X : Type u} [Category.{v, u} X] {Y : Type u'} [Category.{v', u'} Y] {A : Type w} [AddMonoid A] [HasShift Y A] (n : A) (G : Functor X Y) (E : X) : ((shiftFunctor (Functor X Y) n).obj G).obj E = (shiftFunctor Y n).obj (G.obj E)

@[simp]

theorem CategoryTheory.functorCategory_shiftFunctor_map_app {X : Type u} [Category.{v, u} X] {Y : Type u'} [Category.{v', u'} Y] {A : Type w} [AddMonoid A] [HasShift Y A] (n : A) {G G' : Functor X Y} (τ : G ⟶ G') (E : X) : ((shiftFunctor (Functor X Y) n).map τ).app E = (shiftFunctor Y n).map (τ.app E)

theorem CategoryTheory.functorCategory_shiftFunctorZero_hom_app {X : Type u} [Category.{v, u} X] {Y : Type u'} [Category.{v', u'} Y] {A : Type w} [AddMonoid A] [HasShift Y A] (G : Functor X Y) (E : X) : ((shiftFunctorZero (Functor X Y) A).hom.app G).app E = (shiftFunctorZero Y A).hom.app (G.obj E)

theorem CategoryTheory.functorCategory_shiftFunctorZero_inv_app {X : Type u} [Category.{v, u} X] {Y : Type u'} [Category.{v', u'} Y] {A : Type w} [AddMonoid A] [HasShift Y A] (G : Functor X Y) (E : X) : ((shiftFunctorZero (Functor X Y) A).inv.app G).app E = (shiftFunctorZero Y A).inv.app (G.obj E)

theorem CategoryTheory.functorCategory_shiftFunctorAdd_hom_app {X : Type u} [Category.{v, u} X] {Y : Type u'} [Category.{v', u'} Y] {A : Type w} [AddMonoid A] [HasShift Y A] (n m : A) (G : Functor X Y) (E : X) : ((shiftFunctorAdd (Functor X Y) n m).hom.app G).app E = (shiftFunctorAdd Y n m).hom.app (G.obj E)

theorem CategoryTheory.functorCategory_shiftFunctorAdd_inv_app {X : Type u} [Category.{v, u} X] {Y : Type u'} [Category.{v', u'} Y] {A : Type w} [AddMonoid A] [HasShift Y A] (n m : A) (G : Functor X Y) (E : X) : ((shiftFunctorAdd (Functor X Y) n m).inv.app G).app E = (shiftFunctorAdd Y n m).inv.app (G.obj E)

@[implicit_reducible]

instance CategoryTheory.evaluationCommShift (X : Type u) [Category.{v, u} X] (Y : Type u') [Category.{v', u'} Y] (A : Type w) [AddMonoid A] [HasShift Y A] (E : X) : ((evaluation X Y).obj E).CommShift A

Evaluation commutes with the pointwise shift on the nose.

(G ⋙ Y⟦n⟧).obj E and (G.obj E)⟦n⟧ are the same object, so the commutation isomorphism is the identity and both coherence laws reduce to the corresponding law on Y.

Equations

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

@[simp]

theorem CategoryTheory.evaluationCommShift_iso_hom_app (X : Type u) [Category.{v, u} X] (Y : Type u') [Category.{v', u'} Y] (A : Type w) [AddMonoid A] [HasShift Y A] (E : X) (n : A) (G : Functor X Y) : (Functor.commShiftIso ((evaluation X Y).obj E) n).hom.app G = CategoryStruct.id (((shiftFunctor (Functor X Y) n).comp ((evaluation X Y).obj E)).obj G)

@[reducible]

noncomputable def CategoryTheory.Functor.CommShift₂.firstFamilyCommShift {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] {M : Type uM} [AddCommMonoid M] [HasShift K M] [HasShift X M] [HasShift Y M] {F : Functor K (Functor X Y)} (h : CommShift₂Setup Y M) [F.CommShift₂ h] : F.CommShift M

Assemble the shift coherence in the first variable of a bifunctor into an ordinary CommShift structure on its functor-valued family.

This is an explicit definition rather than an instance: a consumer may have already selected another CommShift structure on F.

Equations

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

theorem CategoryTheory.Functor.CommShift₂.firstFamilyCommShift_iso_hom_app_app {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] {M : Type uM} [AddCommMonoid M] [HasShift K M] [HasShift X M] [HasShift Y M] {F : Functor K (Functor X Y)} (h : CommShift₂Setup Y M) [F.CommShift₂ h] (n : M) (A : K) (E : X) : ((commShiftIso F n).hom.app A).app E = (commShiftIso (F.flip.obj E) n).hom.app A

The first-family shift comparison evaluates to the partial comparison selected by CommShift₂.

@[reducible]

noncomputable def CategoryTheory.Functor.CommShift₂.secondFamilyCommShift {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] {M : Type uM} [AddCommMonoid M] [HasShift K M] [HasShift X M] [HasShift Y M] {F : Functor K (Functor X Y)} (h : CommShift₂Setup Y M) [F.CommShift₂ h] : F.flip.CommShift M

Assemble the shift coherence in the second variable of a bifunctor into an ordinary CommShift structure on the flipped functor-valued family.

Equations

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

theorem CategoryTheory.Functor.CommShift₂.secondFamilyCommShift_iso_hom_app_app {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] {M : Type uM} [AddCommMonoid M] [HasShift K M] [HasShift X M] [HasShift Y M] {F : Functor K (Functor X Y)} (h : CommShift₂Setup Y M) [F.CommShift₂ h] (n : M) (E : X) (A : K) : ((commShiftIso F.flip n).hom.app E).app A = (commShiftIso (F.obj A) n).hom.app E

The second-family shift comparison evaluates to the partial comparison selected by CommShift₂.

@[reducible]

noncomputable def CategoryTheory.Functor.CommShift₂.firstFamilyEvaluationCommShift {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] {M : Type uM} [AddCommMonoid M] [HasShift K M] [HasShift X M] [HasShift Y M] {F : Functor K (Functor X Y)} (h : CommShift₂Setup Y M) [F.CommShift₂ h] (E : X) : (F.comp ((evaluation X Y).obj E)).CommShift M

The first-family shift structure, composed with strict evaluation.

Equations

• CategoryTheory.Functor.CommShift₂.firstFamilyEvaluationCommShift h E = CategoryTheory.Functor.CommShift.comp F ((CategoryTheory.evaluation X Y).obj E)

theorem CategoryTheory.Functor.CommShift₂.firstFamilyEvaluationCommShift_eq {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] {M : Type uM} [AddCommMonoid M] [HasShift K M] [HasShift X M] [HasShift Y M] {F : Functor K (Functor X Y)} (h : CommShift₂Setup Y M) [F.CommShift₂ h] (E : X) : firstFamilyEvaluationCommShift h E = commShiftFlipObj h E

Evaluation of the assembled first-family structure is exactly the partial structure selected by CommShift₂.

@[reducible]

noncomputable def CategoryTheory.Functor.CommShift₂.secondFamilyEvaluationCommShift {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] {M : Type uM} [AddCommMonoid M] [HasShift K M] [HasShift X M] [HasShift Y M] {F : Functor K (Functor X Y)} (h : CommShift₂Setup Y M) [F.CommShift₂ h] (A : K) : (F.flip.comp ((evaluation K Y).obj A)).CommShift M

The second-family shift structure, composed with strict evaluation.

Equations

• CategoryTheory.Functor.CommShift₂.secondFamilyEvaluationCommShift h A = CategoryTheory.Functor.CommShift.comp F.flip ((CategoryTheory.evaluation K Y).obj A)

theorem CategoryTheory.Functor.CommShift₂.secondFamilyEvaluationCommShift_eq {K : Type uK} {X : Type uX} {Y : Type uY} [Category.{vK, uK} K] [Category.{vX, uX} X] [Category.{vY, uY} Y] {M : Type uM} [AddCommMonoid M] [HasShift K M] [HasShift X M] [HasShift Y M] {F : Functor K (Functor X Y)} (h : CommShift₂Setup Y M) [F.CommShift₂ h] (A : K) : secondFamilyEvaluationCommShift h A = commShiftObj h A

Evaluation of the assembled second-family structure is exactly the partial structure selected by CommShift₂.