Theorems · Theorem · algebraic geometry

AlgebraicGeometry.Scheme.exists_cover_of_mem_grothendieckTopology

∀ {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

Alias of the forward direction of AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff.

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

Cites19

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
AlgebraicGeometry.Schemestatement and proof · cited by 2,540
CategoryTheory.MorphismPropertystatement and proof · cited by 2,179
CategoryTheory.GrothendieckTopologystatement · cited by 1,415
CategoryTheory.PreZeroHypercover.I₀statement · cited by 763
CategoryTheory.PreZeroHypercover.Xstatement · cited by 649
CategoryTheory.Sievestatement and proof · cited by 552
CategoryTheory.PreZeroHypercover.fstatement · cited by 542
CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercoverstatement · cited by 469
CategoryTheory.Presievestatement · cited by 449
CategoryTheory.Sieve.arrowsstatement · cited by 446

Cited by1

Results whose statement or proof uses this declaration.

AlgebraicGeometry.Scheme.overGrothendieckTopology_eq_toGrothendieck_overPretopologyproof · cited by 1