mapBifunctorLeftUnitor — Mathlib

English

Reinforces the previous HasMap assertion in a reflexive setting with left unitor.

Русский

Укрепляет предыдущее утверждение HasMap в рефлексивной настройке с левым унитором.

LaTeX

$$$$mapBifunctorLeftUnitor_hasMap\;: HasMap (mapBifunctorMapObj F p ((single₀ I).obj X).obj Y) p.$$$$

Lean4

/-- Given `F : C ⥤ D ⥤ D`, `X : C`, `e : F.obj X ≅ 𝟭 D`, `Y : GradedObject J D` and
`p : I × J → J` such that `p ⟨0, j⟩ = j` for all `j`,
this is the left unitor isomorphism `mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y`. -/
noncomputable def mapBifunctorLeftUnitor : mapBifunctorMapObj F p ((single₀ I).obj X) Y ≅ Y :=
  isoMk _ _ (fun j => (CofanMapObjFun.iso (mapBifunctorLeftUnitorCofanIsColimit F X e p hp Y j)).symm)

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