Commit 2023-11-24 22:08 83613d27
View on Github →refactor(CategoryTheory/Sites): continuous functors (#8408)
This PR introduces the typeclass Functor.IsContinuous
which says that the precomposition with a functor preserves the sheaf condition for Grothendieck topologies. It slightly refactors the previous main theorem about CoverPreserving
and CompatiblePreserving
functors: it now states that such functors are continuous. The pushforward functor for a continuous functor is defined under the Functor.IsContinuous
assumption rather than the combination of both CoverPreserving
and CompatiblePreserving
. The property CoverLifting
is renamed IsCocontinuous
and it is made a class. The property IsCoverDense
is also made a class.