inv_naturality — Mathlib

English

For an open immersion f, every stalk map f.stalkMap x is an isomorphism.

Русский

Для открытого вложения f все стежковые отображения f.stalkMap x являются изоморфизмами.

LaTeX

$$$\forall x:\, X,\ IsIso(f.stalkMap(x))$$$

Lean4

@[reassoc (attr := simp)]
theorem inv_naturality {U V : (Opens X)ᵒᵖ} (i : U ⟶ V) :
    X.presheaf.map i ≫ H.invApp _ (unop V) = H.invApp _ (unop U) ≫ Y.presheaf.map (opensFunctor f |>.op.map i) :=
  PresheafedSpace.IsOpenImmersion.inv_naturality f.1 i

Похожие утверждения