functorEnriched_id_comp — Mathlib

English

The component at π maps the homEquiv to the corresponding eHomEquiv value for the component at j.

Русский

Компонент на π сопоставляет homEquiv соответствующий eHomEquiv для компоненты при j.

LaTeX

$$$\\mathrm{homEquiv}_V(\\tau) \\circ \\mathrm{enrichedHom}\\pi_{F_1,F_2}(j) = eHomEquiv_V(\\tau.app(j))$$$

Lean4

@[reassoc (attr := simp)]
theorem functorEnriched_id_comp [HasFunctorEnrichedHom V F₁ F₂] [HasFunctorEnrichedHom V F₁ F₁] :
    (λ_ (functorEnrichedHom V F₁ F₂)).inv ≫
        functorEnrichedId V F₁ ▷ functorEnrichedHom V F₁ F₂ ≫ functorEnrichedComp V F₁ F₁ F₂ =
      𝟙 (functorEnrichedHom V F₁ F₂) :=
  by cat_disch

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