map₂_yonedaEquivFst — Mathlib

English

The fst-component of map₂ is yoneda.map f followed by p.fst.

Русский

Первая компонента map₂ равна yoneda.map f затем p.fst.

LaTeX

$$$\\forall {X Y} (f : X ⟶ Y) (p : YonedaCollection F Y), (YonedaCollection.map₂ F f p).fst = yoneda.map f ≫ p.fst$$$

Lean4

@[simp]
theorem map₂_yonedaEquivFst {Y : C} (f : X ⟶ Y) (p : YonedaCollection F Y) :
    (YonedaCollection.map₂ F f p).yonedaEquivFst = A.map f.op p.yonedaEquivFst := by
  simp only [YonedaCollection.yonedaEquivFst_eq, map₂_fst, yonedaEquiv_naturality]

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