Etale

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

Statistics

Metric	Count
Definitions IsEtale, forget, forgetFullyFaithful, instFaithfulOverEtaleTopMorphismPropertyOverForget, instFullOverEtaleTopMorphismPropertyOverForget, instCategoryEtale, instHasPullbacksEtale	7
Theorems eq_smoothOfRelativeDimension_zero, etale_appLE, etale_comp, etale_isStableUnderBaseChange, iff_flat_and_formallyUnramified, iff_smoothOfRelativeDimension_zero, instFormallyUnramified, instFstScheme, instHasOfPostcompPropertyScheme, instHasOfPostcompPropertySchemeMinMorphismPropertyLocallyOfFiniteTypeFormallyUnramified, instHasRingHomPropertyEtale, instIsMultiplicativeScheme, instMorphismRestrict, instOfIsOpenImmersion, instResLE, instSmooth, instSmoothOfRelativeDimensionOfNatNat, instSndScheme, of_comp, of_formallyUnramified_of_flat, etale_appLE, etale_iff	22
Total	29

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 CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens 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_flat_and_formallyUnramified 📖	mathematical	—	AlgebraicGeometry.Etale AlgebraicGeometry.Flat AlgebraicGeometry.FormallyUnramified AlgebraicGeometry.LocallyOfFinitePresentation	—	AlgebraicGeometry.etale_iff AlgebraicGeometry.flat_iff AlgebraicGeometry.formallyUnramified_iff AlgebraicGeometry.locallyOfFinitePresentation_iff
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 instOfIsOpenImmersion AlgebraicGeometry.Scheme.Pullback.instHasPullback 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
of_formallyUnramified_of_flat 📖	mathematical	—	AlgebraicGeometry.Etale	—	iff_flat_and_formallyUnramified

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
instCategoryEtale 📖	CompOp	—
instHasPullbacksEtale 📖	CompOp	—

AlgebraicGeometry.Scheme.Etale

Definitions

Name	Category	Theorems
forget 📖	CompOp	—
forgetFullyFaithful 📖	CompOp	—
instFaithfulOverEtaleTopMorphismPropertyOverForget 📖	CompOp	—
instFullOverEtaleTopMorphismPropertyOverForget 📖	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 CategoryTheory.Functor.obj Opposite TopologicalSpace.Opens TopCat.carrier AlgebraicGeometry.PresheafedSpace.carrier CommRingCat CommRingCat.instCategory AlgebraicGeometry.SheafedSpace.toPresheafedSpace AlgebraicGeometry.LocallyRingedSpace.toSheafedSpace AlgebraicGeometry.Scheme.toLocallyRingedSpace TopCat.str CategoryTheory.Category.opposite Preorder.smallCategory PartialOrder.toPreorder TopologicalSpace.Opens.instPartialOrder AlgebraicGeometry.PresheafedSpace.presheaf Opposite.op AlgebraicGeometry.Scheme.Opens CommRingCat.commRing CommRingCat.Hom.hom appLE	—	AlgebraicGeometry.Etale.etale_appLE

---

← Back to Index