The pullback of a shift by a monoid morphism

Given a shift by a monoid B on a category C and a monoid morphism φ : A →+ B, we define a shift by A on a category PullbackShift C φ which is a type synonym for C.

If F : C ⥤ D is a functor between categories equipped with shifts by B, we define a type synonym PullbackShift.functor F φ for F. When F has a CommShift structure by B, we define a pulled back CommShift structure by A on PullbackShift.functor F φ.

Similarly, if τ is a natural transformation between functors F,G : C ⥤ D, we define a type synonym PullbackShift.natTrans τ φ : PullbackShift.functor F φ ⟶ PullbackShift.functor G φ. When τ has a CommShift structure by B (i.e. is compatible with CommShift structures on F and G), we define a pulled back CommShift structure by A on PullbackShift.natTrans τ φ.

Finally, if we have an adjunction F ⊣ G (with G : D ⥤ C), we define a type synonym PullbackShift.adjunction adj φ : PullbackShift.functor F φ ⊣ PullbackShift.functor G φ and we show that, if adj compatible with CommShift structures on F and G, then PullbackShift.adjunction adj φ iis also compatible with the pulled back CommShift structures.

def CategoryTheory.PullbackShift (C : Type u_1) [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] : (A →+ B) → [HasShift C B] → Type u_1

The category PullbackShift C φ is equipped with a shift such that for all a, the shift functor by a is shiftFunctor C (φ a).

Equations

• CategoryTheory.PullbackShift C x✝ = C

instance CategoryTheory.instCategoryPullbackShift (C : Type u_1) [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] : Category.{u_4, u_1} (PullbackShift C φ)

Equations

• CategoryTheory.instCategoryPullbackShift C φ = id inferInstance

noncomputable instance CategoryTheory.instHasShiftPullbackShift (C : Type u_1) [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] : HasShift (PullbackShift C φ) A

The shift on PullbackShift C φ is obtained by precomposing the shift on C with the monoidal functor Discrete.addMonoidalFunctor φ : Discrete A ⥤ Discrete B.

Equations

• CategoryTheory.instHasShiftPullbackShift C φ = { shift := (CategoryTheory.Discrete.addMonoidalFunctor φ).comp (CategoryTheory.shiftMonoidalFunctor C B), shiftMonoidal := inferInstance }

instance CategoryTheory.instHasZeroObjectPullbackShift (C : Type u_1) [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] [Limits.HasZeroObject C] : Limits.HasZeroObject (PullbackShift C φ)

instance CategoryTheory.instPreadditivePullbackShift (C : Type u_1) [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] [Preadditive C] : Preadditive (PullbackShift C φ)

Equations

• CategoryTheory.instPreadditivePullbackShift C φ = id inferInstance

instance CategoryTheory.instAdditivePullbackShiftShiftFunctorOfCoeAddMonoidHom (C : Type u_1) [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] [Preadditive C] (a : A) [(shiftFunctor C (φ a)).Additive] : (shiftFunctor (PullbackShift C φ) a).Additive

noncomputable def CategoryTheory.pullbackShiftIso (C : Type u_1) [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] (a : A) (b : B) (h : b = φ a) : shiftFunctor (PullbackShift C φ) a ≅ shiftFunctor C b

When b = φ a, this is the canonical isomorphism shiftFunctor (PullbackShift C φ) a ≅ shiftFunctor C b.

Equations

• CategoryTheory.pullbackShiftIso C φ a b h = CategoryTheory.eqToIso ⋯

theorem CategoryTheory.pullbackShiftFunctorZero_inv_app {C : Type u_1} [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] (X : PullbackShift C φ) : (shiftFunctorZero (PullbackShift C φ) A).inv.app X = CategoryStruct.comp ((shiftFunctorZero C B).inv.app X) ((pullbackShiftIso C φ 0 0 ⋯).inv.app X)

theorem CategoryTheory.pullbackShiftFunctorZero_hom_app {C : Type u_1} [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] (X : PullbackShift C φ) : (shiftFunctorZero (PullbackShift C φ) A).hom.app X = CategoryStruct.comp ((pullbackShiftIso C φ 0 0 ⋯).hom.app X) ((shiftFunctorZero C B).hom.app X)

theorem CategoryTheory.pullbackShiftFunctorZero'_inv_app {C : Type u_1} [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] (X : PullbackShift C φ) : (shiftFunctorZero (PullbackShift C φ) A).inv.app X = CategoryStruct.comp ((shiftFunctorZero' C (φ 0) ⋯).inv.app X) ((pullbackShiftIso C φ 0 (φ 0) ⋯).inv.app X)

