English
For any i: op U ⟶ op V between opens of X, the inverse of the appIso is natural with respect to the presheaf maps: X.presheaf.map i ∘ (f.appIso V)^{-1} = (f.appIso U)^{-1} ∘ Y.presheaf.map (f.opensFunctor.op.map i).
Русский
Для любых открытых множеств U ⊆ X, V ⊆ X и отображения i: op U ⟶ op V, обратная карта из appIso сочетается с отображениями сохраняемости: X.presheaf.map i · (f.appIso V)^{-1} = (f.appIso U)^{-1} · Y.presheaf.map (f.opensFunctor.op.map i).
LaTeX
$$$$X.presheaf.map(i) \circ (f.appIso(V))^{-1} = (f.appIso(U))^{-1} \circ Y.presheaf.map(f.opensFunctor^{op}.map(i)).$$$$
Lean4
@[reassoc (attr := simp)]
theorem appIso_inv_naturality {U V : X.Opens} (i : op U ⟶ op V) :
X.presheaf.map i ≫ (f.appIso V).inv = (f.appIso U).inv ≫ Y.presheaf.map (f.opensFunctor.op.map i) :=
PresheafedSpace.IsOpenImmersion.inv_naturality _ _
