English
Restricted to finite sets, the locally constant presheaf is naturally isomorphic to the finite Yoneda embedding of F.
Русский
Ограничивая локально константный предшествователь на конечные множества, имеется естественная изоморфность между локально константным предшественником и конечнойYoneda-эмбеддингом F.
LaTeX
$$$\\text{locallyConstantIsoFinYonYon} (F):\\; (toProfinite^{op} \\!\\circ\\! (\\text{locallyConstantPresheaf } (F)) ) \\cong \\mathrm{finYoneda}\; F$$$
Lean4
/-- `locallyConstantPresheaf` restricted to finite sets is isomorphic to `finYoneda F`. -/
@[simps! hom_app]
def locallyConstantIsoFinYoneda :
toProfinite.op ⋙ (locallyConstantPresheaf (F.obj (toProfinite.op.obj ⟨of PUnit.{u + 1}⟩))) ≅ finYoneda F :=
NatIso.ofComponents fun Y ↦
{ hom := fun f ↦ f.1
inv := fun f ↦ ⟨f, @IsLocallyConstant.of_discrete _ _ _ ⟨rfl⟩ _⟩ }
