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.

def CategoryTheory.PullbackShift (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] : (A →+ B) → [inst : CategoryTheory.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) [CategoryTheory.Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [CategoryTheory.HasShift C B] : CategoryTheory.Category.{u_4, u_1} (CategoryTheory.PullbackShift C φ)

Equations

• CategoryTheory.instCategoryPullbackShift C φ = id inferInstance

noncomputable instance CategoryTheory.instHasShiftPullbackShift (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [CategoryTheory.HasShift C B] : CategoryTheory.HasShift (CategoryTheory.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) [CategoryTheory.Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [CategoryTheory.HasShift C B] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.PullbackShift C φ)

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.instPreadditivePullbackShift C φ = id inferInstance

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

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.pullbackShiftIso (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [CategoryTheory.HasShift C B] (a : A) (b : B) (h : b = φ a) : CategoryTheory.shiftFunctor (CategoryTheory.PullbackShift C φ) a ≅ CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} C] {A : Type u_2} {B : Type u_3} [AddMonoid A] [AddMonoid B] (φ : A →+ B) [CategoryTheory.HasShift C B] (X : CategoryTheory.PullbackShift C φ) : (CategoryTheory.shiftFunctorZero (CategoryTheory.PullbackShift C φ) A).inv.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorZero C B).inv.app X) ((CategoryTheory.pullbackShiftIso C φ 0 0 ⋯).inv.app X)

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

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

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