equivOfIsAffine — Mathlib

English

Over affine schemes, there is a bijection between ideal sheaves and ideals of global sections.

Русский

Для аффинных схем существует биекция между идеальными слоями и идеалами глобальных секций.

LaTeX

$$equivOfIsAffine(X) : IdealSheafData X ≃o Ideal Γ(X, ⊤)$$

Lean4

/-- Over affine schemes, ideal sheaves are in bijection with ideals of the global sections. -/
@[simps]
def equivOfIsAffine [IsAffine X] : IdealSheafData X ≃o Ideal Γ(X, ⊤)
    where
  toFun := (ideal · ⟨⊤, isAffineOpen_top X⟩)
  invFun := ofIdealTop
  left_inv I := ext_of_isAffine (by simp)
  right_inv I := by simp
  map_rel_iff' {I J} := ⟨le_of_isAffine, (· _)⟩

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