Cover-dense functors into precoherent categories #
We prove that if for a functor F : C ⥤ D into a precoherent category we have
F.EffectivelyEnough, then F.IsCoverDense (coherentTopology _).
We give the corresponding result for the regular topology as well.
instance
CategoryTheory.coherentTopology.instIsCoverDenseCoherentTopology
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.EffectivelyEnough F]
[CategoryTheory.Precoherent D]
:
Equations
- ⋯ = ⋯
instance
CategoryTheory.regularTopology.instIsCoverDenseRegularTopology
{C : Type u_1}
{D : Type u_2}
[CategoryTheory.Category.{u_3, u_1} C]
[CategoryTheory.Category.{u_4, u_2} D]
(F : CategoryTheory.Functor C D)
[CategoryTheory.Functor.EffectivelyEnough F]
[CategoryTheory.Preregular D]
:
Equations
- ⋯ = ⋯