Structures · Category theory
CategoryTheory.Functor.IsCocontinuous
A functor G : (C, J) ⥤ (D, K) between sites is called cocontinuous (SGA 4 III 2.1)
if for all covering sieves R in D, R.pullback G is a covering sieve in C.
- Shape
- 3 explicit arguments · adds cover_lift
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances2
- CategoryTheory.Over
- AlgebraicGeometry.Scheme.Opens
How is a type an instance?
Loading the hierarchy index…
Assumed by71
- CategoryTheory.GrothendieckTopology.Point.map
- CategoryTheory.Functor.cover_lift
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap
- CategoryTheory.Functor.sheafPushforwardCocontinuous
- CategoryTheory.Functor.sheafAdjunctionCocontinuous
- CategoryTheory.GrothendieckTopology.Point.presheafFiberMapObjIso
- CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux
- CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso
- CategoryTheory.RanIsSheafOfIsCocontinuous.lift
- CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility
- SheafOfModules.QuasicoherentData.pushforward
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_presheafFiberMapObjIso_hom
- CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone
- CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map
- CategoryTheory.GrothendieckTopology.Point.map_aux
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality
- CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberMapCocone
- CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_hom
- CategoryTheory.Functor.IsCocontinuous.cover_lift
- CategoryTheory.GrothendieckTopology.Point.presheafFiberMapIso
- CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility
- CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_hom
- SheafOfModules.isQuasicoherent_pushforward_of_isLeftAdjoint
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_presheafFiberMapObjIso_inv
- CategoryTheory.isCocontinuous_comp
- SheafOfModules.isQuasicoherent_pushforward
- CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.transport
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_w
- CategoryTheory.Functor.IsCocontinuous.of_iso
- CategoryTheory.Presheaf.isLocallyInjective_whisker
- CategoryTheory.Equivalence.isDenseSubsite_functor_of_isCocontinuous
- CategoryTheory.Functor.sheafAdjunctionCocontinuous_homEquiv_apply_hom
- CategoryTheory.GrothendieckTopology.Point.presheafFiberMap_hom_ext
- CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility_hom_app_hom
- CategoryTheory.RanIsSheafOfIsCocontinuous.fac
- CategoryTheory.Presheaf.isLocallyInjective_whisker_iff
- CategoryTheory.RanIsSheafOfIsCocontinuous.isLimitMultifork
- CategoryTheory.Presheaf.isLocallySurjective_whisker
- CategoryTheory.RanIsSheafOfIsCocontinuous.fac'
- CategoryTheory.Presheaf.isLocallySurjective_whisker_iff
- CategoryTheory.RanIsSheafOfIsCocontinuous.lift.congr_simp
- CategoryTheory.Equivalence.isDenseSubsite_inverse_of_isCocontinuous
- SheafOfModules.QuasicoherentData.pushforward_I
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_naturality_assoc
- CategoryTheory.GrothendieckTopology.Point.presheafFiberMapCocone_ι_app
- CategoryTheory.Functor.sheafPushforwardCocontinuousCompSheafToPresheafIso_inv
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiberMap_w_assoc
- CategoryTheory.RanIsSheafOfIsCocontinuous.liftAux_map'
- CategoryTheory.ran_isSheaf_of_isCocontinuous
- CategoryTheory.instIsContinuousRightAdjointOfIsCocontinuous
Ancestors0
No ancestors.