map_basicOpen_map — Mathlib

English

For open U ⊆ X, the image of the inclusion induced map along a restriction aligns with the corresponding open image of V.

Русский

Для открытого U ⊆ X образ изображения включения через ограничение согласуется с соответствующим образом изображения V.

LaTeX

$$$ \\cdots $$$

Lean4

theorem map_basicOpen_map (r : Γ(X, U)) : U.ι ''ᵁ (U.toScheme.basicOpen <| U.topIso.inv r) = X.basicOpen r :=
  by
  simp only [Scheme.Opens.toScheme_presheaf_obj]
  rw [Scheme.map_basicOpen, Scheme.basicOpen_res_eq, Scheme.Opens.topIso_inv, Scheme.basicOpen_res_eq X]

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