Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.jointlySurjectiveTopology

CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme

The jointly surjective topology on Scheme is defined by the same condition as the jointly surjective pretopology.

Defined in
Mathlib.AlgebraicGeometry.Sites.Pretopology
Cited by
2 results in Mathlib
Foundations
Depth 198 from the axioms · uses propext, Classical.choice, Quot.sound
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

AlgebraicGeometry.Scheme.jointlySurjectiveTopology_eq_toGrothendieck_jointlySurjectivePretopology · cited by 0Scheme.jointlySurjectiveT…AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology · cited by 0Scheme.mem_jointlySurject…Set.ofPred · cited by 6101Set.ofPredAlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeCategoryTheory.GrothendieckTopology · cited by 1415CategoryTheory.Grothendie…CategoryTheory.Sieve · cited by 552CategoryTheory.SieveCategoryTheory.Sieve.arrows · cited by 446Sieve.arrowsCategoryTheory.Precoverage.coverings · cited by 194Precoverage.coveringsCategoryTheory.Pretopology.toPrecoverage · cited by 34Pretopology.toPrecoverageCategoryTheory.Pretopology.toGrothendieck · cited by 18Pretopology.toGrothendieckAlgebraicGeometry.Scheme.jointlySurjectivePretopology · cited by 4Scheme.jointlySurjectiveP…CategoryTheory.GrothendieckTopology.copy · cited by 3GrothendieckTopology.copyScheme.jointlySurjectiveTopol…CITED BYCITES

Cites10

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

Cited by2

Results whose statement or proof uses this declaration.