ιMapBifunctorMapObj — Mathlib

English

There is a constructor for morphisms from mapBifunctorMapObj F p X Y k to any A from a family of maps indexed by (i,j).

Русский

Существует конструктор морфизмов из mapBifunctorMapObj F p X Y k в любой A, заданный семьей отображений, индексируемой парами (i,j).

LaTeX

$$$mapBifunctorMapObjDesc F p X Y k:\; \{f: \forall (i: I)(j: J)\,(p(i,j)=k) \to (F(X i).Y j \to A)\} \\to mapBifunctorMapObj F p X Y k \to A$$$

Lean4

/-- The inclusion of `(F.obj (X i)).obj (Y j)` in `mapBifunctorMapObj F p X Y k`
when `i + j = k`. -/
noncomputable def ιMapBifunctorMapObj (X : GradedObject I C₁) (Y : GradedObject J C₂)
    [HasMap (((mapBifunctor F I J).obj X).obj Y) p] (i : I) (j : J) (k : K) (h : p ⟨i, j⟩ = k) :
    (F.obj (X i)).obj (Y j) ⟶ mapBifunctorMapObj F p X Y k :=
  (((mapBifunctor F I J).obj X).obj Y).ιMapObj p ⟨i, j⟩ k h

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