Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology

∀ {X : AlgebraicGeometry.Scheme} {U : X.AffineZariskiSite} {s : Set ↑(X.presheaf.obj (Opposite.op U.toOpens))},
  CategoryTheory.Sieve.generate (U.presieveOfSections s) ∈
      (AlgebraicGeometry.Scheme.AffineZariskiSite.grothendieckTopology X) U ↔
    Ideal.span s = ⊤

Defined in: Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Cited by: 1 results in Mathlib
Foundations: Depth 164 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.

Cites47

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

DFunLike.coestatement and proof · cited by 62,936
Setstatement and proof · cited by 53,352
Quiver.Homproof · cited by 32,603
CategoryTheory.Functor.objstatement and proof · cited by 19,642
Top.topstatement · cited by 9,680
SetLike.coeproof · cited by 8,199
Oppositestatement · cited by 8,081
Set.Elemproof · cited by 7,166
Idealstatement · cited by 4,748
mul_oneproof · cited by 3,885
TopCat.carrierstatement and proof · cited by 3,184
AlgebraicGeometry.Schemestatement and proof · cited by 2,540

Cited by1

Results whose statement or proof uses this declaration.

AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieveproof · cited by 0