mapBifunctor — Mathlib

English

The injection from the component (F(X i)) (Y j) into mapBifunctorMapObj is canonical.

Русский

Вводящий мономорфизм из компонента (F(X i)) (Y j) в mapBifunctorMapObj является каноническим.

LaTeX

$$$ιMapBifunctorMapObj F p X Y i j k h: (F(X i)).(Y j) \to mapBifunctorMapObj F p X Y k$$$

Lean4

/-- Given a bifunctor `F : C₁ ⥤ C₂ ⥤ C₃` and types `I` and `J`, this is the obvious
functor `GradedObject I C₁ ⥤ GradedObject J C₂ ⥤ GradedObject (I × J) C₃`. -/
@[simps]
def mapBifunctor (I J : Type*) : GradedObject I C₁ ⥤ GradedObject J C₂ ⥤ GradedObject (I × J) C₃
    where
  obj
    X :=
    { obj := fun Y ij => (F.obj (X ij.1)).obj (Y ij.2)
      map := fun φ ij => (F.obj (X ij.1)).map (φ ij.2) }
  map φ := { app := fun Y ij => (F.map (φ ij.1)).app (Y ij.2) }

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