Etale

📁 Source: Mathlib/AlgebraicGeometry/Sites/Etale.lean

Statistics

Metric	Count
Definitions Etale, Etale, etalePrecoverage, etalePretopology, etaleTopology, geometricFiber, smallEtalePretopology, smallEtaleTopology	8
Theorems instEtaleF, zariskiTopology_le_etaleTopology	2
Total	10

AlgebraicGeometry

Definitions

Name	Category	Theorems
Etale 📖	CompData	17 math math: Etale.instOfIsOpenImmersion, Etale.instFstScheme, Etale.of_comp, Etale.instSndScheme, Etale.instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified, Etale.instIsMultiplicativeScheme, Etale.instResLE, Etale.instHasRingHomPropertyEtale, Etale.etale_isStableUnderBaseChange, Scheme.instEtaleF, Etale.instHasOfPostcompPropertyScheme, Etale.etale_comp, etale_iff, Etale.iff_smoothOfRelativeDimension_zero, Etale.instMorphismRestrict, Etale.eq_smoothOfRelativeDimension_zero, exists_etale_isCompl_of_quasiFiniteAt

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
Etale 📖	CompOp	3 math math: instFullEtaleOverForget, instFaithfulEtaleOverForget, instHasPullbacksEtale
etalePrecoverage 📖	CompOp	—
etalePretopology 📖	CompOp	—
etaleTopology 📖	CompOp	1 math math: zariskiTopology_le_etaleTopology
geometricFiber 📖	CompOp	—
smallEtalePretopology 📖	CompOp	—
smallEtaleTopology 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instEtaleF 📖	mathematical	—	AlgebraicGeometry.Etale CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage CategoryTheory.PreZeroHypercover.f	—	Cover.map_prop
zariskiTopology_le_etaleTopology 📖	mathematical	—	CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme instCategory CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology zariskiTopology etaleTopology	—	grothendieckTopology_monotone AlgebraicGeometry.Etale.instOfIsOpenImmersion

---

← Back to Index