counitForward_naturality₁ — Mathlib

English

The snd component of counitForward matches the prescribed F.map of the snd component under an appropriate equation.

Русский

Вторая компонента counitForward совпадает с отображением F по snd-компоненте согласно заданному равенству.

LaTeX

$$$$ (counitForward F s x).val.snd = F.map (eqToHom (by \text{ simp } [\leftarrow CostructuredArrow.eq_mk])) x $$$$

Lean4

@[simp]
theorem counitForward_naturality₁ {G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (η : F ⟶ G)
    (s : (CostructuredArrow yoneda A)ᵒᵖ) (x : F.obj s) :
    counitForward G s.unop (η.app s x) =
      OverArrows.map₁ (counitForward F s.unop x) (yonedaCollectionPresheafMap₁ η) (by cat_disch) :=
  OverArrows.ext <| YonedaCollection.ext (by simp) (by simp)

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