English
The homs of the iso between composed bifunctor actions satisfy a congruence relation: composing the ι-map with the iso hom gives the same as applying the ι-map for the composed bifunctor.
Русский
Гомоморфизмы изоморфизма между действиями композиции бифункторов удовлетворяют равносвязному соотношению: композиция ι-map с гомоморфизмом изоморфизма даёт то же самое, что применение ι-map для композиции бифункторов.
LaTeX
$$$$ιMapTrifunctorMapObj(\mathrm{bifunctorComp}_{12} F_{12} G) r X_1 X_2 X_3 i_1 i_2 i_3 j h \; \circ \; (\mathrm{mapBifunctorComp}_{12}MapObjIso F_{12} G ρ X_1 X_2 X_3).hom j = ιMapBifunctorBifunctorMapObj F G ρ X_1 X_2 X_3 i_1 i_2 i_3 j h.$$$$
Lean4
@[ext]
theorem mapBifunctor₁₂BifunctorMapObj_ext {A : C₄}
{f g : mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j ⟶ A}
(h :
∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r ⟨i₁, i₂, i₃⟩ = j),
ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ f =
ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ g) :
f = g :=
by
apply Cofan.IsColimit.hom_ext (isColimitCofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)
rintro ⟨i, hi⟩
exact h _ _ _ hi
