# Documentation

Mathlib.CategoryTheory.Shift.Pullback

# 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) [] {A : Type u_2} {B : Type u_3} [] [] :
(A →+ B)[inst : ] → 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
Instances For
instance CategoryTheory.instCategoryPullbackShift (C : Type u_1) [] {A : Type u_2} {B : Type u_3} [] [] (φ : A →+ B) [] :
Equations
• = id inferInstance
noncomputable instance CategoryTheory.instHasShiftPullbackShiftInstCategoryPullbackShift (C : Type u_1) [] {A : Type u_2} {B : Type u_3} [] [] (φ : A →+ B) [] :

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

Equations
• = { shift := ⊗⋙ CategoryTheory.HasShift.shift }
instance CategoryTheory.instHasZeroObjectPullbackShiftInstCategoryPullbackShift (C : Type u_1) [] {A : Type u_2} {B : Type u_3} [] [] (φ : A →+ B) [] :
Equations
instance CategoryTheory.instPreadditivePullbackShiftInstCategoryPullbackShift (C : Type u_1) [] {A : Type u_2} {B : Type u_3} [] [] (φ : A →+ B) [] :
Equations
• = id inferInstance
Equations
noncomputable def CategoryTheory.pullbackShiftIso (C : Type u_1) [] {A : Type u_2} {B : Type u_3} [] [] (φ : A →+ B) [] (a : A) (b : B) (h : b = φ a) :

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

Equations
Instances For
theorem CategoryTheory.pullbackShiftFunctorZero_inv_app {C : Type u_1} [] {A : Type u_2} {B : Type u_3} [] [] (φ : A →+ B) [] (X : ) :
.inv.app X = CategoryTheory.CategoryStruct.comp (.inv.app X) ((CategoryTheory.pullbackShiftIso C φ 0 0 (_ : 0 = φ 0)).inv.app X)
theorem CategoryTheory.pullbackShiftFunctorZero_hom_app {C : Type u_1} [] {A : Type u_2} {B : Type u_3} [] [] (φ : A →+ B) [] (X : ) :
.hom.app X = CategoryTheory.CategoryStruct.comp ((CategoryTheory.pullbackShiftIso C φ 0 0 (_ : 0 = φ 0)).hom.app X) (.hom.app X)
theorem CategoryTheory.pullbackShiftFunctorAdd'_inv_app {C : Type u_1} [] {A : Type u_2} {B : Type u_3} [] [] (φ : A →+ B) [] (X : ) (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₃) :
().inv.app X = CategoryTheory.CategoryStruct.comp (.map ((CategoryTheory.pullbackShiftIso C φ a₁ b₁ h₁).hom.app X)) (CategoryTheory.CategoryStruct.comp ((CategoryTheory.pullbackShiftIso C φ a₂ b₂ h₂).hom.app (().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} [] {A : Type u_2} {B : Type u_3} [] [] (φ : A →+ B) [] (X : ) (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₃) :
().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 (().obj X)) (.map ((CategoryTheory.pullbackShiftIso C φ a₁ b₁ h₁).inv.app X))))