English
If a HasMap structure exists for a triple tensor construction, then the induced HasMap for the mapped triple under a functorial reassignment also exists.
Русский
Если существует структура HasMap для тройной тензорной конструции, то существуют аналогичные HasMap после отображения через функтор.
LaTeX
$$$\text{HasMap}(((mapTrifunctor F I_1 I_2 I_3).obj X_1).obj X_2).obj X_3) p \Rightarrow \text{HasMap}(mapTrifunctorMapObj F p X_1 X_2 X_3) p$$$
Lean4
/-- The obvious inclusion
`((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p X₁ X₂ X₃ j` when
`p ⟨i₁, i₂, i₃⟩ = j`. -/
noncomputable def ιMapTrifunctorMapObj (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃)
(i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : p ⟨i₁, i₂, i₃⟩ = j)
[HasMap ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃) p] :
((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃) ⟶ mapTrifunctorMapObj F p X₁ X₂ X₃ j :=
((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).ιMapObj p ⟨i₁, i₂, i₃⟩ j h
