coyonedaPairing_map — Mathlib

English

For P,Q in the product C × (C ⥤ Type), α : P ⟶ Q and β ∈ (coyonedaPairing C).obj P, the pairing map equals the composition coyoneda.map α.fst.op ≫ β ≫ α.snd.

Русский

Для P,Q ∈ произведения C × (C ⥤ Type), α : P ⟶ Q и β ∈ (coyonedaPairing C).obj P, отображение pairing удовлетворяет равенству: (coyonedaPairing C).map α β = coyoneda.map α.fst.op ≫ β ≫ α.snd.

LaTeX

$$$$ (coyonedaPairing(C)).map \alpha \beta = coyoneda.map \alpha.fst.op \;\gg\; \beta \;\gg\; \alpha.snd $$$$

Lean4

@[simp]
theorem coyonedaPairing_map (P Q : C × (C ⥤ Type v₁)) (α : P ⟶ Q) (β : (coyonedaPairing C).obj P) :
    (coyonedaPairing C).map α β = coyoneda.map α.1.op ≫ β ≫ α.2 :=
  rfl

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