InducedTopology

📁 Source: Mathlib/CategoryTheory/Sites/DenseSubsite/InducedTopology.lean

Statistics

Metric	Count
Definitions LocallyCoverDense, inducedTopology, sheafInducedTopologyEquivOfIsCoverDense	3
Theorems functorPushforward_functorPullback_mem, inducedTopology_coverPreserving, inducedTopology_isCocontinuous, inducedTopology_sieves, instIsDenseSubsiteInducedTopologyOfIsCoverDense, locallyCoverDense_of_isCoverDense, mem_inducedTopology_sieves_iff, over_forget_locallyCoverDense, pushforward_cover_iff_cover_pullback, locallyCoverDense_of_map_functorPullback_mem, toGrothendieck_comap_eq_inducedTopology, toGrothendieck_comap_le_inducedTopology	12
Total	15

CategoryTheory.Functor

Definitions

Name	Category	Theorems
LocallyCoverDense 📖	CompData	7 math math: AlgebraicGeometry.Scheme.locallyCoverDense_of_le, CategoryTheory.Precoverage.locallyCoverDense_of_map_functorPullback_mem, AlgebraicGeometry.Scheme.ProEt.instLocallyCoverDenseOverForgetOverProetaleTopology, locallyCoverDense_of_isCoverDense, AlgebraicGeometry.Scheme.instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology, CategoryTheory.MorphismProperty.locallyCoverDense_forget_of_le, over_forget_locallyCoverDense
inducedTopology 📖	CompOp	15 math math: CategoryTheory.MorphismProperty.toGrothendieck_comap_forget_eq_inducedTopology, CategoryTheory.coherentTopology.eq_induced, inducedTopology_isCocontinuous, inducedTopology_coverPreserving, AlgebraicGeometry.Scheme.ProEt.topology_eq_inducedTopology, CategoryTheory.Equivalence.instIsDenseSubsiteInducedTopologyInverseFunctor, CategoryTheory.Precoverage.toGrothendieck_comap_eq_inducedTopology, inducedTopology_sieves, instIsDenseSubsiteInducedTopologyOfIsCoverDense, CategoryTheory.Precoverage.toGrothendieck_comap_le_inducedTopology, CategoryTheory.Equivalence.eq_inducedTopology_of_isDenseSubsite, CategoryTheory.regularTopology.eq_induced, CategoryTheory.regularTopology.exists_effectiveEpi_iff_mem_induced, CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_induced, mem_inducedTopology_sieves_iff
sheafInducedTopologyEquivOfIsCoverDense 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inducedTopology_coverPreserving 📖	mathematical	—	CategoryTheory.CoverPreserving inducedTopology	—	—
inducedTopology_isCocontinuous 📖	mathematical	—	IsCocontinuous inducedTopology	—	LocallyCoverDense.functorPushforward_functorPullback_mem
inducedTopology_sieves 📖	mathematical	—	CategoryTheory.GrothendieckTopology.sieves inducedTopology setOf CategoryTheory.Sieve obj Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.functorPushforward	—	—
instIsDenseSubsiteInducedTopologyOfIsCoverDense 📖	mathematical	—	IsDenseSubsite inducedTopology	—	—
locallyCoverDense_of_isCoverDense 📖	mathematical	—	LocallyCoverDense	—	IsCoverDense.functorPullback_pushforward_covering
mem_inducedTopology_sieves_iff 📖	mathematical	—	CategoryTheory.Sieve Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve inducedTopology obj CategoryTheory.Sieve.functorPushforward	—	—
over_forget_locallyCoverDense 📖	mathematical	—	LocallyCoverDense CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Over.forget	—	CategoryTheory.Sieve.ext CategoryTheory.Sieve.downward_closed CategoryTheory.Category.id_comp
pushforward_cover_iff_cover_pullback 📖	mathematical	—	CategoryTheory.Sieve obj Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.functorPushforward Set.Elem CategoryTheory.Sieve.functorPullback	—	GaloisCoinsertion.u_l_eq LocallyCoverDense.functorPushforward_functorPullback_mem

CategoryTheory.Functor.LocallyCoverDense

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorPushforward_functorPullback_mem 📖	mathematical	—	CategoryTheory.Sieve CategoryTheory.Functor.obj Set Set.instMembership DFunLike.coe CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve CategoryTheory.Sieve.functorPushforward CategoryTheory.Sieve.functorPullback	—	—

CategoryTheory.Precoverage

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
locallyCoverDense_of_map_functorPullback_mem 📖	mathematical	CategoryTheory.Presieve CategoryTheory.Functor.obj Set Set.instMembership coverings CategoryTheory.Presieve.map CategoryTheory.Presieve.functorPullback	CategoryTheory.Functor.LocallyCoverDense toGrothendieck	—	mem_toGrothendieck_iff_of_isStableUnderComposition le_trans CategoryTheory.Sieve.arrows_generate_map_eq_functorPushforward CategoryTheory.Sieve.le_generate CategoryTheory.Presieve.functorPushforward_monotone CategoryTheory.Presieve.functorPullback_monotone
toGrothendieck_comap_eq_inducedTopology 📖	mathematical	CategoryTheory.Presieve CategoryTheory.Functor.obj Set Set.instMembership coverings CategoryTheory.Presieve.map CategoryTheory.Presieve.functorPullback	toGrothendieck comap CategoryTheory.Functor.inducedTopology locallyCoverDense_of_map_functorPullback_mem CategoryTheory.Functor.IsLocallyFull.of_full CategoryTheory.Functor.IsLocallyFaithful.of_faithful	—	le_antisymm locallyCoverDense_of_map_functorPullback_mem CategoryTheory.Functor.IsLocallyFull.of_full CategoryTheory.Functor.IsLocallyFaithful.of_faithful toGrothendieck_comap_le_inducedTopology mem_toGrothendieck_iff_of_isStableUnderComposition CategoryTheory.Functor.mem_inducedTopology_sieves_iff CategoryTheory.GrothendieckTopology.superset_covering le_trans CategoryTheory.Sieve.generate_functorPullback_le CategoryTheory.Sieve.functorPullback_monotone CategoryTheory.Sieve.generate_mono CategoryTheory.Sieve.generate_sieve CategoryTheory.Sieve.functorPullback_functorPushforward_eq le_refl generate_mem_toGrothendieck
toGrothendieck_comap_le_inducedTopology 📖	mathematical	—	CategoryTheory.GrothendieckTopology CategoryTheory.GrothendieckTopology.instLEGrothendieckTopology toGrothendieck comap CategoryTheory.Functor.inducedTopology	—	toGrothendieck_le_iff_le_toPrecoverage CategoryTheory.GrothendieckTopology.mem_toPrecoverage_iff CategoryTheory.Functor.mem_inducedTopology_sieves_iff CategoryTheory.Sieve.generate_map_eq_functorPushforward generate_mem_toGrothendieck mem_comap_iff

---

← Back to Index