Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff

{X : AlgebraicGeometry.Scheme} →
  (ideal : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))) →
    (∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))),
        Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal U) =
          ideal (X.affineBasicOpen f)) →
      (supportSet : Set ↥X) →
        (∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)) → X.IdealSheafData

A useful constructor of IdealSheafData with the condition on supportSet being easier to check.

Defined in

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Cited by

2 results in Mathlib

Foundations

Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound