Structures · Category theory
CategoryTheory.Presheaf.IsLocallySurjective
A morphism of presheaves f : F ⟶ G is locally surjective with respect to a Grothendieck
topology if every section of G is locally in the image of f.
- Shape
- 2 explicit arguments · adds imageSieve_mem
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances0
No instance on a concrete type; it is reached through other classes.
How is a type an instance?
Loading the hierarchy index…
Assumed by75
- CategoryTheory.Presheaf.imageSieve_mem
- PresheafOfModules.Sheafify.smul
- PresheafOfModules.sheafification
- CategoryTheory.Presheaf.IsLocallySurjective.imageSieve_mem
- PresheafOfModules.sheafify
- PresheafOfModules.Sheafify.map_smul_eq
- PresheafOfModules.sheafificationHomEquiv
- PresheafOfModules.toSheafify
- PresheafOfModules.sheafificationAdjunction
- CategoryTheory.Presheaf.isLocallySurjective_comp_iff
- PresheafOfModules.sheafifyMap
- CategoryTheory.Presheaf.comp_isLocallyInjective_iff
- CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_of_isLocallyInjective
- CategoryTheory.Presheaf.isLocallyInjective_of_isLocallyInjective_of_isLocallySurjective
- CategoryTheory.Presheaf.comp_isLocallySurjective_iff
- CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective
- CategoryTheory.Presheaf.isLocallySurjective_of_whisker
- PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def
- PresheafOfModules.sheafifyHomEquiv'
- PresheafOfModules.sheafificationCompToSheaf
- PresheafOfModules.Sheafify.smulCandidate
- PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm
- CategoryTheory.Presheaf.isLocallySurjective_of_isLocallySurjective_fac
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_surjective
- CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_map_bijective
- CategoryTheory.Presheaf.isLocallySurjective_iff_of_fac
- CategoryTheory.Presheaf.isLocallySurjective_whisker
- AlgebraicGeometry.Scheme.LocalRepresentability.representableBy
- PresheafOfModules.toSheafify_app_apply
- PresheafOfModules.instIsLocallySurjectiveToSheafify
- PresheafOfModules.instPreservesFiniteLimitsSheafAddCommGrpCatCompSheafOfModulesSheafificationToSheaf
- CategoryTheory.Presheaf.instIsLocallySurjectiveFunWhiskerRightOppositeForget
- PresheafOfModules.Sheafify.add_smul
- PresheafOfModules.sheafificationAdjunction_homEquiv_apply
- PresheafOfModules.Sheafify.smul_zero
- AlgebraicGeometry.Scheme.LocalRepresentability.yonedaIsoSheaf
- PresheafOfModules.sheafification_map
- PresheafOfModules.toSheafify_app_apply'
- PresheafOfModules.Sheafify.instUniqueSMulCandidate
- PresheafOfModules.inverseImage_W_toPresheaf_eq_inverseImage_isomorphisms
- PresheafOfModules.Sheafify.smul_add
- PresheafOfModules.sheafifyMap_val
- PresheafOfModules.Sheafify.zero_smul
- PresheafOfModules.instPreservesFiniteLimitsSheafOfModulesSheafification
- PresheafOfModules.restrictHomEquivOfIsLocallySurjective
- AlgebraicGeometry.Scheme.LocalRepresentability.instIsIsoSheafZariskiTopologyTypeYonedaGluedToSheaf
- PresheafOfModules.toSheaf_map_sheafificationAdjunction_counit_app
- CategoryTheory.Presheaf.isLocallySurjective_comp
- PresheafOfModules.Sheafify.mul_smul
- PresheafOfModules.Sheafify.module
Ancestors0
No ancestors.