English
The maps ιMapBifunctorMapObj express the inclusions of the components into the coproduct-shaped object mapBifunctorMapObj.
Русский
Отображения ιMapBifunctorMapObj задают включения компонент в отображение объекта в виде копроизведения.
LaTeX
$$$ιMapBifunctorMapObj F p X Y i j k h: (F(X i)).(Y j) \to mapBifunctorMapObj F p X Y k$$$
Lean4
/-- The maps `mapBifunctorMapObj F p X₁ Y₁ ⟶ mapBifunctorMapObj F p X₂ Y₂` which express
the functoriality of `mapBifunctorMapObj`, see `mapBifunctorMap`. -/
noncomputable def mapBifunctorMapMap {X₁ X₂ : GradedObject I C₁} (f : X₁ ⟶ X₂) {Y₁ Y₂ : GradedObject J C₂} (g : Y₁ ⟶ Y₂)
[HasMap (((mapBifunctor F I J).obj X₁).obj Y₁) p] [HasMap (((mapBifunctor F I J).obj X₂).obj Y₂) p] :
mapBifunctorMapObj F p X₁ Y₁ ⟶ mapBifunctorMapObj F p X₂ Y₂ :=
GradedObject.mapMap (((mapBifunctor F I J).map f).app Y₁ ≫ ((mapBifunctor F I J).obj X₂).map g) p
