English
Equality of inclusions ιMapTrifunctorMapObj under index substitutions i₁,i₂,i₃ that produce the same j is governed by the equalities on p and hpq; this ensures consistency of the triple-index decomposition.
Русский
Эквивалентность инклюзий ιMapTrifunctorMapObj при замещении индексов, приводящих к одному и тому же j, задается равенствами p и hpq; обеспечивает согласованность разложения по тройному индексу.
LaTeX
$$$ιMapTrifunctorMapObj F p X_1 X_2 X_3 i_1 i_2 i_3 j h = (G.map (ιMapTrifunctorMapObj F p X_1 X_2 i_1 i_2 i_1_2 h_1_2)).app (X_3 i_3) ≫ ιMapTrifunctorMapObj G ρ_{p}(...)$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_mapTrifunctorMapMap {X₁ Y₁ : GradedObject I₁ C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : GradedObject I₂ C₂} (f₂ : X₂ ⟶ Y₂)
{X₃ Y₃ : GradedObject I₃ C₃} (f₃ : X₃ ⟶ Y₃) [HasMap ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃) p]
[HasMap ((((mapTrifunctor F I₁ I₂ I₃).obj Y₁).obj Y₂).obj Y₃) p] (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J)
(h : p ⟨i₁, i₂, i₃⟩ = j) :
ιMapTrifunctorMapObj F p X₁ X₂ X₃ i₁ i₂ i₃ j h ≫ mapTrifunctorMapMap F p f₁ f₂ f₃ j =
((F.map (f₁ i₁)).app (X₂ i₂)).app (X₃ i₃) ≫
((F.obj (Y₁ i₁)).map (f₂ i₂)).app (X₃ i₃) ≫
((F.obj (Y₁ i₁)).obj (Y₂ i₂)).map (f₃ i₃) ≫ ιMapTrifunctorMapObj F p Y₁ Y₂ Y₃ i₁ i₂ i₃ j h :=
by
dsimp only [ιMapTrifunctorMapObj, mapTrifunctorMapMap]
rw [ι_mapMap]
dsimp
rw [assoc, assoc]
