mapBifunctorMapObj — Mathlib

English

There are canonical maps between the images of two morphisms under mapBifunctorMapObj, expressing functoriality.

Русский

Существуют канонические отображения между образами двух морфизмов под mapBifunctorMapObj, выражающие функториальность.

LaTeX

$$$mapBifunctorMapMap F p f g: mapBifunctorMapObj F p X_1 Y_1 \to mapBifunctorMapObj F p X_2 Y_2$$$

Lean4

/-- Given a bifunctor `F : C₁ ⥤ C₂ ⥤ C₃`, graded objects `X : GradedObject I C₁` and
`Y : GradedObject J C₂` and a map `p : I × J → K`, this is the `K`-graded object sending
`k` to the coproduct of `(F.obj (X i)).obj (Y j)` for `p ⟨i, j⟩ = k`. -/
noncomputable def mapBifunctorMapObj (X : GradedObject I C₁) (Y : GradedObject J C₂)
    [HasMap (((mapBifunctor F I J).obj X).obj Y) p] : GradedObject K C₃ :=
  (((mapBifunctor F I J).obj X).obj Y).mapObj p

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