Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.IdealSheafData.coe_support_mkOfMemSupportIff

∀ {X : AlgebraicGeometry.Scheme} (ideal : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U)))
  (map_ideal_basicOpen :
    ∀ (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)
  (supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)),
  ↑(AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff ideal map_ideal_basicOpen supportSet
          supportSet_inter).support =
    supportSet

Defined in

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

Cited by

0 results in Mathlib

Foundations

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