English
The image of Aut F inside the product is exactly the compatible families across arrows.
Русский
Изображение Aut F во внутреннем произведении ровно множество совместимых семейств по стрелкам.
LaTeX
$$$\\operatorname{range}(\\mathrm{autEmbedding}(F))=\\bigcap_{f:\\operatorname{Arrow} C} \\{a\\mid F.map f.hom \\circ (a f.right).hom = (a f.left).hom \\circ F.map f.hom\\}$$$
Lean4
/-- The image of `Aut F` in `∀ X, Aut (F.obj X)` are precisely the compatible families of
automorphisms. -/
theorem autEmbedding_range :
Set.range (autEmbedding F) = ⋂ (f : Arrow C), {a | F.map f.hom ≫ (a f.right).hom = (a f.left).hom ≫ F.map f.hom} :=
by
ext a
simp only [Set.mem_range, id_obj, Set.mem_iInter, Set.mem_setOf_eq]
refine ⟨fun ⟨σ, h⟩ i ↦ h.symm ▸ σ.hom.naturality i.hom, fun h ↦ ?_⟩
· use NatIso.ofComponents a (fun {X Y} f ↦ h ⟨X, Y, f⟩)
rfl
