instPreservesFiniteLimitsActionFintypeCatForget

English

Finite G implies that the category of finite sets has colimits of shape a single object G in arbitrary universes.

Русский

Для конечной группы G категория конечных множеств имеет колимиты формы одного объекта G во всех теориях множеств.

LaTeX

$$$\\text{HasColimitsOfShape}(\\mathrm{SingleObj}\\,G, \\mathrm{FintypeCat})$$$

Lean4

noncomputable instance : PreservesFiniteLimits (forget (Action FintypeCat G)) :=
  by
  change PreservesFiniteLimits (Action.forget FintypeCat _ ⋙ FintypeCat.incl)
  apply comp_preservesFiniteLimits

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