English
Two expressions given by index-wise maps ιMapTrifunctorMapObj with the same index pattern are equal; this is a congruence property for the componentwise maps.
Русский
Две конструкции, заданные по индексу через ιMapTrifunctorMapObj, совпадают, если соответствующие компоненты совпадают — свойство равенств по компонентам.
LaTeX
$$$ιMapTrifunctorMapObj F p X_1 X_2 X_3 i_1 i_2 i_3 j h = ιMapTrifunctorMapObj F p X_1 X_2 X_3 i_1 i_2 i_3 j h$$$
Lean4
/-- The natural transformation `mapTrifunctor F I₁ I₂ I₃ ⟶ mapTrifunctor F' I₁ I₂ I₃`
induced by a natural transformation `F ⟶ F` of trifunctors. -/
@[simps]
def mapTrifunctorMapNatTrans (α : F ⟶ F') (I₁ I₂ I₃ : Type*) : mapTrifunctor F I₁ I₂ I₃ ⟶ mapTrifunctor F' I₁ I₂ I₃
where
app
X₁ :=
{ app := fun X₂ => { app := fun _ _ => ((α.app _).app _).app _ }
naturality := fun {X₂ Y₂} φ => by
ext X₃ ⟨i₁, i₂, i₃⟩
dsimp
simp only [← NatTrans.comp_app, NatTrans.naturality] }
naturality := fun {X₁ Y₁} φ => by
ext X₂ X₃ ⟨i₁, i₂, i₃⟩
dsimp
simp only [← NatTrans.comp_app, NatTrans.naturality]
