instMulActionAutCarrierVFintypeCatFunctorObjActionFunctorToAction

English

For each object X, the group Aut X acts on the fiber (F.obj X) via the action transported by functorToAction F.

Русский

Для каждого объекта X группа Aut X действует на волокне F(X) через соответствующее действие, перенесённое functorToAction F.

LaTeX

$$$\\forall X,\\; Aut(X) \\curvearrowright F.obj(X) \\quad\\text{via } ((functorToAction F).obj X).V$$$

Lean4

instance (X : C) : MulAction (Aut X) ((functorToAction F).obj X).V :=
  inferInstanceAs <| MulAction (Aut X) (F.obj X)

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