Documentation Verification Report

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`, `instIsMultiplicativeIsOpenEmbedding`, `instIsStableUnderBaseChangeIsOpenEmbedding`, `instRespectsIsoIsOpenEmbedding`, `instSmallPrecoverage`, `isOpenEmbedding_f_zeroHypercover`, `isOpenEmbedding_iff`, `subcanonical_grothendieckTopology`	8
Total	15

CategoryTheory

Definitions

Name	Category	Theorems
`GrothendieckTopology` 📖	CompData	115 math math: `sheafBotEquivalence_functor`, `AlgebraicGeometry.Scheme.bot_mem_grothendieckTopology`, `GrothendieckTopology.mem_toPretopology`, `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`, `Functor.functorPushforward_imageSieve_mem`, `extensiveTopology.mem_sieves_iff_contains_colimit_cofan`, `Pretopology.toGrothendieck_mono`, `Functor.functorPushforward_mem_iff`, `GrothendieckTopology.trivial_covering`, `GrothendieckTopology.intersection_covering_iff`, `AlgebraicGeometry.Scheme.mem_jointlySurjectiveTopology_iff_jointlySurjectivePretopology`, `Presheaf.isLocallyInjective_iff_equalizerSieve_mem_imp`, `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`, `Functor.OneHypercoverDenseData.mem₁₀`, `Functor.is_cover_of_isCoverDense`, `AlgebraicGeometry.Scheme.grothendieckTopology_le_grothendieckTopology`, `GrothendieckTopology.mem_over_iff`, `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`, `AlgebraicGeometry.Scheme.AffineZariskiSite.generate_presieveOfSections_mem_grothendieckTopology`, `sheafBotEquivalence_inverse_map_val`, `GrothendieckTopology.le_def`, `GrothendieckTopology.discrete_eq_top`, `AlgebraicGeometry.Scheme.mem_overGrothendieckTopology`, `GrothendieckTopology.Cover.Arrow.hf`, `sheafBotEquivalence_unitIso`, `Precoverage.mem_toGrothendieck_iff`, `GrothendieckTopology.mem_sInf`, `GrothendieckTopology.OneHypercover.IsPreservedBy.mem₁`, `sheafBotEquivalence_inverse_obj_val`, `generate_discretePresieve_mem`, `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`, `GrothendieckTopology.Cover.condition`, `GrothendieckTopology.trivial_eq_bot`, `Functor.inducedTopology_sieves`, `ofGrothendieck_iff`, `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.bot_covering`, `GrothendieckTopology.mem_sieves_iff_coe`, `Presheaf.IsLocallySurjective.imageSieve_mem`, `Presheaf.isSheaf_bot`, `Coverage.mem_toGrothendieck`, `Presheaf.equalizerSieve_mem`, `coherentTopology.mem_sieves_of_hasEffectiveEpiFamily`, `GrothendieckTopology.Cover.ext_iff`, `GrothendieckTopology.mem_toPrecoverage_iff`, `AlgebraicGeometry.Scheme.grothendieckTopology_monotone`, `TopCat.Presheaf.presieveOfCovering.mem_grothendieckTopology`, `GrothendieckTopology.pullback_mem_iff_of_isIso`, `GrothendieckTopology.covering_iff_covers_id`, `GrothendieckTopology.isGLB_sInf`, `Pretopology.toGrothendieck_bot`, `AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology`, `Functor.IsCoverDense.is_cover`, `AlgebraicGeometry.Scheme.mem_smallGrothendieckTopology`, `regularTopology.mem_sieves_of_hasEffectiveEpi`, `GrothendieckTopology.Cover.Arrow.to_middle_condition`, `regularTopology.exists_effectiveEpi_iff_mem_induced`, `Precoverage.toGrothendieck_eq_sInf`, `AlgebraicGeometry.Scheme.grothendieckTopology_cover`, `GrothendieckTopology.top_covers`, `Sheaf.le_finestTopology`, `sheafBotEquivalence_counitIso`, `coherentTopology.exists_effectiveEpiFamily_iff_mem_induced`, `GrothendieckTopology.covers_iff`, `Functor.IsCoverDense.functorPullback_pushforward_covering`, `GrothendieckTopology.Cover.Arrow.from_middle_condition`, `Functor.mem_inducedTopology_sieves_iff`, `Pretopology.mem_ofGrothendieck`, `GrothendieckTopology.Subcanonical.le_canonical`, `AlgebraicGeometry.Scheme.mem_toGrothendieck_smallPretopology`, `GrothendieckTopology.mem_toCoverage_iff`, `AlgebraicGeometry.Scheme.AffineZariskiSite.mem_grothendieckTopology_iff_sectionsOfPresieve`, `Functor.IsDenseSubsite.imageSieve_mem`, `Presheaf.imageSieve_mem`, `GrothendieckTopology.Cover.coe_pullback`, `Pretopology.sInf_ofGrothendieck`, `discreteSieve_mem`, `GrothendieckTopology.covering_of_eq_top`, `GrothendieckTopology.OneHypercover.mem₁`, `AlgebraicGeometry.Scheme.Cover.mem_grothendieckTopology`, `GrothendieckTopology.top_covering`, `GrothendieckTopology.le_canonical`

TopCat

Definitions

Name	Category	Theorems
`grothendieckTopology` 📖	CompOp	1 math math: `subcanonical_grothendieckTopology`
`instHasIsosPrecoverage` 📖	CompOp	—
`instIsStableUnderBaseChangePrecoverage` 📖	CompOp	—
`instIsStableUnderCompositionPrecoverage` 📖	CompOp	—
`isOpenEmbedding` 📖	CompOp	4 math math: `isOpenEmbedding_iff`, `instRespectsIsoIsOpenEmbedding`, `instIsStableUnderBaseChangeIsOpenEmbedding`, `instIsMultiplicativeIsOpenEmbedding`
`precoverage` 📖	CompOp	3 math math: `instSmallPrecoverage`, `isOpenEmbedding_f_zeroHypercover`, `exists_mem_zeroHypercover_range`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`exists_mem_zeroHypercover_range` 📖	mathematical	—	`carrier` `Set` `Set.instMembership` `Set.range` `CategoryTheory.PreZeroHypercover.X` `TopCat` `instCategory` `CategoryTheory.Precoverage.ZeroHypercover.toPreZeroHypercover` `precoverage` `DFunLike.coe` `CategoryTheory.ConcreteCategory.hom` `ContinuousMap` `str` `ContinuousMap.instFunLike` `instConcreteCategoryContinuousMapCarrier` `CategoryTheory.PreZeroHypercover.f`	—	`CategoryTheory.Presieve.map_ofArrows` `CategoryTheory.Precoverage.ZeroHypercover.mem₀`
`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`	—	—
`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