GrothendieckTopology

📁 Source: Mathlib/Topology/Category/TopCat/GrothendieckTopology.lean

Statistics

Metric	Count
Definitions GrothendieckTopology, grothendieckTopology, instHasIsosPrecoverage, instIsStableUnderBaseChangePrecoverage, instIsStableUnderCompositionPrecoverage, isOpenEmbedding, precoverage	7
Theorems exists_mem_zeroHypercover_range, instIsContinuousUliftFunctorGrothendieckTopology, instIsMultiplicativeIsOpenEmbedding, instIsStableUnderBaseChangeIsOpenEmbedding, instRespectsIsoIsOpenEmbedding, instSmallPrecoverage, isOpenEmbedding_f_zeroHypercover, isOpenEmbedding_iff, precoverage_le_comap_uliftFunctor, subcanonical_grothendieckTopology	10
Total	17

CategoryTheory

Definitions

Name	Category	Theorems
GrothendieckTopology 📖	CompData	161 math math: sheafBotEquivalence_functor, AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology, GrothendieckTopology.mem_toPretopology, GrothendieckTopology.superset_covering, instHasSheafifyBotGrothendieckTopology, GrothendieckTopology.ext_iff, Precoverage.toGrothendieck_le_iff_le_toPrecoverage, AlgebraicGeometry.Scheme.mem_grothendieckTopology_iff, AlgebraicGeometry.Scheme.zariskiTopology_le_etaleTopology, GrothendieckTopology.OneHypercover.mem₀, Functor.OneHypercoverDenseData.mem₁, Presieve.isSheaf_bot, GrothendieckTopology.transitive, Functor.functorPushforward_imageSieve_mem, extensiveTopology.mem_sieves_iff_contains_colimit_cofan, Pretopology.toGrothendieck_mono, Functor.functorPushforward_mem_iff, GrothendieckTopology.trivial_covering, AlgebraicGeometry.Scheme.zariskiTopology_le_fpqcTopology, GrothendieckTopology.intersection_covering_iff, AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology, Presheaf.isLocallyInjective_iff_equalizerSieve_mem_imp, Precoverage.galoisConnection_toGrothendieck_toPrecoverage, GrothendieckTopology.OneHypercover.mem_sieve₁', Pretopology.mem_toGrothendieck, GrothendieckTopology.Cover.preOneHypercover_sieve₀, Precoverage.toGrothendieck_mono, Coverage.toGrothendieck_eq_sInf, Coverage.mem_toGrothendieck_sieves_of_superset, le_topology_of_closedSieves_isSheaf, GrothendieckTopology.top_mem, Functor.IsLocallyFull.functorPushforward_imageSieve_mem, sheafBotEquivalence_inverse_map_hom, GrothendieckTopology.overEquiv_symm_mem_over, Functor.OneHypercoverDenseData.mem₁₀, Functor.is_cover_of_isCoverDense, GrothendieckTopology.mem_over_iff, GrothendieckTopology.toGrothendieck_toPrecoverage_le, regularTopology.mem_sieves_iff_hasEffectiveEpi, GrothendieckTopology.coversTop_iff_of_isTerminal, GrothendieckTopology.bot_covers, Functor.functorPushforward_equalizer_mem, Functor.IsDenseSubsite.equalizer_mem, GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac, GrothendieckTopology.close_eq_top_iff_mem, GrothendieckTopology.coe_copy, GrothendieckTopology.pointBotFunctor_map_hom, AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology, Presheaf.equalizerSieve_mem_of_equalizerSieve_app_mem, GrothendieckTopology.pointBotFunctor_obj, GrothendieckTopology.le_def, GrothendieckTopology.pullback_stable, GrothendieckTopology.discrete_eq_top, AlgebraicGeometry.Scheme.mem_overGrothendieckTopology, GrothendieckTopology.Cover.Arrow.hf, sheafBotEquivalence_unitIso, Precoverage.mem_toGrothendieck_iff, GrothendieckTopology.mem_sInf, GrothendieckTopology.bot_eq_top_iff_isEmpty, GrothendieckTopology.OneHypercover.IsPreservedBy.mem₁, generate_discretePresieve_mem, GrothendieckTopology.isConservative_pointsBot, coherentTopology.mem_sieves_iff_hasEffectiveEpiFamily, Precoverage.generate_mem_toGrothendieck, Functor.LocallyCoverDense.functorPushforward_functorPullback_mem, Functor.pushforward_cover_iff_cover_pullback, Functor.IsDenseSubsite.functorPushforward_mem_iff, Precoverage.mem_toGrothendieck_iff_of_isStableUnderComposition, Presheaf.IsLocallyInjective.equalizerSieve_mem, AlgebraicGeometry.Scheme.Cover.mem_propQCTopology, GrothendieckTopology.Cover.condition, GrothendieckTopology.pointBotPresheafFiberIso_inv, GrothendieckTopology.trivial_eq_bot, Functor.inducedTopology_sieves, GrothendieckTopology.dense_covering, GrothendieckTopology.OneHypercover.IsPreservedBy.mem₀, Functor.OneHypercoverDenseData.sieve_mem, GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac', Functor.OneHypercoverDenseData.mem₀, Functor.IsLocallyFaithful.functorPushforward_equalizer_mem, GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc, GrothendieckTopology.bind_covering, GrothendieckTopology.bot_covering, GrothendieckTopology.mem_sieves_iff_coe, Presheaf.IsLocallySurjective.imageSieve_mem, Precoverage.toGrothendieck_comap_le_inducedTopology, ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem_of_small, Presheaf.isSheaf_bot, Coverage.mem_toGrothendieck, sheafBotEquivalence_inverse_obj_obj, Presheaf.equalizerSieve_mem, GrothendieckTopology.intersection_covering, coherentTopology.mem_sieves_of_hasEffectiveEpiFamily, GrothendieckTopology.Cover.ext_iff, GrothendieckTopology.eq_top_of_isEmpty, GrothendieckTopology.mem_toPrecoverage_iff, CoverPreserving.cover_preserve, AlgebraicGeometry.Scheme.ProEt.bot_mem_topology, GrothendieckTopology.instHasEnoughPointsBot, AlgebraicGeometry.Scheme.grothendieckTopology_monotone, TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology, GrothendieckTopology.pullback_mem_iff_of_isIso, AlgebraicGeometry.Scheme.fppfTopology_le_fpqcTopology, GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_shrinkYoneda_map, GrothendieckTopology.covering_iff_covers_id, GrothendieckTopology.isGLB_sInf, Pretopology.toGrothendieck_bot, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology, AlgebraicGeometry.ofArrows_ι_mem_zariskiTopology_of_isColimit, GrothendieckTopology.toPrecoverage_monotone, GrothendieckTopology.eq_top_iff, Functor.IsCoverDense.is_cover, AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology, regularTopology.mem_sieves_of_hasEffectiveEpi, GrothendieckTopology.instIsIsoFunctorOppositeToPresheafFiberNatTransPointBotCoeEquivHomUnopOpObjTypeShrinkYonedaSymmShrinkYonedaObjObjEquivId, Precoverage.toGrothendieck_monotone, GrothendieckTopology.Cover.Arrow.to_middle_condition, Precoverage.toGrothendieck_bot, regularTopology.exists_effectiveEpi_iff_mem_induced, Precoverage.toGrothendieck_eq_sInf, AlgebraicGeometry.Scheme.etaleTopology_le_proetaleTopology, GrothendieckTopology.top_covers, Sheaf.le_finestTopology, sheafBotEquivalence_counitIso, AlgebraicGeometry.Scheme.ProEt.topology_eq_top_of_isEmpty, coherentTopology.exists_effectiveEpiFamily_iff_mem_induced, ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_ofArrows_mem, GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_uliftYoneda_map, GrothendieckTopology.covers_iff, Functor.cover_lift, AlgebraicGeometry.Scheme.zariskiTopology_le_propQCTopology, GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_cofanIsColimitDesc_uliftYoneda_map, Functor.IsCoverDense.functorPullback_pushforward_covering, GrothendieckTopology.Cover.Arrow.from_middle_condition, Functor.mem_inducedTopology_sieves_iff, GrothendieckTopology.arrows_mem_toPrecoverage_iff, GrothendieckTopology.bindOfArrows, GrothendieckTopology.Subcanonical.le_canonical, AlgebraicGeometry.Scheme.bot_mem_propQCTopology, AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology, GrothendieckTopology.bot_lt_top_iff_nonempty, AlgebraicGeometry.Scheme.Hom.generate_singleton_mem_propQCTopology, GrothendieckTopology.mem_toCoverage_iff, GrothendieckTopology.mem_iff_isSheafFor_closedSieves, GrothendieckTopology.pointBot_fiber, AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve, Functor.IsDenseSubsite.imageSieve_mem, Presheaf.imageSieve_mem, AlgebraicGeometry.Scheme.proetaleTopology_le_fpqcTopology, Functor.IsCocontinuous.cover_lift, GrothendieckTopology.Cover.coe_pullback, Pretopology.sInf_ofGrothendieck, GrothendieckTopology.toPrecoverage_top, discreteSieve_mem, GrothendieckTopology.covering_of_eq_top, GrothendieckTopology.OneHypercover.mem₁, GrothendieckTopology.instSmallPointBotPointsBotOfSmall, AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology, GrothendieckTopology.ofArrows_mem_iff_isLocallySurjective_sigmaDesc_shrinkYoneda_map, GrothendieckTopology.top_covering, GrothendieckTopology.le_canonical

