English
If G is a finite group, the inclusion of finite G-sets into finite types preserves colimits indexed by the one-object category with endomorphism G, i.e., preserves limits/colimits of shape SingleObj G.
Русский
Если G — конечная группа, включение конечных G-наборов в конечные множества сохраняет колимиты индексируемые одной объектной категорией с концевой группой G; то есть сохраняются колимиты формы SingleObj G.
LaTeX
$$$\operatorname{PreservesColimitsOfShape}(\mathrm{SingleObj}\,G,\mathrm{FintypeCat.incl}).$$$
Lean4
noncomputable instance {G : Type v} [Group G] [Finite G] : PreservesColimitsOfShape (SingleObj G) FintypeCat.incl.{w} :=
by
choose G' hg hf e using Finite.exists_type_univ_nonempty_mulEquiv G
exact Limits.preservesColimitsOfShape_of_equiv (Classical.choice e).toSingleObjEquiv.symm _
