basicOpen — Mathlib

English

The basic open set basicOpen 𝒜 f consists of all points x in the projective spectrum for which f is not contained in the homogeneous ideal of x.

Русский

Множество basicOpen 𝒜 f состоит из всех точек x в проективном спектре, для которых f не содержится в однородном идеале x.

LaTeX

$$$\text{basicOpen}_{\mathcal{A}}(f) = \{ x \in \mathrm{ProjSpec}_{\mathcal{A}} \mid f \notin x.asHomogeneousIdeal \}$$$

Lean4

/-- `basicOpen r` is the open subset containing all prime ideals not containing `r`. -/
def basicOpen (r : A) : TopologicalSpace.Opens (ProjectiveSpectrum 𝒜)
    where
  carrier := {x | r ∉ x.asHomogeneousIdeal}
  is_open' := ⟨{ r }, Set.ext fun _ => Set.singleton_subset_iff.trans <| Classical.not_not.symm⟩

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