Proetale

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

Statistics

Metric	Count
Definitions ProEt, equivOfIsEmpty, forget, forgetFullyFaithful, mk, precoverage, topology, instCategoryProEt, instHasFiniteLimitsProEt, instHasIsosProetalePrecoverage, instIsStableUnderBaseChangeProetalePrecoverage, instIsStableUnderCompositionProetalePrecoverage, proetalePrecoverage, proetaleTopology	14
Theorems bot_mem_topology, forget_map, forget_obj, instFaithfulOverForget, instFullOverForget, instIsContinuousCompOverForgetForgetTopologyProetaleTopology, instIsContinuousOverForgetTopologyOverProetaleTopology, instLocallyCoverDenseOverForgetOverProetaleTopology, instPreservesFiniteLimitsOverForget, instRepresentablyFlatOverForget, instSubcanonicalTopology, instWeaklyEtaleHomDiscretePUnit, mk_hom, mk_left, mk_right_as, topology_eq_inducedTopology, topology_eq_top_of_isEmpty, etalePrecoverage_le_proetalePrecoverage, etaleTopology_le_proetaleTopology, instSubcanonicalProetaleTopology, instWeaklyEtaleF, proetalePrecoverage_le_fpqcPrecoverage, proetalePrecoverage_le_precoverage_weaklyEtale, proetaleTopology_eq_propQCTopology, proetaleTopology_le_fpqcTopology	25
Total	39

AlgebraicGeometry.Scheme

Definitions

Name	Category	Theorems
ProEt 📖	CompOp	15 math math: ProEt.instIsContinuousCompOverForgetForgetTopologyProetaleTopology, ProEt.forget_obj, ProEt.instSubcanonicalTopology, ProEt.instLocallyCoverDenseOverForgetOverProetaleTopology, ProEt.topology_eq_inducedTopology, ProEt.forget_map, ProEt.instFaithfulOverForget, ProEt.instPreservesFiniteLimitsOverForget, ProEt.bot_mem_topology, isZero_ellAdicSheaf_of_isEmpty, ProEt.instFullOverForget, ProEt.instRepresentablyFlatOverForget, instIsGrothendieckAbelianSheafProEtTopologyAb, ProEt.topology_eq_top_of_isEmpty, ProEt.instIsContinuousOverForgetTopologyOverProetaleTopology
instCategoryProEt 📖	CompOp	15 math math: ProEt.instIsContinuousCompOverForgetForgetTopologyProetaleTopology, ProEt.forget_obj, ProEt.instSubcanonicalTopology, ProEt.instLocallyCoverDenseOverForgetOverProetaleTopology, ProEt.topology_eq_inducedTopology, ProEt.forget_map, ProEt.instFaithfulOverForget, ProEt.instPreservesFiniteLimitsOverForget, ProEt.bot_mem_topology, isZero_ellAdicSheaf_of_isEmpty, ProEt.instFullOverForget, ProEt.instRepresentablyFlatOverForget, instIsGrothendieckAbelianSheafProEtTopologyAb, ProEt.topology_eq_top_of_isEmpty, ProEt.instIsContinuousOverForgetTopologyOverProetaleTopology
instHasFiniteLimitsProEt 📖	CompOp	—
instHasIsosProetalePrecoverage 📖	CompOp	—
instIsStableUnderBaseChangeProetalePrecoverage 📖	CompOp	—
instIsStableUnderCompositionProetalePrecoverage 📖	CompOp	—
proetalePrecoverage 📖	CompOp	3 math math: proetalePrecoverage_le_precoverage_weaklyEtale, etalePrecoverage_le_proetalePrecoverage, proetalePrecoverage_le_fpqcPrecoverage
proetaleTopology 📖	CompOp	8 math math: ProEt.instIsContinuousCompOverForgetForgetTopologyProetaleTopology, ProEt.instLocallyCoverDenseOverForgetOverProetaleTopology, ProEt.topology_eq_inducedTopology, proetaleTopology_eq_propQCTopology, etaleTopology_le_proetaleTopology, instSubcanonicalProetaleTopology, ProEt.instIsContinuousOverForgetTopologyOverProetaleTopology, proetaleTopology_le_fpqcTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
etalePrecoverage_le_proetalePrecoverage 📖	mathematical	—	CategoryTheory.Precoverage AlgebraicGeometry.Scheme instCategory Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder etalePrecoverage proetalePrecoverage	—	proetalePrecoverage.eq_1 propQCPrecoverage.eq_1 etalePrecoverage.eq_1 le_inf_iff precoverage_le_qcPrecoverage_of_isOpenMap Hom.isOpenMap AlgebraicGeometry.UniversallyOpen.of_flat AlgebraicGeometry.WeaklyEtale.flat AlgebraicGeometry.WeaklyEtale.instOfEtale AlgebraicGeometry.instLocallyOfFinitePresentationOfSmooth AlgebraicGeometry.Etale.instSmooth precoverage_mono
etaleTopology_le_proetaleTopology 📖	mathematical	—	CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme instCategory CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology etaleTopology proetaleTopology	—	CategoryTheory.Precoverage.toGrothendieck_mono etalePrecoverage_le_proetalePrecoverage
instSubcanonicalProetaleTopology 📖	mathematical	—	CategoryTheory.GrothendieckTopology.Subcanonical AlgebraicGeometry.Scheme instCategory proetaleTopology	—	CategoryTheory.GrothendieckTopology.Subcanonical.of_le proetaleTopology_le_fpqcTopology instSubcanonicalFpqcTopology
instWeaklyEtaleF 📖	mathematical	—	AlgebraicGeometry.WeaklyEtale CategoryTheory.PreZeroHypercover.X AlgebraicGeometry.Scheme instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage CategoryTheory.PreZeroHypercover.f	—	Cover.map_prop
proetalePrecoverage_le_fpqcPrecoverage 📖	mathematical	—	CategoryTheory.Precoverage AlgebraicGeometry.Scheme instCategory Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder proetalePrecoverage fpqcPrecoverage	—	propQCPrecoverage_monotone AlgebraicGeometry.WeaklyEtale.flat
proetalePrecoverage_le_precoverage_weaklyEtale 📖	mathematical	—	CategoryTheory.Precoverage AlgebraicGeometry.Scheme instCategory Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder proetalePrecoverage CategoryTheory.MorphismProperty.precoverage AlgebraicGeometry.WeaklyEtale	—	le_trans inf_le_right
proetaleTopology_eq_propQCTopology 📖	mathematical	—	proetaleTopology propQCTopology AlgebraicGeometry.WeaklyEtale	—	—
proetaleTopology_le_fpqcTopology 📖	mathematical	—	CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme instCategory CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology proetaleTopology fpqcTopology	—	CategoryTheory.Precoverage.toGrothendieck_mono proetalePrecoverage_le_fpqcPrecoverage