TopCat

Definitions

Name	Category	Theorems
grothendieckTopology 📖	CompOp	3 math math: AlgebraicGeometry.Scheme.instIsContinuousTopCatForgetToTopZariskiTopologyGrothendieckTopology, instIsContinuousUliftFunctorGrothendieckTopology, subcanonical_grothendieckTopology
instHasIsosPrecoverage 📖	CompOp	—
instIsStableUnderBaseChangePrecoverage 📖	CompOp	—
instIsStableUnderCompositionPrecoverage 📖	CompOp	—
isOpenEmbedding 📖	CompOp	4 math math: isOpenEmbedding_iff, instRespectsIsoIsOpenEmbedding, instIsStableUnderBaseChangeIsOpenEmbedding, instIsMultiplicativeIsOpenEmbedding
precoverage 📖	CompOp	4 math math: instSmallPrecoverage, isOpenEmbedding_f_zeroHypercover, precoverage_le_comap_uliftFunctor, exists_mem_zeroHypercover_range

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_mem_zeroHypercover_range 📖	mathematical	—	CategoryTheory.PreZeroHypercover.I₀ TopCat instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage carrier Set Set.instMembership Set.range CategoryTheory.PreZeroHypercover.X DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap str ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Presieve.map_ofArrows CategoryTheory.Precoverage.ZeroHypercover.mem₀
instIsContinuousUliftFunctorGrothendieckTopology 📖	mathematical	—	CategoryTheory.Functor.IsContinuous TopCat instCategory uliftFunctor grothendieckTopology	—	CategoryTheory.Functor.isContinuous_toGrothendieck_of_pullbacksPreservedBy CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits CategoryTheory.Precoverage.instPullbacksPreservedByOfPreservesLimitsOfShapeWalkingCospan CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits CategoryTheory.Limits.PreservesLimits.preservesFiniteLimits instPreservesLimitsOfSizeUliftFunctor precoverage_le_comap_uliftFunctor
instIsMultiplicativeIsOpenEmbedding 📖	mathematical	—	CategoryTheory.MorphismProperty.IsMultiplicative TopCat instCategory isOpenEmbedding	—	Topology.IsOpenEmbedding.id Topology.IsOpenEmbedding.comp
instIsStableUnderBaseChangeIsOpenEmbedding 📖	mathematical	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange TopCat instCategory isOpenEmbedding	—	CategoryTheory.MorphismProperty.IsStableUnderBaseChange.mk' instRespectsIsoIsOpenEmbedding fst_isOpenEmbedding_of_right
instRespectsIsoIsOpenEmbedding 📖	mathematical	—	CategoryTheory.MorphismProperty.RespectsIso TopCat instCategory isOpenEmbedding	—	CategoryTheory.MorphismProperty.respectsIso_of_isStableUnderComposition CategoryTheory.MorphismProperty.IsMultiplicative.toIsStableUnderComposition instIsMultiplicativeIsOpenEmbedding Homeomorph.isOpenEmbedding
instSmallPrecoverage 📖	mathematical	—	CategoryTheory.Precoverage.Small TopCat instCategory precoverage	—	CategoryTheory.Precoverage.Small.inf CategoryTheory.Precoverage.instSmallComap CategoryTheory.Types.instSmallJointlySurjectivePrecoverage
isOpenEmbedding_f_zeroHypercover 📖	mathematical	—	Topology.IsOpenEmbedding carrier CategoryTheory.PreZeroHypercover.X TopCat instCategory CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover precoverage str DFunLike.coe CategoryTheory.ConcreteCategory.hom ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier CategoryTheory.PreZeroHypercover.f	—	CategoryTheory.Precoverage.ZeroHypercover.mem₀
isOpenEmbedding_iff 📖	mathematical	—	isOpenEmbedding Topology.IsOpenEmbedding carrier str DFunLike.coe CategoryTheory.ConcreteCategory.hom TopCat instCategory ContinuousMap ContinuousMap.instFunLike instConcreteCategoryContinuousMapCarrier	—	—
precoverage_le_comap_uliftFunctor 📖	mathematical	—	CategoryTheory.Precoverage TopCat instCategory Preorder.toLE PartialOrder.toPreorder CategoryTheory.Precoverage.instPartialOrder precoverage CategoryTheory.Precoverage.comap uliftFunctor	—	CategoryTheory.Precoverage.le_of_zeroHypercover CategoryTheory.Presieve.map_ofArrows exists_mem_zeroHypercover_range Topology.IsOpenEmbedding.uliftMap isOpenEmbedding_f_zeroHypercover
subcanonical_grothendieckTopology 📖	mathematical	—	CategoryTheory.GrothendieckTopology.Subcanonical TopCat instCategory grothendieckTopology	—	CategoryTheory.GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj CategoryTheory.Precoverage.isSheaf_toGrothendieck_iff_of_isStableUnderBaseChange_of_small CategoryTheory.Precoverage.instHasPullbacksOfHasPullbacks CategoryTheory.Limits.hasLimitsOfShape_widePullbackShape Finite.of_fintype CategoryTheory.Limits.hasFiniteWidePullbacks_of_hasFiniteLimits CategoryTheory.Limits.hasFiniteLimits_of_hasLimits topCat_hasLimits instSmallPrecoverage CategoryTheory.Presieve.isSheafFor_arrows_iff Topology.IsOpenEmbedding.toIsEmbedding isOpenEmbedding_f_zeroHypercover Continuous.comp' ContinuousMapClass.map_continuous ContinuousMap.instContinuousMapClass Homeomorph.continuous CategoryTheory.Limits.PullbackCone.condition Topology.IsEmbedding.toHomeomorph_symm_apply exists_mem_zeroHypercover_range IsOpen.mem_nhds Topology.IsOpenEmbedding.isOpen_range ext ContinuousMap.liftCover_coe

---

← Back to Index