Documentation Verification Report

Etale

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

Statistics

Metric	Count
Definitions `IsEtale`, `forget`, `forgetFullyFaithful`, `instCategoryEtale`	4
Theorems `eq_smoothOfRelativeDimension_zero`, `etale_appLE`, `etale_comp`, `etale_isStableUnderBaseChange`, `iff_smoothOfRelativeDimension_zero`, `instFormallyUnramified`, `instFstScheme`, `instHasOfPostcompPropertyScheme`, `instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified`, `instHasRingHomPropertyEtale`, `instIsMultiplicativeScheme`, `instMorphismRestrict`, `instOfIsOpenImmersion`, `instResLE`, `instSmooth`, `instSmoothOfRelativeDimensionOfNatNat`, `instSndScheme`, `of_comp`, `etale_appLE`, `instFaithfulEtaleOverForget`, `instFullEtaleOverForget`, `instHasPullbacksEtale`, `etale_iff`	23
Total	27

AlgebraicGeometry

Definitions

Name	Category	Theorems
`IsEtale` 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`etale_iff` 📖	mathematical	—	`Etale` `RingHom.Etale` `CommRingCat.carrier` `CategoryTheory.Functor.obj` `Opposite` `TopologicalSpace.Opens` `TopCat.carrier` `PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `SheafedSpace.toPresheafedSpace` `LocallyRingedSpace.toSheafedSpace` `Scheme.toLocallyRingedSpace` `TopCat.str` `CategoryTheory.Category.opposite` `Preorder.smallCategory` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `PresheafedSpace.presheaf` `Opposite.op` `Scheme.Opens` `CommRingCat.commRing` `CommRingCat.Hom.hom` `Scheme.Hom.appLE`	—	—

AlgebraicGeometry.Etale

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_smoothOfRelativeDimension_zero` 📖	mathematical	—	`AlgebraicGeometry.Etale` `AlgebraicGeometry.SmoothOfRelativeDimension`	—	`AlgebraicGeometry.HasRingHomProperty.ext` `instHasRingHomPropertyEtale` `AlgebraicGeometry.instHasRingHomPropertySmoothOfRelativeDimensionLocallyIsStandardSmoothOfRelativeDimension` `RingHom.etale_iff_isStandardSmoothOfRelativeDimension_zero` `RingHom.locally_iff_of_localizationSpanTarget` `RingHom.Etale.respectsIso` `RingHom.Etale.ofLocalizationSpanTarget`
`etale_appLE` 📖	mathematical	`AlgebraicGeometry.Scheme.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'`	`RingHom.Etale` `CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `AlgebraicGeometry.Scheme.Hom.appLE`	—	—
`etale_comp` 📖	mathematical	—	`AlgebraicGeometry.Etale` `CategoryTheory.CategoryStruct.comp` `AlgebraicGeometry.Scheme` `CategoryTheory.Category.toCategoryStruct` `AlgebraicGeometry.Scheme.instCategory`	—	`CategoryTheory.MorphismProperty.comp_mem` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `instIsMultiplicativeScheme`
`etale_isStableUnderBaseChange` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsStableUnderBaseChange` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Etale`	—	`AlgebraicGeometry.HasRingHomProperty.isStableUnderBaseChange` `instHasRingHomPropertyEtale` `RingHom.Etale.isStableUnderBaseChange`
`iff_smoothOfRelativeDimension_zero` 📖	mathematical	—	`AlgebraicGeometry.Etale` `AlgebraicGeometry.SmoothOfRelativeDimension`	—	`eq_smoothOfRelativeDimension_zero`
`instFormallyUnramified` 📖	mathematical	—	`AlgebraicGeometry.FormallyUnramified`	—	`RingHom.Etale.formallyUnramified` `AlgebraicGeometry.Scheme.Hom.etale_appLE`
`instFstScheme` 📖	mathematical	—	`AlgebraicGeometry.Etale` `CategoryTheory.Limits.pullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.fst`	—	`CategoryTheory.MorphismProperty.pullback_fst` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `etale_isStableUnderBaseChange`
`instHasOfPostcompPropertyScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasOfPostcompProperty` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Etale`	—	`CategoryTheory.MorphismProperty.HasOfPostcompProperty.of_le` `instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified` `AlgebraicGeometry.instLocallyOfFiniteTypeOfLocallyOfFinitePresentation` `AlgebraicGeometry.instLocallyOfFinitePresentationOfSmooth` `instSmooth` `instFormallyUnramified`
`instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified` 📖	mathematical	—	`CategoryTheory.MorphismProperty.HasOfPostcompProperty` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Etale` `CategoryTheory.MorphismProperty` `CategoryTheory.Category.toCategoryStruct` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `ConditionallyCompleteLattice.toLattice` `CompleteLattice.toConditionallyCompleteLattice` `CompleteBooleanAlgebra.toCompleteLattice` `CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra` `AlgebraicGeometry.LocallyOfFiniteType` `AlgebraicGeometry.FormallyUnramified`	—	`AlgebraicGeometry.Scheme.Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.hasOfPostcompProperty_iff_le_diagonal` `etale_isStableUnderBaseChange` `instIsMultiplicativeScheme` `CategoryTheory.MorphismProperty.IsStableUnderBaseChange.inf` `AlgebraicGeometry.locallyOfFiniteType_isStableUnderBaseChange` `AlgebraicGeometry.FormallyUnramified.instIsStableUnderBaseChangeScheme` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `instOfIsOpenImmersion` `AlgebraicGeometry.FormallyUnramified.isOpenImmersion_diagonal`
`instHasRingHomPropertyEtale` 📖	mathematical	—	`AlgebraicGeometry.HasRingHomProperty` `AlgebraicGeometry.Etale` `RingHom.Etale`	—	`RingHom.Etale.propertyIsLocal` `CategoryTheory.MorphismProperty.ext` `AlgebraicGeometry.etale_iff` `AlgebraicGeometry.affineLocally_iff_forall_isAffineOpen`
`instIsMultiplicativeScheme` 📖	mathematical	—	`CategoryTheory.MorphismProperty.IsMultiplicative` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Etale`	—	`AlgebraicGeometry.HasRingHomProperty.isMultiplicative` `instHasRingHomPropertyEtale` `RingHom.Etale.stableUnderComposition` `RingHom.Etale.containsIdentities`
`instMorphismRestrict` 📖	mathematical	—	`AlgebraicGeometry.Etale` `AlgebraicGeometry.Scheme.Opens.toScheme` `CategoryTheory.Functor.obj` `AlgebraicGeometry.Scheme.Opens` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `TopCat.str` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'` `AlgebraicGeometry.morphismRestrict`	—	`AlgebraicGeometry.IsZariskiLocalAtTarget.restrict` `AlgebraicGeometry.HasRingHomProperty.instIsZariskiLocalAtTarget` `instHasRingHomPropertyEtale`
`instOfIsOpenImmersion` 📖	mathematical	—	`AlgebraicGeometry.Etale`	—	`AlgebraicGeometry.HasRingHomProperty.of_isOpenImmersion` `instHasRingHomPropertyEtale` `RingHom.Etale.containsIdentities`
`instResLE` 📖	mathematical	`AlgebraicGeometry.Scheme.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `AlgebraicGeometry.Scheme.Hom.toLRSHom'`	`AlgebraicGeometry.Etale` `AlgebraicGeometry.Scheme.Opens.toScheme` `AlgebraicGeometry.Scheme.Hom.resLE`	—	`etale_comp` `instOfIsOpenImmersion` `AlgebraicGeometry.instIsOpenImmersionHomOfLE` `instMorphismRestrict`
`instSmooth` 📖	mathematical	—	`AlgebraicGeometry.Smooth`	—	`AlgebraicGeometry.SmoothOfRelativeDimension.smooth` `instSmoothOfRelativeDimensionOfNatNat`
`instSmoothOfRelativeDimensionOfNatNat` 📖	mathematical	—	`AlgebraicGeometry.SmoothOfRelativeDimension`	—	`iff_smoothOfRelativeDimension_zero`
`instSndScheme` 📖	mathematical	—	`AlgebraicGeometry.Etale` `CategoryTheory.Limits.pullback` `AlgebraicGeometry.Scheme` `AlgebraicGeometry.Scheme.instCategory` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.Limits.pullback.snd`	—	`CategoryTheory.MorphismProperty.pullback_snd` `AlgebraicGeometry.Scheme.Pullback.instHasPullback` `CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeAlongOfIsStableUnderBaseChange` `etale_isStableUnderBaseChange`
`of_comp` 📖	mathematical	—	`AlgebraicGeometry.Etale`	—	`CategoryTheory.MorphismProperty.of_postcomp` `instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified`

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
`instCategoryEtale` 📖	CompOp	3 math math: `instFullEtaleOverForget`, `instFaithfulEtaleOverForget`, `instHasPullbacksEtale`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFaithfulEtaleOverForget` 📖	mathematical	—	`CategoryTheory.Functor.Faithful` `Etale` `instCategoryEtale` `CategoryTheory.Over` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.instCategoryOver` `Etale.forget`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.Comma.instFaithfulCommaForget`
`instFullEtaleOverForget` 📖	mathematical	—	`CategoryTheory.Functor.Full` `Etale` `instCategoryEtale` `CategoryTheory.Over` `AlgebraicGeometry.Scheme` `instCategory` `CategoryTheory.instCategoryOver` `Etale.forget`	—	`CategoryTheory.MorphismProperty.IsMultiplicative.instTop` `CategoryTheory.MorphismProperty.Comma.instFullTopCommaForget`
`instHasPullbacksEtale` 📖	mathematical	—	`CategoryTheory.Limits.HasPullbacks` `Etale` `instCategoryEtale`	—	`CategoryTheory.MorphismProperty.Over.hasPullbacks` `Pullback.instHasPullbacks` `CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition` `AlgebraicGeometry.Etale.instIsMultiplicativeScheme` `AlgebraicGeometry.Etale.etale_isStableUnderBaseChange` `AlgebraicGeometry.Etale.instHasOfPostcompPropertyScheme`

