mapTrifunctorMapFunctorObj — Mathlib

English

Given a trifactor F, the object part mapTrifunctorMapObj F p X₁ X₂ X₃ defines a functor from GradedObject I₂ C₂ to GradedObject I₃ C₃ to GradedObject J C₄, by composing the underlying functors and maps.

Русский

У данного трифутктора F компонент объекта образуют функтор от GradedObject I₂ C₂ в GradedObject I₃ C₃ в GradedObject J C₄ через композицию базовых функторов и отображений.

LaTeX

$$$mapTrifunctorMapObj\ F\ p\ X_1\ X_2\ X_3 : GradedObject\ I_2\ C_2 ⥤ GradedObject\ I_3\ C_3 ⥤ GradedObject\ J\ C_4$$$

Lean4

/-- Given a trifunctor `F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄`, a map `p : I₁ × I₂ × I₃ → J`, and
graded objects `X₁ : GradedObject I₁ C₁`, `X₂ : GradedObject I₂ C₂` and `X₃ : GradedObject I₃ C₃`,
this is the `J`-graded object sending `j` to the coproduct of
`((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃)` for `p ⟨i₁, i₂, i₃⟩ = j`. -/
@[simps]
noncomputable def mapTrifunctorMapFunctorObj (X₁ : GradedObject I₁ C₁)
    [∀ X₂ X₃, HasMap ((((mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj X₃) p] :
    GradedObject I₂ C₂ ⥤ GradedObject I₃ C₃ ⥤ GradedObject J C₄
    where
  obj
    X₂ :=
    { obj := fun X₃ => mapTrifunctorMapObj F p X₁ X₂ X₃
      map := fun {_ _} φ => mapTrifunctorMapMap F p (𝟙 X₁) (𝟙 X₂) φ
      map_id := fun X₃ => by
        ext j i₁ i₂ i₃ h
        simp only [ι_mapTrifunctorMapMap, categoryOfGradedObjects_id, Functor.map_id, NatTrans.id_app, id_comp, comp_id]
      map_comp := fun {X₃ Y₃ Z₃} φ ψ => by
        ext j i₁ i₂ i₃ h
        simp only [ι_mapTrifunctorMapMap, categoryOfGradedObjects_id, Functor.map_id, NatTrans.id_app,
          categoryOfGradedObjects_comp, Functor.map_comp, assoc, id_comp, ι_mapTrifunctorMapMap_assoc] }
  map {X₂ Y₂}
    φ :=
    { app := fun X₃ => mapTrifunctorMapMap F p (𝟙 X₁) φ (𝟙 X₃)
      naturality := fun {X₃ Y₃} ψ => by
        ext j i₁ i₂ i₃ h
        dsimp
        simp only [ι_mapTrifunctorMapMap_assoc, categoryOfGradedObjects_id, Functor.map_id, NatTrans.id_app,
          ι_mapTrifunctorMapMap, id_comp, NatTrans.naturality_assoc] }
  map_id
    X₂ := by
    ext X₃ j i₁ i₂ i₃ h
    simp only [ι_mapTrifunctorMapMap, categoryOfGradedObjects_id, Functor.map_id, NatTrans.id_app, id_comp, comp_id]
  map_comp {X₂ Y₂ Z₂} φ
    ψ := by
    ext X₃ j i₁ i₂ i₃
    simp only [ι_mapTrifunctorMapMap, categoryOfGradedObjects_id, Functor.map_id, NatTrans.id_app,
      categoryOfGradedObjects_comp, Functor.map_comp, NatTrans.comp_app, id_comp, assoc, ι_mapTrifunctorMapMap_assoc]

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