preservesColimits_forget — Mathlib

English

The forgetful functor preserves colimits, by the same evaluation-based natural isomorphism.

Русский

Функтор забывания сохраняет колимиты через аналогичную натуральную изоморфность.

LaTeX

$$preservesColimits_forget (V) (G) : PreservesColimits (forget V G)$$

Lean4

noncomputable instance preservesColimits_forget [HasColimits V] : PreservesColimits (forget V G) :=
  preservesColimits_of_natIso
    (Action.functorCategoryEquivalenceCompEvaluation V G)
      -- TODO construct categorical images?

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