English
Let f: F → G be a morphism of presheaves on C, and for an object U in C, a type s in G.obj(U). For any g: V → U.unop and the data hg ensuring a local preimage exists, the image of the localPreimage under f equals the canonical image of s along G. In symbols, f_U(localPreimage(f, s, g, hg)) = G.map(g^{op})(s).
Русский
Пусть f: F → G — морфизм непрерывных препространств на C. Пусть U — объект C, s ∈ G.obj(U). Для любого g: V → U, и данных hg, обеспечивающих существование локального предобраза, образ локального предобраза через f совпадает с каноническим отображением s по G. Обозначения: f_U(localPreimage(f, s, g, hg)) = G.map(g^{op})(s).
LaTeX
$$$ f_U\big(\mathrm{localPreimage}(f, s, g, hg)\big) = G\big( g^{op} \big)(s) $$$
Lean4
@[simp]
theorem app_localPreimage {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) {U : Cᵒᵖ} (s : ToType (G.obj U)) {V : C} (g : V ⟶ U.unop)
(hg : imageSieve f s g) : f.app _ (localPreimage f s g hg) = G.map g.op s :=
hg.choose_spec