AlgebraicGeometry.Scheme.Etale

Definitions

Name	Category	Theorems
`forget` 📖	CompOp	2 math math: `AlgebraicGeometry.Scheme.instFullEtaleOverForget`, `AlgebraicGeometry.Scheme.instFaithfulEtaleOverForget`
`forgetFullyFaithful` 📖	CompOp	—

AlgebraicGeometry.Scheme.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`etale_appLE` 📖	mathematical	`AlgebraicGeometry.Scheme.Opens` `Preorder.toLE` `PartialOrder.toPreorder` `TopologicalSpace.Opens.instPartialOrder` `TopCat.carrier` `AlgebraicGeometry.PresheafedSpace.carrier` `CommRingCat` `CommRingCat.instCategory` `AlgebraicGeometry.SheafedSpace.toPresheafedSpace` `AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace` `AlgebraicGeometry.Scheme.toLocallyRingedSpace` `AlgebraicGeometry.SheafedSpace.instTopologicalSpaceCarrierCarrier` `CategoryTheory.Functor.obj` `Preorder.smallCategory` `TopologicalSpace.Opens` `TopCat.str` `TopologicalSpace.Opens.map` `AlgebraicGeometry.PresheafedSpace.Hom.base` `AlgebraicGeometry.LocallyRingedSpace.Hom.toHom` `toLRSHom'`	`RingHom.Etale` `CommRingCat.carrier` `Opposite` `CategoryTheory.Category.opposite` `AlgebraicGeometry.PresheafedSpace.presheaf` `Opposite.op` `CommRingCat.commRing` `CommRingCat.Hom.hom` `appLE`	—	`AlgebraicGeometry.Etale.etale_appLE`

---

← Back to Index