Structures · Category theory
CategoryTheory.GrothendieckTopology.PreservesSheafification
A functor F : A ⥤ B preserves the sheafification for the Grothendieck
topology J on a category C if whenever a morphism of presheaves f : P₁ ⟶ P₂
in Cᵒᵖ ⥤ A is such that becomes an iso after sheafification, then it is
also the case of whiskerRight f F : P₁ ⋙ F ⟶ P₂ ⋙ F.
- Shape
- 2 explicit arguments · adds le
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 by27
- CategoryTheory.sheafifyComposeIso
- CategoryTheory.GrothendieckTopology.W_of_preservesSheafification
- CategoryTheory.constantCommuteCompose
- CategoryTheory.sheafComposeIso_hom_fac
- CategoryTheory.Sheaf.isConstant_iff_forget
- CategoryTheory.constantCommuteCompose_hom_app_hom
- CategoryTheory.presheafToSheafCompComposeAndSheafifyIso
- CategoryTheory.GrothendieckTopology.PreservesSheafification.le
- CategoryTheory.constantSheafAdj_counit_w
- CategoryTheory.sheafComposeIso_inv_fac
- CategoryTheory.sheafComposeIso_hom_fac_assoc
- CategoryTheory.Sheaf.isConstant_of_forget
- CategoryTheory.instLiftingFunctorOppositeSheafPresheafToSheafWCompObjWhiskeringRightComposeAndSheafify
- CategoryTheory.GrothendieckTopology.PreservesSheafification.transport
- CategoryTheory.Presheaf.isLocallySurjective_toSheafify'
- CategoryTheory.instIsConstantObjSheafSheafCompose
- CategoryTheory.presheafToSheafCompComposeAndSheafifyIso_inv_app
- CategoryTheory.sheafComposeIso_inv_fac_assoc
- CategoryTheory.instIsIsoFunctorOppositeSheafSheafComposeNatTrans
- CategoryTheory.GrothendieckTopology.instPreservesSheafification_1
- CategoryTheory.instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify
- CategoryTheory.Presheaf.isLocallyInjective_toSheafify'
- CategoryTheory.sheafComposeNatIso
- CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget
- CategoryTheory.constantCommuteCompose_hom_app_val
- CategoryTheory.GrothendieckTopology.W_isInvertedBy_whiskeringRight_presheafToSheaf
- CategoryTheory.sheafifyComposeIso.congr_simp
Ancestors0
No ancestors.