Structures · Category theory
CategoryTheory.Functor.LocallyCoverDense
We say that a functor C ⥤ D into a site is "locally dense" if
for each covering sieve T in D, T ∩ mor(C) generates a covering sieve in D.
- Shape
- 2 explicit arguments · adds functorPushforward_functorPullback_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- CategoryTheory.Over
- AlgebraicGeometry.Scheme.ProEt
- CategoryTheory.MorphismProperty.Over
How is a type an instance?
Loading the hierarchy index…
Assumed by11
- CategoryTheory.Functor.mem_inducedTopology_iff_of_isCoverDense
- CategoryTheory.Functor.coverPreserving_restrictedTopology
- CategoryTheory.Functor.LocallyCoverDense.functorPushforward_functorPullback_mem
- CategoryTheory.Functor.mem_restrictedTopology_iff
- CategoryTheory.Functor.sheafInducedTopologyEquivOfIsCoverDense
- CategoryTheory.Functor.pushforward_cover_iff_cover_pullback
- CategoryTheory.Functor.instIsDenseSubsiteInducedTopologyOfIsCoverDense
- CategoryTheory.Functor.instIsDenseSubsiteRestrictedTopologyOfIsCoverDense
- CategoryTheory.Functor.inducedTopology_coverPreserving
- CategoryTheory.Functor.instIsCocontinuousRestrictedTopology
- CategoryTheory.Functor.mem_inducedTopology_sieves_iff
Ancestors0
No ancestors.