English
There is a matching principle for mapBifunctorMapObjDesc with a fixed i,j and h.
Русский
Существует принцип согласования mapBifunctorMapObjDesc для заданных i,j и h.
LaTeX
$$$mapBifunctorMapObjDesc F p X Y k \;|_{i,j,h} = f$$$
Lean4
/-- Given a bifunctor `F : C₁ ⥤ C₂ ⥤ C₃` and a map `p : I × J → K`, this is the
functor `GradedObject I C₁ ⥤ GradedObject J C₂ ⥤ GradedObject K C₃` sending
`X : GradedObject I C₁` and `Y : GradedObject J C₂` to the `K`-graded object sending
`k` to the coproduct of `(F.obj (X i)).obj (Y j)` for `p ⟨i, j⟩ = k`. -/
@[simps]
noncomputable def mapBifunctorMap [∀ X Y, HasMap (((mapBifunctor F I J).obj X).obj Y) p] :
GradedObject I C₁ ⥤ GradedObject J C₂ ⥤ GradedObject K C₃
where
obj
X :=
{ obj := fun Y => mapBifunctorMapObj F p X Y
map := fun ψ => mapBifunctorMapMap F p (𝟙 X) ψ }
map {X₁ X₂}
φ :=
{ app := fun Y => mapBifunctorMapMap F p φ (𝟙 Y)
naturality := fun {Y₁ Y₂} ψ => by
dsimp
simp only [Functor.map_id, NatTrans.id_app, id_comp, comp_id, ← mapMap_comp, NatTrans.naturality] }
