instHasEnrichedHomUnderCompMapForget

English

The simplification lemma for homEquiv of identity: it equals enrichedId on F₁ F₂.

Русский

Лемма упрощения для homEquiv от идентичности: равняется enrichedId на F₁ F₂.

LaTeX

$$$\\mathrm{homEquiv}_V(\\mathbf{1}_{F_1}) = \\mathrm{enrichedId}_V F_1$$$

Lean4

instance {j j' : J} (f : j ⟶ j') :
    HasEnrichedHom V (Under.map f ⋙ Under.forget j ⋙ F₁) (Under.map f ⋙ Under.forget j ⋙ F₂) :=
  inferInstanceAs (HasEnrichedHom V (Under.forget j' ⋙ F₁) (Under.forget j' ⋙ F₂))

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