enrichedComp_π — Mathlib

English

There is a natural bijection between ordinary morphisms from F₁ to F₂ and enriched morphisms from the corresponding enriched functors, given by the homEquiv.

Русский

Существует естественная биекция между обычными морфизмами от F₁ к F₂ и обогащёнными морфизмами между соответствующими обогащёнными функторaми, задаваемая через гом‑эквивалентность.

LaTeX

$$$\\mathrm{homEquiv}_V: (F_1 \\to F_2) \\simeq (\\mathbb{1}_V \\to \\mathrm{enrichedHom}\; V\\; F_1\\; F_2)$$$

Lean4

@[reassoc (attr := simp)]
theorem enrichedComp_π (j : J) :
    enrichedComp V F₁ F₂ F₃ ≫ end_.π _ j = (end_.π (diagram V F₁ F₂) j ⊗ₘ end_.π (diagram V F₂ F₃) j) ≫ eComp V _ _ _ :=
  by simp [enrichedComp]

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