English
Let F be a fiber functor. Then Aut X acts on F.obj X by σ • a = F.map(σ.hom) a, with the usual unit and compatibility: 1 • a = a and (gh) • a = g • (h • a).
Русский
Пусть F — фибер-функтор. Тогда группа Aut X действует на F.obj X следующим образом: σ • a = F.map(σ.hom) a, и выполняются тождества 1 • a = a и (gh) • a = g • (h • a).
LaTeX
$$$\sigma \cdot a = F.map(\sigma.hom)\,a$,\quad $1\cdot a = a$,\quad $(gh)\cdot a = g\cdot(h\cdot a)$.$$
Lean4
/-- The natural action of `Aut X` on `F.obj X`. -/
instance autMulFiber (F : C ⥤ FintypeCat.{w}) (X : C) : MulAction (Aut X) (F.obj X)
where
smul σ a := F.map σ.hom a
one_smul
a := by
change F.map (𝟙 X) a = a
simp only [map_id, FintypeCat.id_apply]
mul_smul g h
a := by
change F.map (h.hom ≫ g.hom) a = (F.map h.hom ≫ F.map g.hom) a
simp only [map_comp, FintypeCat.comp_apply]
