Theorems · Theorem · algebraic geometry

AlgebraicGeometry.IsAffineOpen.iSup_basicOpen_eq_self_iff

∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {s : Set ↑(X.presheaf.obj (Opposite.op U))}, ⨆ f, X.basicOpen ↑f = U ↔ Ideal.span s = ⊤

In an affine open set U, a family of basic open covers U iff the sections span Γ(X, U). See iSup_basicOpen_of_span_eq_top for the inverse direction without the affine-ness assumption.

Defined in: Mathlib.AlgebraicGeometry.AffineScheme
Cited by: 2 results in Mathlib
Foundations: Depth 152 from the axioms · uses propext, Classical.choice, Quot.sound

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites57

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

DFunLike.coeproof · cited by 62,936
Setstatement and proof · cited by 53,352
CategoryTheory.Functor.objstatement and proof · cited by 19,642
Top.topstatement and proof · cited by 9,680
SetLike.coeproof · cited by 8,199
Oppositestatement · cited by 8,081
Set.Elemstatement and proof · cited by 7,166
Set.imageproof · cited by 5,609
Set.preimageproof · cited by 4,946
Idealstatement · cited by 4,748
Set.rangeproof · cited by 4,705
CategoryTheory.ConcreteCategory.homproof · cited by 4,022

Cited by2

Results whose statement or proof uses this declaration.

AlgebraicGeometry.IsAffineOpen.self_le_iSup_basicOpen_iffproof · cited by 3
AlgebraicGeometry.iSup_basicOpen_of_span_eq_topproof · cited by 2