basicOpen_appLE — Mathlib

English

There is a canonical basic open construction arising from the appLE map, yielding an equality with a lattice intersection of opens.

Русский

Существует каноническое конструирование базового открытого, получаемое из карты appLE, приводящее к равенству между открытыми через пересечение.

LaTeX

$$$X.basicOpen\\left( f_{appLE}(V,U,e,s) \\right) = U \\cap \\left( (\\text{map } f).basicOpen s \\right)$$$

Lean4

theorem basicOpen_appLE {X Y : Scheme.{u}} (f : X ⟶ Y) (U : X.Opens) (V : Y.Opens) (e : U ≤ f ⁻¹ᵁ V) (s : Γ(Y, V)) :
    X.basicOpen (f.appLE V U e s) = U ⊓ f ⁻¹ᵁ (Y.basicOpen s) :=
  by
  simp only [preimage_basicOpen, Hom.appLE, CommRingCat.comp_apply]
  rw [basicOpen_res]

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