Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover

(X : AlgebraicGeometry.Scheme) → X.OpenCover

The directed cover of a scheme indexed by X.AffineZariskiSite. Note the related Scheme.directedAffineCover, which has the same (defeq) cover but a different category instance on the indices.

Defined in
Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
Cited by
9 results in Mathlib
Foundations
Depth 148 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.Hom.toNormalization · cited by 28Hom.toNormalizationAlgebraicGeometry.Scheme.Hom.normalizationDesc · cited by 10Hom.normalizationDescAlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData · cited by 5AffineZariskiSite.relativ…AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp · cited by 5Hom.normalizationDesc_compAlgebraicGeometry.Scheme.Hom.ι_fromNormalization · cited by 4Hom.ι_fromNormalizationAlgebraicGeometry.Scheme.Hom.normalizationGlueData · cited by 3Hom.normalizationGlueDataAlgebraicGeometry.Scheme.Hom.ι_toNormalization · cited by 2Hom.ι_toNormalizationAlgebraicGeometry.Scheme.AffineZariskiSite.opensRange_relativeGluingData_map · cited by 1AffineZariskiSite.opensRa…AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.colimitDesc_preimage · cited by 0PreservesLocalization.col…AlgebraicGeometry.Scheme.AffineZariskiSite.PreservesLocalization.opensRange_map · cited by 0PreservesLocalization.ope…AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_I₀ · cited by 0AffineZariskiSite.directe…AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_X · cited by 0AffineZariskiSite.directe…AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover_f · cited by 0AffineZariskiSite.directe…AlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeAlgebraicGeometry.Scheme.Opens.toScheme · cited by 433Opens.toSchemeAlgebraicGeometry.Scheme.Opens.ι · cited by 275Opens.ιAlgebraicGeometry.Scheme.OpenCover · cited by 207Scheme.OpenCoverAlgebraicGeometry.Scheme.AffineZariskiSite · cited by 30Scheme.AffineZariskiSiteAffineZariskiSite.directedCov…CITED BYCITES

Cites5

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

Cited by13

Results whose statement or proof uses this declaration.