English
The natural isomorphism mapTrifunctorMapIso shows an isomorphism between mapTrifunctor F I₁ I₂ I₃ and mapTrifunctor F' I₁ I₂ I₃ induced by an isomorphism e: F ≅ F'. The construction preserves horizontal composition and identities.
Русский
Натуральный изоморфизм mapTrifunctorMapIso демонстрирует изоморфизм между mapTrifunctor F I₁ I₂ I₃ и mapTrifunctor F' I₁ I₂ I₃, индуцируемый изоморфизмом 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
/-- The inclusion of `(G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃)` in
`mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j`
when `r (i₁, i₂, i₃) = j`. -/
noncomputable def ιMapBifunctor₁₂BifunctorMapObj (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
(G.obj ((F₁₂.obj (X₁ i₁)).obj (X₂ i₂))).obj (X₃ i₃) ⟶
mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j :=
(G.map (ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ _ rfl)).app (X₃ i₃) ≫
ιMapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ (ρ₁₂.p ⟨i₁, i₂⟩) i₃ j (by rw [← h, ← ρ₁₂.hpq])
