Structures · Category theory
CategoryTheory.Functor.EffectivelyEnough
D has effectively enough objects with respect to the functor F if every object has an
effective presentation.
- Shape
- One type argument · adds presentation
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- Profinite
- Stonean
How is a type an instance?
Loading the hierarchy index…
Assumed by19
- CategoryTheory.Functor.EffectivelyEnough.presentation
- CategoryTheory.Functor.effectiveEpiOver
- CategoryTheory.Functor.reflects_preregular
- CategoryTheory.Functor.reflects_precoherent
- CategoryTheory.regularTopology.exists_effectiveEpi_iff_mem_induced
- CategoryTheory.coherentTopology.exists_effectiveEpiFamily_iff_mem_induced
- CategoryTheory.Functor.effectiveEpiOverObj
- CategoryTheory.coherentTopology.eq_induced
- CategoryTheory.coherentTopology.instIsDenseSubsite
- CategoryTheory.regularTopology.coverPreserving
- CategoryTheory.coherentTopology.equivalence'
- CategoryTheory.Functor.instEffectiveEpiEffectiveEpiOver
- CategoryTheory.regularTopology.eq_induced
- CategoryTheory.coherentTopology.instIsCoverDense
- CategoryTheory.coherentTopology.coverPreserving
- CategoryTheory.coherentTopology.equivalence
- CategoryTheory.regularTopology.equivalence
- CategoryTheory.regularTopology.instIsCoverDense
- CategoryTheory.regularTopology.instIsDenseSubsite
Ancestors0
No ancestors.