theorem CategoryTheory.pullbackShiftFunctorZero'_hom_app {C : Type u_1} [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] (X : PullbackShift C φ) : (shiftFunctorZero (PullbackShift C φ) A).hom.app X = CategoryStruct.comp ((pullbackShiftIso C φ 0 (φ 0) ⋯).hom.app X) ((shiftFunctorZero' C (φ 0) ⋯).hom.app X)

theorem CategoryTheory.pullbackShiftFunctorAdd'_inv_app {C : Type u_1} [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] (X : PullbackShift C φ) (a₁ a₂ a₃ : A) (h : a₁ + a₂ = a₃) (b₁ b₂ b₃ : B) (h₁ : b₁ = φ a₁) (h₂ : b₂ = φ a₂) (h₃ : b₃ = φ a₃) : (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ a₃ h).inv.app X = CategoryStruct.comp ((shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).hom.app X)) (CategoryStruct.comp ((pullbackShiftIso C φ a₂ b₂ h₂).hom.app ((shiftFunctor C b₁).obj X)) (CategoryStruct.comp ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).inv.app X) ((pullbackShiftIso C φ a₃ b₃ h₃).inv.app X)))

theorem CategoryTheory.pullbackShiftFunctorAdd'_hom_app {C : Type u_1} [Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] (X : PullbackShift C φ) (a₁ a₂ a₃ : A) (h : a₁ + a₂ = a₃) (b₁ b₂ b₃ : B) (h₁ : b₁ = φ a₁) (h₂ : b₂ = φ a₂) (h₃ : b₃ = φ a₃) : (shiftFunctorAdd' (PullbackShift C φ) a₁ a₂ a₃ h).hom.app X = CategoryStruct.comp ((pullbackShiftIso C φ a₃ b₃ h₃).hom.app X) (CategoryStruct.comp ((shiftFunctorAdd' C b₁ b₂ b₃ ⋯).hom.app X) (CategoryStruct.comp ((pullbackShiftIso C φ a₂ b₂ h₂).inv.app ((shiftFunctor C b₁).obj X)) ((shiftFunctor (PullbackShift C φ) a₂).map ((pullbackShiftIso C φ a₁ b₁ h₁).inv.app X))))

def CategoryTheory.PullbackShift.functor {C : Type u_1} [Category.{u_5, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] {D : Type u_4} [Category.{u_6, u_4} D] [HasShift D B] (F : Functor C D) : Functor (PullbackShift C φ) (PullbackShift D φ)

The functor F, seen as a functor from PullbackShift C φ to PullbackShift D φ. Then a CommShift B instance on F will define a CommShift A instance on PullbackShift.functor F φ, and we won't have to juggle with two CommShift instances on F.

Equations

• CategoryTheory.PullbackShift.functor φ F = F

def CategoryTheory.PullbackShift.natTrans {C : Type u_1} [Category.{u_5, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] {D : Type u_4} [Category.{u_6, u_4} D] [HasShift D B] {F G : Functor C D} (τ : F ⟶ G) : functor φ F ⟶ functor φ G

The natural transformation τ, seen as a natural transformation from PullbackShift.functor F φ to PullbackShift.functor G φ. Then a CommShift B instance on τ will define a CommShift A instance on PullbackShift.natTrans τ φ, and we won't have to juggle with two CommShift instances on τ.

Equations

• CategoryTheory.PullbackShift.natTrans φ τ = τ

noncomputable instance CategoryTheory.Functor.commShiftPullback {C : Type u_1} [Category.{u_5, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] {D : Type u_4} [Category.{u_6, u_4} D] [HasShift D B] (F : Functor C D) [F.CommShift B] : (PullbackShift.functor φ F).CommShift A

If F : C ⥤ D commutes with the shifts on C and D, then PullbackShift.functor F φ commutes with their pullbacks by an additive map φ.

Equations

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

theorem CategoryTheory.Functor.commShiftPullback_iso_eq {C : Type u_1} [Category.{u_6, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] {D : Type u_4} [Category.{u_5, u_4} D] [HasShift D B] (F : Functor C D) [F.CommShift B] (a : A) (b : B) (h : b = φ a) : (PullbackShift.functor φ F).commShiftIso a = isoWhiskerRight (pullbackShiftIso C φ a b h) F ≪≫ F.commShiftIso b ≪≫ isoWhiskerLeft F (pullbackShiftIso D φ a b h).symm

instance CategoryTheory.NatTrans.commShiftPullback {C : Type u_1} [Category.{u_6, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] {D : Type u_4} [Category.{u_5, u_4} D] [HasShift D B] {F : Functor C D} [F.CommShift B] {G : Functor C D} [G.CommShift B] (τ : F ⟶ G) [CommShift τ B] : CommShift (PullbackShift.natTrans φ τ) A

def CategoryTheory.NatTrans.PullbackShift.natIsoId (C : Type u_1) [Category.{u_5, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] : Functor.id (PullbackShift C φ) ≅ PullbackShift.functor φ (Functor.id C)

The natural isomorphism between the identity of PullbackShift C φ and the pullback of the identity of C.

Equations

• CategoryTheory.NatTrans.PullbackShift.natIsoId C φ = CategoryTheory.Iso.refl (CategoryTheory.Functor.id (CategoryTheory.PullbackShift C φ))

instance CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoId {C : Type u_1} [Category.{u_5, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] : CommShift (PullbackShift.natIsoId C φ).hom A

This expresses the compatibility between two CommShift structures by A on (synonyms of) 𝟭 C: the canonical CommShift structure on 𝟭 (PullbackShift C φ), and the CommShift structure on PullbackShift.functor (𝟭 C) φ (i.e the pullback of the canonical CommShift structure on 𝟭 C).

def CategoryTheory.NatTrans.PullbackShift.natIsoComp {C : Type u_1} [Category.{u_6, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] {D : Type u_4} [Category.{u_7, u_4} D] [HasShift D B] (F : Functor C D) {E : Type u_5} [Category.{u_8, u_5} E] [HasShift E B] (G : Functor D E) : PullbackShift.functor φ (F.comp G) ≅ (PullbackShift.functor φ F).comp (PullbackShift.functor φ G)

The natural isomorphism between the pullback of F ⋙ G and the composition of the pullbacks of F and G.

Equations

• CategoryTheory.NatTrans.PullbackShift.natIsoComp φ F G = CategoryTheory.Iso.refl (CategoryTheory.PullbackShift.functor φ (F.comp G))

instance CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoComp {C : Type u_1} [Category.{u_6, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] {D : Type u_4} [Category.{u_8, u_4} D] [HasShift D B] (F : Functor C D) [F.CommShift B] {E : Type u_5} [Category.{u_7, u_5} E] [HasShift E B] (G : Functor D E) [G.CommShift B] : CommShift (PullbackShift.natIsoComp φ F G).hom A

def CategoryTheory.PullbackShift.adjunction {C : Type u_1} [Category.{u_5, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] {D : Type u_4} [Category.{u_6, u_4} D] [HasShift D B] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) : functor φ F ⊣ functor φ G

The adjunction adj, seen as an adjunction between PullbackShift.functor F φ and PullbackShift.functor G φ.

Equations

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

theorem CategoryTheory.PullbackShift.adjunction_unit {C : Type u_1} [Category.{u_5, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] {D : Type u_4} [Category.{u_6, u_4} D] [HasShift D B] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) : (adjunction φ adj).unit = CategoryStruct.comp (NatTrans.PullbackShift.natIsoId C φ).hom (CategoryStruct.comp (natTrans φ adj.unit) (NatTrans.PullbackShift.natIsoComp φ F G).hom)

theorem CategoryTheory.PullbackShift.adjunction_counit {C : Type u_1} [Category.{u_5, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] {D : Type u_4} [Category.{u_6, u_4} D] [HasShift D B] {F : Functor C D} {G : Functor D C} (adj : F ⊣ G) : (adjunction φ adj).counit = CategoryStruct.comp (NatTrans.PullbackShift.natIsoComp φ G F).inv (CategoryStruct.comp (natTrans φ adj.counit) (NatTrans.PullbackShift.natIsoId D φ).inv)

instance CategoryTheory.Adjunction.commShiftPullback {C : Type u_1} [Category.{u_5, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [HasShift C B] {D : Type u_4} [Category.{u_6, u_4} D] [HasShift D B] {F : Functor C D} [F.CommShift B] {G : Functor D C} (adj : F ⊣ G) [G.CommShift B] [adj.CommShift B] : (PullbackShift.adjunction φ adj).CommShift A

If an adjunction F ⊣ G is compatible with CommShift structures on F and G, then it is also compatible with the pulled back CommShift structures by an additive map φ : B →+ A.