homEquiv_apply_π — Mathlib

English

For F1,F2 with HasEnrichedHom V F1 F2, the homEquiv evaluated at the identity functor 𝟙 F1 gives the enriched identity; i.e., the bijection sends the identity natural transformation to the enriched identity.

Русский

Для F1,F2 с HadEnrichedHom V F1 F2 отображение homEquiv на тождественный функтор 𝟙 F1 даёт обогащённый тождественный морфизм; биекция отправляет тождественную натTrans в обогащённый тождественный.

LaTeX

$$$\\text{homEquiv } V (\\mathrm{id}_{F_1}) = \\mathrm{enrichedId } V F_1.$$$

Lean4

@[reassoc (attr := simp)]
theorem homEquiv_apply_π (τ : F₁ ⟶ F₂) (j : J) : homEquiv V τ ≫ enrichedHomπ V _ _ j = eHomEquiv V (τ.app j) := by
  simp [homEquiv]

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