instHasColimitsOfShapeSingleObjFintypeCatOfFinite

English

There exists a mono factorization of the lift of Y via a subobject Z in the PreGalois setting, expressing Y as a subobject of F.obj X.

Русский

Существует факторизация мономорфизма подъёма над Z в пред-Галуа-настройке, выражающая Y как подпредмет F.obj X.

LaTeX

$$$\\exists Z:\\, C, \\exists f:\\, Z \\to X, \\exists u:\\, Y \\cong (\\mathrm{functorToAction} F).obj Z, \\text{ with } i = u.hom \\circ (\\mathrm{functorToAction} F).map f$$$

Lean4

/-- The category of finite sets has quotients by finite groups in arbitrary universes. -/
instance [Finite G] : HasColimitsOfShape (SingleObj G) FintypeCat.{w} :=
  by
  obtain ⟨G', hg, hf, ⟨e⟩⟩ := Finite.exists_type_univ_nonempty_mulEquiv G
  exact Limits.hasColimitsOfShape_of_equivalence e.toSingleObjEquiv.symm

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