Documentation Verification Report

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`	9
Total	12

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`LocallyCoverDense` 📖	CompData	4 math math: `AlgebraicGeometry.Scheme.locallyCoverDense_of_le`, `locallyCoverDense_of_isCoverDense`, `AlgebraicGeometry.Scheme.instLocallyCoverDenseOverTopMorphismPropertyOverForgetOverGrothendieckTopology`, `over_forget_locallyCoverDense`
`inducedTopology` 📖	CompOp	11 math math: `CategoryTheory.coherentTopology.eq_induced`, `inducedTopology_isCocontinuous`, `inducedTopology_coverPreserving`, `CategoryTheory.Equivalence.instIsDenseSubsiteInducedTopologyInverseFunctor`, `inducedTopology_sieves`, `instIsDenseSubsiteInducedTopologyOfIsCoverDense`, `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` `DFunLike.coe` `CategoryTheory.GrothendieckTopology` `Set` `CategoryTheory.Sieve` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `obj` `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	—	`DFunLike.coe` `CategoryTheory.GrothendieckTopology` `Set` `CategoryTheory.Sieve` `CategoryTheory.GrothendieckTopology.instDFunLikeSetSieve` `obj` `CategoryTheory.Sieve.functorPushforward` `CategoryTheory.Sieve.functorPullback` `Set.instMembership`	—	`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`	—	—

---

← Back to Index