instHasColimitsOfShapeSingleObjOfFinite

English

For every finite group G, the shape SingleObj(G) has colimits in C.

Русский

Для каждого конечного группы G форма SingleObj(G) имеет колимиты в C.

LaTeX

$$$\\forall C\\,[\\mathrm{Category}(C) \\land \\mathrm{PreGaloisCategory}(C) \\Rightarrow \\forall G\\,[\\mathrm{Group}(G) \\land \\mathrm{Finite}(G) \\Rightarrow \\mathrm{HasColimitsOfShape}(\\mathrm{SingleObj}(G), C)]]$$$

Lean4

instance {G : Type*} [Group G] [Finite G] : HasColimitsOfShape (SingleObj G) C :=
  by
  obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G
  exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm

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