English
There is a natural isomorphism between mapTrifunctor F I₁ I₂ I₃ and mapTrifunctor F' I₁ I₂ I₃ induced by a natural isomorphism e: F ≅ F'. The map respects composition and identities in both directions.
Русский
Существует натуральное изоморфизм между mapTrifunctor F и mapTrifunctor F', индуцируемый натуральным изоморфизмом e: F ≅ F'. Отображение сохраняет композицию и тождества.
LaTeX
$$$mapTrifunctorMapIso(F,I_1,I_2,I_3)(e) : mapTrifunctor F I_1 I_2 I_3 \cong mapTrifunctor F' I_1 I_2 I_3$$$
Lean4
/-- Given a trifunctor `F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₃`, graded objects `X₁ : GradedObject I₁ C₁`,
`X₂ : GradedObject I₂ C₂`, `X₃ : GradedObject I₃ C₃`, and a map `p : I₁ × I₂ × I₃ → J`,
this is 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₃⟩ = k`. -/
noncomputable def mapTrifunctorMapObj (X₁ : GradedObject I₁ C₁) (X₂ : GradedObject I₂ C₂) (X₃ : GradedObject I₃ C₃)
[HasMap ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃) p] : GradedObject J C₄ :=
((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).mapObj p
