Mathlib Map

Theorems · Definition · algebraic geometry

AlgebraicGeometry.Scheme.smallEtaleTopology

(X : AlgebraicGeometry.Scheme) → CategoryTheory.GrothendieckTopology X.Etale

The small étale site of a scheme is the Grothendieck topology on the category of schemes étale over X induced from the étale topology on Scheme.{u}.

Defined in
Mathlib.AlgebraicGeometry.Sites.Etale
Cited by
9 results in Mathlib
Foundations
Depth 108 from the axioms · uses propext, Classical.choice, Quot.sound

Around this declaration

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

AlgebraicGeometry.Scheme.pointSmallEtale · cited by 7Scheme.pointSmallEtaleAlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage · cited by 4Scheme.pointSmallEtaleFib…AlgebraicGeometry.Scheme.ofArrows_mem_smallEtaleTopology_iff · cited by 1Scheme.ofArrows_mem_small…AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_coe · cited by 1Scheme.pointSmallEtaleFib…AlgebraicGeometry.Scheme.isConservative_pointSmallEtale · cited by 1Scheme.isConservative_poi…AlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage_surjective · cited by 1Scheme.pointSmallEtaleFib…AlgebraicGeometry.Scheme.AffineEtale.sheafEquiv · cited by 1AffineEtale.sheafEquivAlgebraicGeometry.Scheme.AffineEtale.topology · cited by 1AffineEtale.topologyAlgebraicGeometry.Scheme.isConservativeFamilyOfPoints_pointSmallEtale' · cited by 0Scheme.isConservativeFami…AlgebraicGeometry.Scheme.pointSmallEtale_fiber · cited by 0Scheme.pointSmallEtale_fi…AlgebraicGeometry.Scheme.pointSmallEtale.congr_simp · cited by 0pointSmallEtale.congr_simpAlgebraicGeometry.Scheme.pointSmallEtaleFiberObjToPreimage.congr_simp · cited by 0pointSmallEtaleFiberObjTo…AlgebraicGeometry.Scheme.AffineEtale.sheafEquiv_inverse · cited by 0AffineEtale.sheafEquiv_in…AlgebraicGeometry.Scheme · cited by 2540AlgebraicGeometry.SchemeCategoryTheory.GrothendieckTopology · cited by 1415CategoryTheory.Grothendie…AlgebraicGeometry.Etale · cited by 27AlgebraicGeometry.EtaleAlgebraicGeometry.Scheme.Etale · cited by 16Scheme.EtaleAlgebraicGeometry.Scheme.smallGrothendieckTopology · cited by 3Scheme.smallGrothendieckT…Scheme.smallEtaleTopologyCITED 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.