Structures · Category theory
CategoryTheory.Functor.IsContinuous
A functor F is continuous if the precomposition with F.op sends sheaves of
Type (max u₁ v₁ u₂ v₂) to sheaves. This implies that this holds for an arbitrary
universe (see Functor.op_comp_isSheaf_of_types).
- Defined in
- Mathlib.CategoryTheory.Sites.Continuous
- Shape
- 3 explicit arguments · adds op_comp_isSheaf_of_types
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances6
- CategoryTheory.Over
- AlgebraicGeometry.Scheme
- TopCat
- TopologicalSpace.Opens
- AlgebraicGeometry.Scheme.ProEt
- AlgebraicGeometry.Scheme.Opens
How is a type an instance?
Loading the hierarchy index…
Assumed by141
- CategoryTheory.Functor.sheafPushforwardContinuous
- SheafOfModules.pushforward
- SheafOfModules.pullback
- CategoryTheory.Functor.sheafPushforwardContinuousNatTrans
- CategoryTheory.Functor.isContinuous_comp
- SheafOfModules.pushforwardComp
- SheafOfModules.pushforwardCongr
- SheafOfModules.pushforwardNatTrans
- CategoryTheory.Functor.op_comp_isSheaf
- CategoryTheory.Functor.sheafAdjunctionCocontinuous
- SheafOfModules.pullbackPushforwardAdjunction
- CategoryTheory.Functor.sheafPushforwardContinuousCompSheafToPresheafIso
- SheafOfModules.pullbackObjFreeIso
- SheafOfModules.pullbackObjUnitToUnit
- SheafOfModules.pullbackComp
- CategoryTheory.Functor.op_comp_isSheaf_of_isSheaf
- CategoryTheory.Functor.op_comp_isSheaf_of_types
- SheafOfModules.unitToPushforwardObjUnit
- SheafOfModules.pushforwardSections
- CategoryTheory.Functor.pushforwardContinuousSheafificationCompatibility
- SheafOfModules.QuasicoherentData.pushforward
- CategoryTheory.CoverPreserving.of_isContinuous
- CategoryTheory.GrothendieckTopology.W_whiskerLeft_iff
- CategoryTheory.Functor.sheafPushforwardContinuousId'
- SheafOfModules.pushforwardPushforwardAdj
- CategoryTheory.GrothendieckTopology.W_inverseImage_whiskeringLeft
- CategoryTheory.Functor.sheafPullback
- CategoryTheory.GrothendieckTopology.Point.skyscraperSheafFunctorCompSheafPushforwardContinuous
- SheafOfModules.pushforwardCongr₂
- SheafOfModules.pushforwardPushforwardEquivalence
- CategoryTheory.Functor.isContinuous_of_iso
- CategoryTheory.Functor.sheafAdjunctionContinuous
- CategoryTheory.Functor.sheafPushforwardContinuousComp
- CategoryTheory.Functor.sheafPushforwardContinuousIso
- CategoryTheory.Functor.sheafAdjunctionCocontinuous_unit_app_hom
- SheafOfModules.pushforwardNatIso
- SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom
- CategoryTheory.GrothendieckTopology.Point.sheafFiberComapIso
- CategoryTheory.Functor.sheafPushforwardContinuousComp'
- CategoryTheory.Adjunction.sheafPushforwardContinuous
- CategoryTheory.Functor.toSheafify_pullbackSheafificationCompatibility
- CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_hom
- SheafOfModules.isQuasicoherent_pushforward_of_isLeftAdjoint
- SheafOfModules.pullback_map_ιFree_comp_pullbackObjFreeIso_hom_assoc
- SheafOfModules.isQuasicoherent_pushforward
- CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.transport
- CategoryTheory.Functor.W_map_of_adjunction_of_isContinuous
- SheafOfModules.pullback_assoc
- CategoryTheory.Functor.restrictedTopology_eq_inducedTopology
- SheafOfModules.pullback_comp_id
Ancestors0
No ancestors.