English
There is a definition of a functor mapTrifunctorMap that sends triple-graded objects to a triple-graded object in the target category via a trifunctor F and a map p: I₁ × I₂ × I₃ → J.
Русский
Существует определение mapTrifunctorMap, отправляющее тройные градационные объекты в тройно градуированный объект в целевой категории через трефунктор F и отображение p: I₁ × I₂ × I₃ → J.
LaTeX
$$$mapTrifunctorMap : GradedObject I_1 C_1 ⥤ GradedObject I_2 C_2 ⥤ GradedObject I_3 C_3 ⥤ GradedObject (I_1 × I_2 × I_3) C_4$$$
Lean4
@[reassoc]
theorem ιMapBifunctor₁₂BifunctorMapObj_eq (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) (i₁₂ : ρ₁₂.I₁₂)
(h₁₂ : ρ₁₂.p ⟨i₁, i₂⟩ = i₁₂) :
ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h =
(G.map (ιMapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂ i₁ i₂ i₁₂ h₁₂)).app (X₃ i₃) ≫
ιMapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ i₁₂ i₃ j (by rw [← h₁₂, ← h, ← ρ₁₂.hpq]) :=
by
subst h₁₂
rfl
