sectionsSubring — Mathlib

English

The sections satisfying the local fraction property form a commutative ring when viewed as sections of the Type-valued structure sheaf.

Русский

Секции, удовлетворяющие свойству локальной дроби, образуют коммутативное кольцо, рассматривая их как секции структуры оболочки значений типа.

LaTeX

$$$$\text{sectionsSubring}(U) \text{ is a } \mathbb{C}$$-ring (Commutative) on appropriate type-valued sections.$$

Lean4

/-- The functions satisfying `isLocallyFraction` form a subring of all dependent functions
`Π x : U, HomogeneousLocalization 𝒜 x`. -/
def sectionsSubring (U : (Opens (ProjectiveSpectrum.top 𝒜))ᵒᵖ) : Subring (∀ x : U.unop, at x.1)
    where
  carrier := {f | (isLocallyFraction 𝒜).pred f}
  zero_mem' := zero_mem' U
  one_mem' := one_mem' U
  add_mem' := add_mem' U _ _
  neg_mem' := neg_mem' U _
  mul_mem' := mul_mem' U _ _

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