map_val — Mathlib

English

In the Yoneda-special situation, the first component of mk s x equals s.

Русский

В ситуации Yoneda, первая компонента mk s x равна s.

LaTeX

$$$\\forall {s} {x},\\; (mk\\ s\\ x).fst = s$$$

Lean4

/-- In the special case `F = yoneda.obj Y`, the element `p.val` for `p : OverArrows η s` is itself
a morphism `X ⟶ Y`. -/
@[simp]
theorem map_val {Y : C} {η : yoneda.obj Y ⟶ A} {X : C} {s : yoneda.obj X ⟶ A} (p : OverArrows η s) :
    yoneda.map p.val ≫ η = s :=
  by
  rw [← yonedaEquiv.injective.eq_iff, yonedaEquiv_comp, yonedaEquiv_yoneda_map]
  simp only [unop_op, p.app_val]

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