toOpen_eq — Mathlib

English

Equality expressing relation of open objects via toOpen and Spec construction.

Русский

Эквивалентность отношений открытых подмножеств через toOpen и конструктор Spec.

LaTeX

$$$ \text{toOpen}_{R}(U) = (\GammaSpecIso R)^{-1} \circ (\mathrm{Spec}R).presheaf.map (\mathrm{homOfLE} \ le_{\mathrm top}).op $$$

Lean4

theorem toOpen_eq (U) :
    (by exact StructureSheaf.toOpen R U) = (ΓSpecIso R).inv ≫ (Spec R).presheaf.map (homOfLE le_top).op :=
  rfl

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