Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsAffineOpen.mem_ideal_iff

∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {s : ↑(X.presheaf.obj (Opposite.op U))} {I : Ideal ↑(X.presheaf.obj (Opposite.op U))},
      s ∈ I ↔
        ∀ (x : ↥X) (h : x ∈ U),
          (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x h)) s ∈
            Ideal.map (CommRingCat.Hom.hom (X.presheaf.germ U x h)) I

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

1 results in Mathlib

Foundations

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