Structures · Category theory
CategoryTheory.HasSheafify
HasSheafify means that the inclusion functor from sheaves to presheaves admits a left exact
left adjoint (sheafification).
Given a functor, preserving finite limits, F : (Cᵒᵖ ⥤ A) ⥤ Sheaf J A and an adjunction
adj : F ⊣ sheafToPresheaf J A, use HasSheafify.mk' to construct a HasSheafify instance.
- Shape
- 2 explicit arguments · adds isRightAdjoint, isLeftExact
Extends0
Extends nothing: this is a root of the hierarchy.
Extended by0
Nothing extends this class yet.
Concrete types that are instances3
- AlgebraicGeometry.Scheme.AffineEtale
- AlgebraicGeometry.Scheme.Etale
- LightProfinite
How is a type an instance?
Loading the hierarchy index…
Assumed by185
- SheafOfModules.mapFreeIso
- CategoryTheory.Sheaf.H'
- CategoryTheory.Sheaf.H
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex
- CategoryTheory.Sheaf.H.map
- SheafOfModules.generatorsOfIsCokernelFree
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod
- SheafOfModules.LocalGeneratorsData.quasiCoherentData
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.toBiprod
- CategoryTheory.Sheaf.cohomologyPresheaf
- SheafOfModules.Presentation.map
- CategoryTheory.Sheaf.isLocallySurjective_iff_epi'
- SheafOfModules.Presentation.ofIsIso
- LightCondensed.discrete
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.δ
- SheafOfModules.Presentation.mapRelations
- SheafOfModules.GeneratingSections.map
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.mk'
- SheafOfModules.Presentation.mapGenerators
- CategoryTheory.Sheaf.functorH
- SheafOfModules.Presentation.quasicoherentData
- SheafOfModules.QuasicoherentData.ofIsIso
- SheafOfModules.GeneratingSections.localGeneratorsData
- SheafOfModules.mapFree
- SheafOfModules.QuasicoherentData.pushforward
- SheafOfModules.relationsOfIsCokernelFree
- SheafOfModules.ιFree_mapFree
- CategoryTheory.Sheaf.isLocallySurjective_iff_epi
- CategoryTheory.Sheaf.H.addEquiv₀_map
- SheafOfModules.Presentation.isColimit
- SheafOfModules.ιFree_mapFreeIso_hom
- SheafOfModules.map_ιFree_mapFreeIso_inv
- CategoryTheory.Sheaf.H.equiv₀
- SheafOfModules.presentationOfIsCokernelFree
- SheafOfModules.Presentation.mapRelations_mapGenerators
- Condensed.epi_iff_locallySurjective_on_compHaus
- LightCondensed.discreteUnderlyingAdj
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequence_exact
- Condensed.epi_iff_surjective_on_stonean
- CategoryTheory.hasSheafifyEssentiallySmallSite
- CategoryTheory.Equivalence.transportSheafificationAdjunction
- CategoryTheory.Equivalence.hasSheafify
- CategoryTheory.ObjectProperty.IsConservativeFamilyOfPoints.jointly_reflect_isLocallySurjective
- SheafOfModules.isQuasicoherent_pushforward_of_isLeftAdjoint
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_g
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.fromBiprod_δ
- CategoryTheory.GrothendieckTopology.MayerVietorisSquare.shortComplex_shortExact
- SheafOfModules.QuasicoherentData.bind
- SheafOfModules.isQuasicoherent_pushforward
- CategoryTheory.HasSheafify.isRightAdjoint
Ancestors0
No ancestors.