AlgebraicGeometry.Scheme.ProEt

Definitions

Name	Category	Theorems
equivOfIsEmpty 📖	CompOp	—
forget 📖	CompOp	10 math math: instIsContinuousCompOverForgetForgetTopologyProetaleTopology, forget_obj, instLocallyCoverDenseOverForgetOverProetaleTopology, topology_eq_inducedTopology, forget_map, instFaithfulOverForget, instPreservesFiniteLimitsOverForget, instFullOverForget, instRepresentablyFlatOverForget, instIsContinuousOverForgetTopologyOverProetaleTopology
forgetFullyFaithful 📖	CompOp	—
mk 📖	CompOp	—
precoverage 📖	CompOp	—
topology 📖	CompOp	8 math math: instIsContinuousCompOverForgetForgetTopologyProetaleTopology, instSubcanonicalTopology, topology_eq_inducedTopology, bot_mem_topology, AlgebraicGeometry.Scheme.isZero_ellAdicSheaf_of_isEmpty, AlgebraicGeometry.Scheme.instIsGrothendieckAbelianSheafProEtTopologyAb, topology_eq_top_of_isEmpty, instIsContinuousOverForgetTopologyOverProetaleTopology

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_mem_topology 📖	mathematical	—	CategoryTheory.Sieve AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve topology Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.Sieve.instCompleteLattice BoundedOrder.toOrderBot CompleteLattice.toBoundedOrder	—	instLocallyCoverDenseOverForgetOverProetaleTopology CategoryTheory.Functor.IsLocallyFull.of_full instFullOverForget CategoryTheory.Functor.IsLocallyFaithful.of_faithful instFaithfulOverForget topology_eq_inducedTopology CategoryTheory.Sieve.functorPushforward_bot CategoryTheory.Sieve.overEquiv_bot
forget_map 📖	mathematical	—	CategoryTheory.Functor.map AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt CategoryTheory.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.instCategoryOver forget CategoryTheory.MorphismProperty.Comma.Hom.hom CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit AlgebraicGeometry.WeaklyEtale Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	CategoryTheory.MorphismProperty.IsMultiplicative.instTop
forget_obj 📖	mathematical	—	CategoryTheory.Functor.obj AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt CategoryTheory.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.instCategoryOver forget CategoryTheory.MorphismProperty.Comma.toComma CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit AlgebraicGeometry.WeaklyEtale Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—
instFaithfulOverForget 📖	mathematical	—	CategoryTheory.Functor.Faithful AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt CategoryTheory.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.instCategoryOver forget	—	—
instFullOverForget 📖	mathematical	—	CategoryTheory.Functor.Full AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt CategoryTheory.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.instCategoryOver forget	—	—
instIsContinuousCompOverForgetForgetTopologyProetaleTopology 📖	mathematical	—	CategoryTheory.Functor.IsContinuous AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.comp CategoryTheory.Over CategoryTheory.instCategoryOver forget CategoryTheory.Over.forget topology AlgebraicGeometry.Scheme.proetaleTopology	—	CategoryTheory.Functor.isContinuous_comp instIsContinuousOverForgetTopologyOverProetaleTopology CategoryTheory.GrothendieckTopology.instIsContinuousOverForgetOver
instIsContinuousOverForgetTopologyOverProetaleTopology 📖	mathematical	—	CategoryTheory.Functor.IsContinuous AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt CategoryTheory.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.instCategoryOver forget topology CategoryTheory.GrothendieckTopology.over AlgebraicGeometry.Scheme.proetaleTopology	—	instLocallyCoverDenseOverForgetOverProetaleTopology CategoryTheory.Functor.IsLocallyFull.of_full instFullOverForget CategoryTheory.Functor.IsLocallyFaithful.of_faithful instFaithfulOverForget topology_eq_inducedTopology CategoryTheory.Functor.isContinuous_of_coverPreserving CategoryTheory.compatiblePreservingOfFlat instRepresentablyFlatOverForget CategoryTheory.Functor.inducedTopology_coverPreserving
instLocallyCoverDenseOverForgetOverProetaleTopology 📖	mathematical	—	CategoryTheory.Functor.LocallyCoverDense AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt CategoryTheory.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.instCategoryOver forget CategoryTheory.GrothendieckTopology.over AlgebraicGeometry.Scheme.proetaleTopology	—	CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition AlgebraicGeometry.WeaklyEtale.instIsMultiplicativeScheme CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks AlgebraicGeometry.Scheme.proetalePrecoverage_le_precoverage_weaklyEtale
instPreservesFiniteLimitsOverForget 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt CategoryTheory.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.instCategoryOver forget	—	—
instRepresentablyFlatOverForget 📖	mathematical	—	CategoryTheory.RepresentablyFlat AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt CategoryTheory.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.instCategoryOver forget	—	CategoryTheory.flat_of_preservesFiniteLimits instPreservesFiniteLimitsOverForget
instSubcanonicalTopology 📖	mathematical	—	CategoryTheory.GrothendieckTopology.Subcanonical AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt topology	—	CategoryTheory.GrothendieckTopology.subcanonical_of_full_of_faithful instFullOverForget instFaithfulOverForget instIsContinuousOverForgetTopologyOverProetaleTopology CategoryTheory.GrothendieckTopology.subcanonical_over AlgebraicGeometry.Scheme.instSubcanonicalProetaleTopology
instWeaklyEtaleHomDiscretePUnit 📖	mathematical	—	AlgebraicGeometry.WeaklyEtale CategoryTheory.Functor.obj AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Functor.id CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra CategoryTheory.Comma.right CategoryTheory.Comma.hom	—	CategoryTheory.MorphismProperty.Comma.prop
mk_hom 📖	mathematical	—	CategoryTheory.Comma.hom AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma AlgebraicGeometry.WeaklyEtale Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—
mk_left 📖	mathematical	—	CategoryTheory.Comma.left AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma AlgebraicGeometry.WeaklyEtale Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—
mk_right_as 📖	mathematical	—	CategoryTheory.Discrete.as CategoryTheory.Comma.right AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.MorphismProperty.Comma.toComma AlgebraicGeometry.WeaklyEtale Top.top CategoryTheory.MorphismProperty CategoryTheory.Category.toCategoryStruct BooleanAlgebra.toTop CompleteBooleanAlgebra.toBooleanAlgebra CategoryTheory.MorphismProperty.instCompleteBooleanAlgebra	—	—
topology_eq_inducedTopology 📖	mathematical	—	topology CategoryTheory.Functor.inducedTopology AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt CategoryTheory.Over AlgebraicGeometry.Scheme AlgebraicGeometry.Scheme.instCategory CategoryTheory.instCategoryOver forget CategoryTheory.GrothendieckTopology.over AlgebraicGeometry.Scheme.proetaleTopology instLocallyCoverDenseOverForgetOverProetaleTopology CategoryTheory.Functor.IsLocallyFull.of_full instFullOverForget CategoryTheory.Functor.IsLocallyFaithful.of_faithful instFaithfulOverForget	—	CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition AlgebraicGeometry.WeaklyEtale.instIsMultiplicativeScheme CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks AlgebraicGeometry.Scheme.Pullback.instHasPullbacks AlgebraicGeometry.Scheme.proetalePrecoverage_le_precoverage_weaklyEtale
topology_eq_top_of_isEmpty 📖	mathematical	—	topology Top.top CategoryTheory.GrothendieckTopology AlgebraicGeometry.Scheme.ProEt AlgebraicGeometry.Scheme.instCategoryProEt OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice CategoryTheory.GrothendieckTopology.instCompleteLattice BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	CategoryTheory.GrothendieckTopology.eq_top_iff Function.isEmpty bot_mem_topology

---

← Back to Index