Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff

∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [P.IsStableUnderBaseChange] [P.IsMultiplicative]
  {X : AlgebraicGeometry.Scheme} {S : CategoryTheory.Sieve X},
  S ∈ (AlgebraicGeometry.Scheme.grothendieckTopology P) X ↔ ∃ 𝒰, CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f ≤ S.arrows

Defined in: Mathlib.AlgebraicGeometry.Sites.Pretopology
Cited by: 2 results in Mathlib
Foundations: Depth 197 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: CategoryTheory.MorphismProperty.IsStableUnderBaseChange CategoryTheory.MorphismProperty.IsMultiplicative

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites26

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

DFunLike.coestatement · cited by 62,936
Setstatement · cited by 53,352
Quiver.Homproof · cited by 32,603
AlgebraicGeometry.Schemestatement and proof · cited by 2,540
CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
CategoryTheory.GrothendieckTopologystatement · cited by 1,415
le_transproof · cited by 985
CategoryTheory.PreZeroHypercover.I₀statement and proof · cited by 763
CategoryTheory.PreZeroHypercover.Xstatement and proof · cited by 649
CategoryTheory.Sievestatement and proof · cited by 552
CategoryTheory.PreZeroHypercover.fstatement and proof · cited by 542
CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercoverstatement and proof · cited by 469

Cited by2

Results whose statement or proof uses this declaration.

AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopologyproof · cited by 1
AlgebraicGeometry.Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopologyproof · cited by 1