yonedaPairing_map — Mathlib

English

For α : P ⟶ Q and β : (yonedaPairing C).obj P, the map is given by a composite: (yonedaPairing C).map α β = yoneda.map α.1.unop ≫ β ≫ α.2.

Русский

Для α : P ⟶ Q и β : (yonedaPairing C).obj P отображение задано композитом: (yonedaPairing C).map α β = yoneda.map α.1.unop ≫ β ≫ α.2.

LaTeX

$$$\bigl(\mathrm{yonedaPairing}\; C\bigr).map \alpha \beta = \yoneda.map \alpha.1.unop \gg \beta \gg \alpha.2$$$

Lean4

@[simp]
theorem yonedaPairing_map (P Q : Cᵒᵖ × (Cᵒᵖ ⥤ Type v₁)) (α : P ⟶ Q) (β : (yonedaPairing C).obj P) :
    (yonedaPairing C).map α β = yoneda.map α.1.unop ≫ β ≫ α.2 :=
  rfl

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