basicOpen_eq_of_affine' — Mathlib

English

For f in Γ(Spec R, ⊤), the basic open in Spec R corresponding to f equals the basic open of PrimeSpectrum via the natural iso: Spec R basicOpen f = PrimeSpectrum.basicOpen f.

Русский

Для f в Γ(Spec R, ⊤) соответствующая базовая открытая подмножество в Spec R равна базовой открытой подмножеству в PrimeSpectrum через натуральную изоморфность: Spec R basicOpen f = PrimeSpectrum.basicOpen f.

LaTeX

$$$(\mathrm{Spec} R).basicOpen f = \mathrm{PrimeSpectrum}.basicOpen f$$$

Lean4

@[simp]
theorem basicOpen_eq_of_affine' {R : CommRingCat} (f : Γ(Spec R, ⊤)) :
    (Spec R).basicOpen f = PrimeSpectrum.basicOpen ((Scheme.ΓSpecIso R).hom f) :=
  by
  convert basicOpen_eq_of_affine ((Scheme.ΓSpecIso R).hom f)
  exact (Iso.hom_inv_id_apply (Scheme.ΓSpecIso R) f).symm

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