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
Instances For
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]
:
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]
:
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]
:
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]
:
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
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)
:
When b = φ a, this is the canonical
isomorphism shiftFunctor (PullbackShift C φ) a ≅ shiftFunctor C b.
Equations
- CategoryTheory.pullbackShiftIso C φ a b h = CategoryTheory.eqToIso ⋯
Instances For
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.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 (φ 0) ⋯).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 (φ 0) ⋯).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))))
noncomputable def
CategoryTheory.Functor.commShiftPullback
{C : Type u_1}
[CategoryTheory.Category.{u_5, u_1} C]
{A : Type u_2}
{B : Type u_3}
[AddMonoid A]
[AddMonoid B]
(φ : A →+ B)
[CategoryTheory.HasShift C B]
{D : Type u_4}
[CategoryTheory.Category.{u_6, u_4} D]
[CategoryTheory.HasShift D B]
(F : CategoryTheory.Functor C D)
[F.CommShift B]
:
F.CommShift A
If F : C ⥤ D commutes with the shifts on C and D, then it also commutes with
their pullbacks by an additive map.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CategoryTheory.Functor.commShiftPullback_iso_eq
{C : Type u_1}
[CategoryTheory.Category.{u_6, u_1} C]
{A : Type u_2}
{B : Type u_3}
[AddMonoid A]
[AddMonoid B]
(φ : A →+ B)
[CategoryTheory.HasShift C B]
{D : Type u_4}
[CategoryTheory.Category.{u_5, u_4} D]
[CategoryTheory.HasShift D B]
(F : CategoryTheory.Functor C D)
[F.CommShift B]
(a : A)
(b : B)
(h : b = φ a)
:
F.commShiftIso a = CategoryTheory.isoWhiskerRight (CategoryTheory.pullbackShiftIso C φ a b h) F ≪≫ F.commShiftIso b ≪≫ CategoryTheory.isoWhiskerLeft F (CategoryTheory.pullbackShiftIso D φ a b h).symm