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.instHasShiftPullbackShiftInstCategoryPullbackShift (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.instHasShiftPullbackShiftInstCategoryPullbackShift C φ = { shift := CategoryTheory.Discrete.addMonoidalFunctor φ ⊗⋙ CategoryTheory.HasShift.shift }

instance CategoryTheory.instHasZeroObjectPullbackShiftInstCategoryPullbackShift (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

• (_ : CategoryTheory.Limits.HasZeroObject (CategoryTheory.PullbackShift C φ)) = (_ : CategoryTheory.Limits.HasZeroObject (CategoryTheory.PullbackShift C φ))

instance CategoryTheory.instPreadditivePullbackShiftInstCategoryPullbackShift (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.instPreadditivePullbackShiftInstCategoryPullbackShift C φ = id inferInstance

instance CategoryTheory.instAdditivePullbackShiftInstCategoryPullbackShiftInstPreadditivePullbackShiftInstCategoryPullbackShiftShiftFunctorInstHasShiftPullbackShiftInstCategoryPullbackShift (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.Functor.Additive (CategoryTheory.shiftFunctor C (φ a))] : CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor (CategoryTheory.PullbackShift C φ) a)

Equations

• (_ : CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor (CategoryTheory.PullbackShift C φ) a)) = (_ : CategoryTheory.Functor.Additive (CategoryTheory.shiftFunctor C (φ a)))

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 (_ : CategoryTheory.shiftFunctor (CategoryTheory.PullbackShift C φ) a = CategoryTheory.shiftFunctor C b)

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 (_ : 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 (_ : 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) (a₃ : A) (h : a₁ + a₂ = a₃) (b₁ : B) (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₂).toPrefunctor.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₁).toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C b₁ b₂ b₃ (_ : 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) (a₃ : A) (h : a₁ + a₂ = a₃) (b₁ : B) (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₃ (_ : b₁ + b₂ = b₃)).hom.app X) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.pullbackShiftIso C φ a₂ b₂ h₂).inv.app ((CategoryTheory.shiftFunctor C b₁).toPrefunctor.obj X)) ((CategoryTheory.shiftFunctor (CategoryTheory.PullbackShift C φ) a₂).toPrefunctor.map ((CategoryTheory.pullbackShiftIso C φ a₁ b₁ h₁).inv.app X))))