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)
[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
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
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))))
def
CategoryTheory.PullbackShift.functor
{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)
:
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
Instances For
def
CategoryTheory.PullbackShift.natTrans
{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 G : CategoryTheory.Functor C D}
(τ : F ⟶ 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
Instances For
noncomputable instance
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]
:
(CategoryTheory.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}
[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)
:
(CategoryTheory.PullbackShift.functor φ 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
instance
CategoryTheory.NatTrans.commShiftPullback
{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]
{G : CategoryTheory.Functor C D}
[G.CommShift B]
(τ : F ⟶ G)
[CategoryTheory.NatTrans.CommShift τ B]
:
def
CategoryTheory.NatTrans.PullbackShift.natIsoId
(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]
:
The natural isomorphism between the identity of PullbackShift C φ and the
pullback of the identity of C.
Equations
Instances For
instance
CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoId
{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]
:
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}
[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_7, u_4} D]
[CategoryTheory.HasShift D B]
(F : CategoryTheory.Functor C D)
{E : Type u_5}
[CategoryTheory.Category.{u_8, u_5} E]
[CategoryTheory.HasShift E B]
(G : CategoryTheory.Functor D E)
:
CategoryTheory.PullbackShift.functor φ (F.comp G) ≅ (CategoryTheory.PullbackShift.functor φ F).comp (CategoryTheory.PullbackShift.functor φ G)
The natural isomorphism between the pullback of F ⋙ G and the
composition of the pullbacks of F and G.
Equations
Instances For
instance
CategoryTheory.NatTrans.instCommShiftPullbackShiftHomFunctorNatIsoComp
{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_8, u_4} D]
[CategoryTheory.HasShift D B]
(F : CategoryTheory.Functor C D)
[F.CommShift B]
{E : Type u_5}
[CategoryTheory.Category.{u_7, u_5} E]
[CategoryTheory.HasShift E B]
(G : CategoryTheory.Functor D E)
[G.CommShift B]
:
def
CategoryTheory.PullbackShift.adjunction
{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}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ 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.
Instances For
theorem
CategoryTheory.PullbackShift.adjunction_unit
{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}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
:
theorem
CategoryTheory.PullbackShift.adjunction_counit
{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}
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
:
(CategoryTheory.PullbackShift.adjunction φ adj).counit = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.PullbackShift.natIsoComp φ G F).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.PullbackShift.natTrans φ adj.counit)
(CategoryTheory.NatTrans.PullbackShift.natIsoId D φ).inv)
instance
CategoryTheory.Adjunction.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]
{G : CategoryTheory.Functor D C}
(adj : F ⊣ G)
[G.CommShift B]
[adj.CommShift B]
:
(CategoryTheory.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.