English
Let f: X → Y be a morphism of schemes, with U, U' ⊆ Y open and V ⊆ X open, and e: V ≤ f^{-1}(U). If i: U' = U, then the natural map on sections along i composed with the appLE map at U' and V equals the appLE map at U and V applied to e; i.e. Y.presheaf.map (eqToHom i)^{op} ∘ f.appLE U' V (i ▸ e) = f.appLE U V e. This expresses naturality of the appLE construction with respect to equality of opens.
Русский
Пусть f: X → Y — морфизм схем, U, U' ⊆ Y — открытые подмножества, V ⊆ X — открытое, и e: V ≤ f^{-1}(U). При i: U' = U выполняется равенство: Y.presheaf.map (eqToHom i)^{op} ∘ f.appLE U' V (i ▸ e) = f.appLE U V e. Это выражает естественность конструкции appLE по отношению к равенству открытых множеств.
LaTeX
$$$Y.presheaf.map (eqToHom i)^{op} \\circ f.appLE U' V (i \\; ▸ \\; e) = f.appLE U V e$$$
Lean4
@[reassoc]
theorem map_appLE' (e : V ≤ f ⁻¹ᵁ U) (i : U' = U) :
Y.presheaf.map (eqToHom i).op ≫ f.appLE U' V (i ▸ e) = f.appLE U V e :=
map_appLE _ _ _
