The associator for actions of bifunctors on homological complexes #
In this file, we shall adapt the results of the file
CategoryTheory.GradedObject.Associator
to the case of homological complexes.
Given functors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
, G : C₁₂ ⥤ C₃ ⥤ C₄
,
F : C₁ ⥤ C₂₃ ⥤ C₄
, G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
equipped with an isomorphism
associator : bifunctorComp₁₂ F₁₂ G ≅ bifunctorComp₂₃ F G₂₃
(which informally means
that we have natural isomorphisms G(F₁₂(X₁, X₂), X₃) ≅ F(X₁, G₂₃(X₂, X₃))
),
we define an isomorphism mapBifunctorAssociator
from
mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄
to
mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄
when
we have three homological complexes K₁ : HomologicalComplex C₁ c₁
,
K₂ : HomologicalComplex C₂ c₂
and K₃ : HomologicalComplex C₃ c₃
,
assumptions TotalComplexShape c₁ c₂ c₁₂
, TotalComplexShape c₁₂ c₃ c₄
,
TotalComplexShape c₂ c₃ c₂₃
, TotalComplexShape c₁ c₂₃ c₄
,
and ComplexShape.Associative c₁ c₂ c₃ c₁₂ c₂₃ c₄
about the complex
shapes, and technical assumptions
[HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
and
[HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄]
about the
commutation of certain functors to certain coproducts.
The main application of these results shall be the construction of the associator for the monoidal category structure on homological complexes.
Given bifunctors F₁₂ : C₁ ⥤ C₂ ⥤ C₁₂
, G : C₁₂ ⥤ C₃ ⥤ C₄
, homological complexes
K₁ : HomologicalComplex C₁ c₁
, K₂ : HomologicalComplex C₂ c₂
and
K₃ : HomologicalComplex C₃ c₃
, and complexes shapes c₁₂
, c₄
, this asserts
that for all i₁₂ : ι₁₂
and i₃ : ι₃
, the functor G(-, K₃.X i₃)
commutes with
the coproducts of the F₁₂(X₁ i₁, X₂ i₂)
such that π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = i₁₂
.
Equations
- HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄ = CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj F₁₂ G (c₁.ρ₁₂ c₂ c₃ c₁₂ c₄) K₁.X K₂.X K₃.X
Instances For
Given bifunctors F : C₁ ⥤ C₂₃ ⥤ C₄
, G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃
, homological complexes
K₁ : HomologicalComplex C₁ c₁
, K₂ : HomologicalComplex C₂ c₂
and
K₃ : HomologicalComplex C₃ c₃
, and complexes shapes c₁₂
, c₂₃
, c₄
with ComplexShape.Associative c₁ c₂ c₃ c₁₂ c₂₃ c₄
, this asserts that for
all i₁ : ι₁
and i₂₃ : ι₂₃
, the functor F(K₁.X i₁, _)
commutes with
the coproducts of the G₂₃(K₂.X i₂, K₃.X i₃)
such that π c₂ c₃ c₂₃ ⟨i₂, i₃⟩ = i₂₃
.
Equations
- HomologicalComplex.HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ = CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ (c₁.ρ₂₃ c₂ c₃ c₁₂ c₂₃ c₄) K₁.X K₂.X K₃.X
Instances For
The associator isomorphism for the action of bifunctors on homological complexes, in each degree.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inclusion of a summand in mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄
.
Equations
- HomologicalComplex.mapBifunctor₁₂.ι F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j h = CategoryTheory.GradedObject.ιMapBifunctor₁₂BifunctorMapObj F₁₂ G (c₁.ρ₁₂ c₂ c₃ c₁₂ c₄) K₁.X K₂.X K₃.X i₁ i₂ i₃ j h
Instances For
The inclusion of a summand in mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄
,
or zero.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructor for morphisms from
(mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄).X j
.
Equations
Instances For
The first differential on a summand
of mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The second differential on a summand
of mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The third differential on a summand
of mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The first differential on mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The second differential on mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The third differential on mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄
.
Equations
- HomologicalComplex.mapBifunctor₁₂.D₃ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' = HomologicalComplex.mapBifunctor.D₂ (K₁.mapBifunctor K₂ F₁₂ c₁₂) K₃ G c₄ j j'
Instances For
The inclusion of a summand in mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄
.
Equations
- HomologicalComplex.mapBifunctor₂₃.ι F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄ i₁ i₂ i₃ j h = CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ (c₁.ρ₂₃ c₂ c₃ c₁₂ c₂₃ c₄) K₁.X K₂.X K₃.X i₁ i₂ i₃ j h
Instances For
The inclusion of a summand in mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄
,
or zero.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Constructor for morphisms from
(mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄).X j
.
Equations
Instances For
The first differential on a summand
of mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The second differential on a summand
of mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The third differential on a summand
of mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The first differential on mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄
.
Equations
- HomologicalComplex.mapBifunctor₂₃.D₁ F G₂₃ K₁ K₂ K₃ c₂₃ c₄ j j' = HomologicalComplex.mapBifunctor.D₁ K₁ (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄ j j'
Instances For
The second differential on mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The third differential on mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The associator isomorphism for the action of bifunctors on homological complexes.
Equations
- HomologicalComplex.mapBifunctorAssociator associator K₁ K₂ K₃ c₁₂ c₂₃ c₄ = HomologicalComplex.Hom.isoOfComponents (HomologicalComplex.mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄) ⋯