IsFraction — Mathlib

English

For positive-degree homogeneous data, the stalk of Spec at a prime is isomorphic to the corresponding localization, giving an explicit equivalence between the two local rings.

Русский

Для однородной информации с положительной степенью градации, stalk Spec в простом идеале изоморфен соответствующей локализации; явное эквивалентное соответствие локальных колец.

LaTeX

$$$$\mathrm{presheaf}\;\text{stalk} \cong \mathrm{Localization}$$$$

Lean4

/-- The predicate saying that a dependent function on an open `U` is realised as a fixed fraction
`r / s` of *same grading* in each of the stalks (which are localizations at various prime ideals).
-/
def IsFraction {U : Opens (ProjectiveSpectrum.top 𝒜)} (f : ∀ x : U, at x.1) : Prop :=
  ∃ (i : ℕ) (r s : 𝒜 i) (s_nin : ∀ x : U, s.1 ∉ x.1.asHomogeneousIdeal), ∀ x : U, f x = .mk ⟨i, r, s, s_nin x⟩

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