mapTrifunctor — Mathlib

English

A natural transformation α: F ⟶ F' induces a natural transformation mapTrifunctor from mapTrifunctor F to mapTrifunctor F'. The two naturality constraints commute with the given φ and ψ components.

Русский

Естественное преобразование α: F ⟶ F' порождает естественное преобразование mapTrifunctor между mapTrifunctor F и F', причём естественные условия согласовываются с компонентами φ и ψ.

LaTeX

$$$\text{def mapTrifunctorMapNatTrans}(\alpha) : mapTrifunctor F I_1 I_2 I_3 \to mapTrifunctor F' I_1 I_2 I_3$$$

Lean4

/-- Given a trifunctor `F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄` and types `I₁`, `I₂`, `I₃`,
this is the obvious functor
`GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject (I₁ × I₂ × I₃) C₄`.
-/
@[simps]
def mapTrifunctor (I₁ I₂ I₃ : Type*) :
    GradedObject I₁ C₁ ⥤ GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject (I₁ × I₂ × I₃) C₄
    where
  obj X₁ := mapTrifunctorObj F X₁ I₂ I₃
  map {X₁ Y₁}
    φ :=
    { app := fun X₂ => { app := fun X₃ x => ((F.map (φ x.1)).app (X₂ x.2.1)).app (X₃ x.2.2) }
      naturality := fun {X₂ Y₂} ψ => by
        ext X₃ x
        dsimp
        simp only [← NatTrans.comp_app]
        congr 1
        rw [NatTrans.naturality] }

Похожие утверждения