ι_mapBifunctorMapObjDesc — Mathlib

English

Equivalence of different descriptions of the same universal map from mapBifunctorMapObjDesc.

Русский

Эквивалентность различных описаний одного универсального отображения из mapBifunctorMapObjDesc.

LaTeX

$$$Equiv(mapBifunctorMapObjDesc, otherDesc)$$$

Lean4

@[reassoc (attr := simp)]
theorem ι_mapBifunctorMapObjDesc {X : GradedObject I C₁} {Y : GradedObject J C₂} {A : C₃} {k : K}
    [HasMap (((mapBifunctor F I J).obj X).obj Y) p]
    (f : ∀ (i : I) (j : J) (_ : p ⟨i, j⟩ = k), (F.obj (X i)).obj (Y j) ⟶ A) (i : I) (j : J) (hij : p ⟨i, j⟩ = k) :
    ιMapBifunctorMapObj F p X Y i j k hij ≫ mapBifunctorMapObjDesc f = f i j hij := by apply ι_descMapObj

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