limitEquivFixedPoints — Mathlib

English

The limit of a functor J: SingleObj G ⥤ Type is canonically equivalent to the fixed points of the induced G-action on J(star G).

Русский

Предел Functor J: SingleObj G ⥤ Type эквивалентен фиксированным точкам порождаемого действия G на J(star G).

LaTeX

$$$\\lim J \\;\cong\\; \\operatorname{Fix}_G(J(\\mathrm{star} G))$$$

Lean4

/-- The limit of `J : SingleObj M ⥤ Type u` is equivalent to the fixed points of the
induced action on `J.obj (SingleObj.star M)`. -/
@[simps!]
noncomputable def limitEquivFixedPoints : limit J ≃ MulAction.fixedPoints M (J.obj (SingleObj.star M)) :=
  (Types.limitEquivSections J).trans (Types.sections.equivFixedPoints J)

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