Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsAffineOpen.ideal_le_iff

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

Defined in

Mathlib.AlgebraicGeometry.AffineScheme

Cited by

1 results in Mathlib

Foundations

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