Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.qcPrecoverage

CategoryTheory.Precoverage AlgebraicGeometry.Scheme

The quasi-compact precoverage on the category of schemes is the precoverage given by quasi-compact covers. The intersection of this precoverage with the precoverage defined by jointly surjective families of flat morphisms is the fpqc-precoverage.

Defined in
Mathlib.AlgebraicGeometry.Sites.QuasiCompact
Cited by
7 results in Mathlib
Foundations
Depth 150 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.propQCPrecoverage · cited by 10Scheme.propQCPrecoverageAlgebraicGeometry.Scheme.presieve₀_mem_qcPrecoverage_iff · cited by 4Scheme.presieve₀_mem_qcPr…AlgebraicGeometry.Scheme.precoverage_le_qcPrecoverage_of_isOpenMap · cited by 3Scheme.precoverage_le_qcP…AlgebraicGeometry.Scheme.propQCPrecoverage_monotone · cited by 1Scheme.propQCPrecoverage_…AlgebraicGeometry.Scheme.Hom.singleton_mem_qcPrecoverage · cited by 1Hom.singleton_mem_qcPreco…AlgebraicGeometry.Scheme.bot_mem_qcPrecoverage · cited by 1Scheme.bot_mem_qcPrecover…AlgebraicGeometry.Scheme.zariskiPrecoverage_le_qcPrecoverage · cited by 1Scheme.zariskiPrecoverage…AlgebraicGeometry.Scheme.etalePrecoverage_le_proetalePrecoverage · cited by 1Scheme.etalePrecoverage_l…AlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeCategoryTheory.Precoverage · cited by 204CategoryTheory.PrecoverageCategoryTheory.PreZeroHypercoverFamily.precoverage · cited by 6PreZeroHypercoverFamily.p…AlgebraicGeometry.Scheme.qcCoverFamily · cited by 1Scheme.qcCoverFamilyScheme.qcPrecoverageCITED BYCITES

Cites4

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

Cited by8

Results whose statement or proof uses this declaration.