mapBifunctorMapObjDesc — Mathlib

English

Alternative presentation of the same descent map ensuring compatibility with i,j,k indexing.

Русский

Альтернативное представление того же отображения спада, обеспечивающее совместимость с индексами i,j,k.

LaTeX

$$$\text{MapObjDescAlt}$$$

Lean4

/-- Constructor for morphisms from `mapBifunctorMapObj F p X Y k`. -/
noncomputable def 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) : mapBifunctorMapObj F p X Y k ⟶ A :=
  descMapObj _ _ (fun ⟨i, j⟩ hij => f i j hij)

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