ofIdeals — Mathlib

English

Given a family I of ideals indexed by affine opens, the construction ofIdeals(I) yields the largest ideal sheaf data whose component-wise ideals are bounded above by I.

Русский

Дано семейство I из идеалов, отсчитываемых по аффинным открытым поддиапазонам; конструкция ofIdeals(I) возвращает наибольшие данные идеалов, чьи компонентные идеалы не превышают I.

LaTeX

$$$\operatorname{ofIdeals}(I) = \sup\{ J \in X.\text{IdealSheafData} \mid J.ideal \le I \}$$$

Lean4

/-- The largest ideal sheaf contained in a family of ideals. -/
def ofIdeals (I : ∀ U : X.affineOpens, Ideal Γ(X, U)) : IdealSheafData X :=
  sSup {J : IdealSheafData X | J.ideal ≤ I}

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