fromSpec_preimage_self — Mathlib

English

For an affine open U in X, the preimage of U under the canonical map from Spec of Γ(X,U) to X equals the whole space.

Русский

Для афинного открытого подмножества U в X предобраз U под каноническим отображением из Spec Γ(X,U) в X есть всякая точка пространства.

LaTeX

$$$h_U^{-1}(U)=\top$$$

Lean4

@[simp]
theorem fromSpec_preimage_self : hU.fromSpec ⁻¹ᵁ U = ⊤ :=
  by
  ext1
  rw [Opens.map_coe, Opens.coe_top, ← hU.range_fromSpec, ← Set.image_univ]
  exact Set.preimage_image_eq _ PresheafedSpace.IsOpenImmersion.base_open.injective

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