English
The image of Aut F in the product of Aut(F.obj X) over all objects X consists exactly of the families (a_X) that are compatible across all arrows f: X → Y; i.e., F.map f.hom followed by a_Y.right equals a_X.left followed by F.map f.hom.
Русский
Образ Aut F в произведение Aut(F.obj X) по всем X состоит точно из семейств (a_X), совместимых по всем стрелкам f: X → Y: F.map f.hom ∘ a_X.right = a_Y.left ∘ F.map f.hom.
LaTeX
$$$\\operatorname{range}(\\mathrm{autEmbedding}(F)) = \\bigcap_{f:\\mathrm{Arrow}(C)} \\{a : \\prod_X Aut(F.obj X) \mid F.map f.hom \\circ (a f.right).hom = (a f.left).hom \\circ F.map f.hom\\}$$$
Lean4
/-- The `Aut F` action on the fiber of a connected object is transitive. -/
instance isPretransitive_of_isConnected (X : C) [IsConnected X] : MulAction.IsPretransitive (Aut F) (F.obj X) where
exists_smul_eq x
y := by
let F' : C ⥤ FintypeCat.{u₂} := F ⋙ FintypeCat.uSwitch.{w, u₂}
letI : FiberFunctor F' := FiberFunctor.comp_right _
let e (Y : C) : F'.obj Y ≃ F.obj Y := (F.obj Y).uSwitchEquiv
set x' : F'.obj X := (e X).symm x with hx'
set y' : F'.obj X := (e X).symm y with hy'
obtain ⟨g', (hg' : g'.hom.app X x' = y')⟩ := MulAction.exists_smul_eq (Aut F') x' y'
let gapp (Y : C) : F.obj Y ≅ F.obj Y :=
FintypeCat.equivEquivIso <| (e Y).symm.trans <| (FintypeCat.equivEquivIso.symm (g'.app Y)).trans (e Y)
let g : F ≅ F :=
NatIso.ofComponents gapp <| fun {X Y} f ↦ by
ext x
simp only [FintypeCat.comp_apply, FintypeCat.equivEquivIso_apply_hom, Equiv.trans_apply,
FintypeCat.equivEquivIso_symm_apply_apply, Iso.app_hom, gapp, e]
erw [FintypeCat.uSwitchEquiv_naturality (F.map f)]
rw [← Functor.comp_map, ← FunctorToFintypeCat.naturality]
simp only [comp_obj, Functor.comp_map, F']
rw [FintypeCat.uSwitchEquiv_symm_naturality (F.map f)]
refine ⟨g, show (gapp X).hom x = y from ?_⟩
simp only [FintypeCat.equivEquivIso_apply_hom, Equiv.trans_apply, FintypeCat.equivEquivIso_symm_apply_apply,
Iso.app_hom, gapp]
rw [← hx', hg', hy', Equiv.apply_symm_apply]
