homEquiv_id — Mathlib

English

In enriched functor categories, the isomorphism homEquiv evaluated at the identity equals enrichedId: homEquiv V (𝟙 F₁) = enrichedId V F₁.

Русский

В обогащённых функторных категориях изоморфизм homEquiv, применённый к тождественному морфизму, равен enrichedId: homEquiv V (𝟙 F₁) = enrichedId V F₁.

LaTeX

$$$ \mathrm{homEquiv}\ V\ (\mathbb{1}\ F_1) = \mathrm{enrichedId}\ V\ F_1 $$$

Lean4

@[simp]
theorem homEquiv_id : homEquiv V (𝟙 F₁) = enrichedId V F₁ :=
  rfl

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