instHasFiniteProducts — Mathlib

English

If V has finite limits, then the action category Action V G has finite limits as well.

Русский

Если у категории V существуют конечные пределы, то у категории действий Action V G существуют конечные пределы.

LaTeX

$$$\operatorname{HasFiniteProducts}(\mathrm{Action}(V,G)).$$$

Lean4

instance [HasFiniteProducts V] : HasFiniteProducts (Action V G) where
  out _ := Adjunction.hasLimitsOfShape_of_equivalence (Action.functorCategoryEquivalence _ _).functor

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