English
Equality for the inclusions ιMapTrifunctorMapObj under two index decompositions that produce the same j, via the functorial mapping on ρ-parts.
Русский
Равенство для включений ιMapTrifunctorMapObj под двумя разложениями индексов, порождающими один и тот же j, через отображение по частям ρ.
LaTeX
$$$ιMapTrifunctorMapObj F p X_1 X_2 X_3 i_1 i_2 i_3 j h = (G.map (ιMapTrifunctorMapObj F p X_1 X_2 i_1 i_2 i_{1,2} h_{1,2})).app (X_3 i_3) ≫ ιMapTrifunctorMapObj G p (mapBifunctorMapObj F p X_1 X_2) X_3 i_{1,2} i_3 j (by rw[...])$$$
Lean4
/-- Given a trifunctor `F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄` and a map `p : I₁ × I₂ × I₃ → J`,
this is the functor
`GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject J C₄`
sending `X₁ : GradedObject I₁ C₁`, `X₂ : GradedObject I₂ C₂` and `X₃ : GradedObject I₃ C₃`
to the `J`-graded object sending `j` to the coproduct of
`((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃)` for `p ⟨i₁, i₂, i₃⟩ = j`. -/
noncomputable def mapTrifunctorMap [∀ X₁ X₂ X₃, HasMap ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃) p] :
GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject J C₄
where
obj X₁ := mapTrifunctorMapFunctorObj F p X₁
map := fun {X₁ Y₁} φ =>
{ app := fun X₂ =>
{ app := fun X₃ => mapTrifunctorMapMap F p φ (𝟙 X₂) (𝟙 X₃)
naturality := fun {X₃ Y₃} φ => by
dsimp
ext j i₁ i₂ i₃ h
dsimp
simp only [ι_mapTrifunctorMapMap_assoc, categoryOfGradedObjects_id, Functor.map_id, NatTrans.id_app,
ι_mapTrifunctorMapMap, id_comp, NatTrans.naturality_assoc] }
naturality := fun {X₂ Y₂} ψ => by
ext X₃ j
dsimp
ext i₁ i₂ i₃ h
simp only [ι_mapTrifunctorMapMap_assoc, categoryOfGradedObjects_id, Functor.map_id, NatTrans.id_app,
ι_mapTrifunctorMapMap, id_comp, NatTrans.naturality_app_assoc] }
