Sheafification

📁 Source: Mathlib/CategoryTheory/Sites/Sheafification.lean

Statistics

Metric	Count
Definitions HasSheafify, HasWeakSheafify, instReflectiveFunctorOppositeSheafSheafToPresheafOfHasWeakSheafify, isoSheafify, presheafToSheaf, sheafification, sheafificationAdjunction, sheafificationIso, sheafificationNatIso, sheafify, sheafifyLift, sheafifyMap, toSheafification, toSheafify	14
Theorems isLeftExact, isRightAdjoint, mk', instHasWeakSheafifyOfHasSheafify, instIsIsoFunctorOppositeValAppSheafCounitSheafificationAdjunction, instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf, instPreservesFiniteLimitsFunctorOppositeSheafLeftAdjointSheafToPresheaf, instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf, instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf, isIso_sheafificationAdjunction_counit, isIso_toSheafify, isoSheafify_hom, isoSheafify_inv, sheafificationAdjunction_counit_app_val, sheafificationAdjunction_unit_app, sheafificationIso_hom_val, sheafificationIso_inv_val, sheafificationNatIso_hom_app_val, sheafificationNatIso_inv_app_val, sheafification_map, sheafification_obj, sheafification_reflective, sheafifyLift_id_toSheafify, sheafifyLift_id_toSheafify_assoc, sheafifyLift_unique, sheafifyMap_comp, sheafifyMap_id, sheafifyMap_sheafifyLift, sheafifyMap_sheafifyLift_assoc, sheafify_hom_ext, toSheafification_app, toSheafify_naturality, toSheafify_naturality_assoc, toSheafify_sheafifyLift, toSheafify_sheafifyLift_assoc	35
Total	49

CategoryTheory

Definitions

Name	Category	Theorems
HasSheafify 📖	CompData	8 math math: hasSheafifyEssentiallySmallSite, instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover, LightProfinite.hasSheafify, Equivalence.hasSheafify, HasSheafify.mk', LightCondMod.LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat, LightProfinite.hasSheafify_type, instHasSheafifyType
HasWeakSheafify 📖	MathDef	2 math math: HasSheafify.isRightAdjoint, instHasWeakSheafifyOfHasSheafify
instReflectiveFunctorOppositeSheafSheafToPresheafOfHasWeakSheafify 📖	CompOp	1 math math: instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf
isoSheafify 📖	CompOp	4 math math: sheafificationIso_inv_val, isoSheafify_hom, sheafificationIso_hom_val, isoSheafify_inv
presheafToSheaf 📖	CompOp	41 math math: isIso_sheafificationAdjunction_counit, GrothendieckTopology.MayerVietorisSquare.shortComplex_X₃, GrothendieckTopology.W_eq_inverseImage_isomorphisms, sheafificationNatIso_inv_app_val, GrothendieckTopology.MayerVietorisSquare.shortComplex_X₁, Condensed.discrete_map, instIsIsoFunctorOppositeValAppSheafCounitSheafificationAdjunction, sheafificationNatIso_hom_app_val, LightCondensed.discrete_map, Sheaf.isPullback_square_op_map_yoneda_presheafToSheaf_yoneda_iff, Presheaf.isLocallyInjective_presheafToSheaf_map_iff, GrothendieckTopology.MayerVietorisSquare.biprodAddEquiv_symm_biprodIsoProd_hom_toBiprod_apply, GrothendieckTopology.MayerVietorisSquare.isPushout, sheafificationIso_inv_val, GrothendieckTopology.W_isInvertedBy_whiskeringRight_presheafToSheaf, GrothendieckTopology.MayerVietorisSquare.mk₀_f_comp_biprodAddEquiv_symm_biprodIsoProd_hom, PresheafOfModules.sheafification_map, toPresheafToSheafCompComposeAndSheafify_app, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf, Functor.toSheafify_pullbackSheafificationCompatibility, GrothendieckTopology.MayerVietorisSquare.shortComplex_g, GrothendieckTopology.MayerVietorisSquare.isPushoutAddCommGrpFreeSheaf, sheafificationAdjunction_unit_app, presheafToSheaf_additive, sheafificationIso_hom_val, LightCondensed.discrete_obj, presheafToSheafCompComposeAndSheafifyIso_inv_app, GrothendieckTopology.instIsLocalizationFunctorOppositeSheafPresheafToSheafW, GrothendieckTopology.W_iff, GrothendieckTopology.MayerVietorisSquare.shortComplex_f, instIsIsoFunctorOppositeSheafToPresheafToSheafCompComposeAndSheafify, sheafificationAdjunction_counit_app_val, GrothendieckTopology.MayerVietorisSquare.shortComplex_X₂, sheafification_reflective, constantSheafAdj_counit_app, instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf, Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv, Condensed.discrete_obj, Presheaf.isLocallySurjective_presheafToSheaf_map_iff
sheafification 📖	CompOp	3 math math: sheafification_map, toSheafification_app, sheafification_obj
sheafificationAdjunction 📖	CompOp	8 math math: isIso_sheafificationAdjunction_counit, instIsIsoFunctorOppositeValAppSheafCounitSheafificationAdjunction, PresheafOfModules.toSheaf_map_sheafificationHomEquiv_symm, sheafificationAdjunction_unit_app, sheafificationAdjunction_counit_app_val, sheafification_reflective, constantSheafAdj_counit_app, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv
sheafificationIso 📖	CompOp	2 math math: sheafificationIso_inv_val, sheafificationIso_hom_val
sheafificationNatIso 📖	CompOp	2 math math: sheafificationNatIso_inv_app_val, sheafificationNatIso_hom_app_val
sheafify 📖	CompOp	34 math math: constantCommuteCompose_hom_app_val, GrothendieckTopology.instIsLocallyInjectiveToSheafify, toSheafify_sheafifyLift_assoc, isIso_toSheafify, sheafificationIso_inv_val, sheafComposeIso_hom_fac, Presheaf.isLocallySurjective_toSheafify', sheafifyMap_id, Presheaf.isLocallyInjective_toSheafify', sheafifyMap_sheafifyLift, sheafifyLift_id_toSheafify, toSheafify_plusPlusIsoSheafify_hom, isoSheafify_hom, GrothendieckTopology.Point.instIsIsoMapFunctorOppositePresheafFiberToSheafify, Sheaf.adjunction_unit_app_val, Functor.toSheafify_pullbackSheafificationCompatibility, sheafifyMap_comp, sheafificationIso_hom_val, sheafComposeIso_inv_fac_assoc, isoSheafify_inv, toSheafify_sheafifyLift, sheafification_obj, GrothendieckTopology.instIsLocallySurjectiveToSheafify, GrothendieckTopology.W_toSheafify, toSheafify_naturality_assoc, toSheafify_plusPlusIsoSheafify_hom_assoc, sheafComposeIso_hom_fac_assoc, sheafComposeIso_inv_fac, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, sheafifyMap_sheafifyLift_assoc, sheafifyLift_id_toSheafify_assoc, Sheaf.sheafifyCocone_ι_app_val, Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val, toSheafify_naturality
sheafifyLift 📖	CompOp	12 math math: sheafifyLift_unique, sheafificationNatIso_inv_app_val, toSheafify_sheafifyLift_assoc, sheafifyMap_sheafifyLift, sheafifyLift_id_toSheafify, Sheaf.adjunction_counit_app_val, isoSheafify_inv, toSheafify_sheafifyLift, sheafificationAdjunction_counit_app_val, sheafifyMap_sheafifyLift_assoc, sheafifyLift_id_toSheafify_assoc, Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val
sheafifyMap 📖	CompOp	8 math math: constantCommuteCompose_hom_app_val, sheafification_map, sheafifyMap_id, sheafifyMap_sheafifyLift, sheafifyMap_comp, toSheafify_naturality_assoc, sheafifyMap_sheafifyLift_assoc, toSheafify_naturality
toSheafification 📖	CompOp	1 math math: toSheafification_app
toSheafify 📖	CompOp	33 math math: sheafificationNatIso_hom_app_val, GrothendieckTopology.instIsLocallyInjectiveToSheafify, toSheafify_sheafifyLift_assoc, isIso_toSheafify, sheafComposeIso_hom_fac, Presheaf.isLocallySurjective_toSheafify', Presheaf.isLocallyInjective_toSheafify', sheafifyLift_id_toSheafify, PresheafOfModules.sheafification_map, toPresheafToSheafCompComposeAndSheafify_app, toSheafify_plusPlusIsoSheafify_hom, isoSheafify_hom, GrothendieckTopology.Point.instIsIsoMapFunctorOppositePresheafFiberToSheafify, Sheaf.adjunction_unit_app_val, toSheafification_app, Functor.toSheafify_pullbackSheafificationCompatibility, sheafificationAdjunction_unit_app, sheafComposeIso_inv_fac_assoc, presheafToSheafCompComposeAndSheafifyIso_inv_app, toSheafify_sheafifyLift, GrothendieckTopology.instIsLocallySurjectiveToSheafify, GrothendieckTopology.W_toSheafify, Sheaf.sheafifyCocone_ι_app_val_assoc, toSheafify_naturality_assoc, toSheafify_plusPlusIsoSheafify_hom_assoc, PresheafOfModules.toPresheaf_map_sheafificationAdjunction_unit_app, sheafComposeIso_hom_fac_assoc, sheafComposeIso_inv_fac, PresheafOfModules.toPresheaf_map_sheafificationHomEquiv_def, sheafifyLift_id_toSheafify_assoc, Sheaf.sheafifyCocone_ι_app_val, Functor.pushforwardContinuousSheafificationCompatibility_hom_app_val, toSheafify_naturality

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasWeakSheafifyOfHasSheafify 📖	mathematical	—	HasWeakSheafify	—	HasSheafify.isRightAdjoint
instIsIsoFunctorOppositeValAppSheafCounitSheafificationAdjunction 📖	mathematical	—	IsIso Functor Opposite Category.opposite Functor.category Sheaf.val Functor.obj Sheaf Sheaf.instCategorySheaf Functor.comp sheafToPresheaf presheafToSheaf Functor.id Sheaf.Hom.val NatTrans.app Adjunction.counit sheafificationAdjunction	—	Functor.map_isIso isIso_sheafificationAdjunction_counit
instIsLeftAdjointFunctorOppositeSheafPresheafToSheaf 📖	mathematical	—	Functor.IsLeftAdjoint Functor Opposite Category.opposite Functor.category Sheaf Sheaf.instCategorySheaf presheafToSheaf	—	—
instPreservesFiniteLimitsFunctorOppositeSheafLeftAdjointSheafToPresheaf 📖	mathematical	—	Limits.PreservesFiniteLimits Functor Opposite Category.opposite Functor.category Sheaf Sheaf.instCategorySheaf Functor.leftAdjoint sheafToPresheaf instHasWeakSheafifyOfHasSheafify	—	HasSheafify.isLeftExact
instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf 📖	mathematical	—	Limits.PreservesFiniteLimits Functor Opposite Category.opposite Functor.category Sheaf Sheaf.instCategorySheaf presheafToSheaf instHasWeakSheafifyOfHasSheafify	—	HasSheafify.isLeftExact
instPreservesFiniteLimitsFunctorOppositeSheafReflectorSheafToPresheaf 📖	mathematical	—	Limits.PreservesFiniteLimits Functor Opposite Category.opposite Functor.category Sheaf Sheaf.instCategorySheaf reflector sheafToPresheaf instReflectiveFunctorOppositeSheafSheafToPresheafOfHasWeakSheafify instHasWeakSheafifyOfHasSheafify	—	instHasWeakSheafifyOfHasSheafify instPreservesFiniteLimitsFunctorOppositeSheafPresheafToSheaf
isIso_sheafificationAdjunction_counit 📖	mathematical	—	IsIso Sheaf Sheaf.instCategorySheaf Functor.obj Functor.comp Functor Opposite Category.opposite Functor.category sheafToPresheaf presheafToSheaf Functor.id NatTrans.app Adjunction.counit sheafificationAdjunction	—	isIso_of_fully_faithful instFullSheafFunctorOppositeSheafToPresheaf instFaithfulSheafFunctorOppositeSheafToPresheaf Functor.map_isIso Adjunction.instIsIsoAppCounitOfFullOfFaithful
isIso_toSheafify 📖	mathematical	Presheaf.IsSheaf	IsIso Functor Opposite Category.opposite Functor.category sheafify toSheafify	—	Adjunction.right_triangle Functor.map_isIso Adjunction.instIsIsoAppCounitOfFullOfFaithful instFullSheafFunctorOppositeSheafToPresheaf instFaithfulSheafFunctorOppositeSheafToPresheaf Adjunction.inv_counit_map IsIso.hom_inv_id
isoSheafify_hom 📖	mathematical	Presheaf.IsSheaf	Iso.hom Functor Opposite Category.opposite Functor.category sheafify isoSheafify toSheafify	—	—
isoSheafify_inv 📖	mathematical	Presheaf.IsSheaf	Iso.inv Functor Opposite Category.opposite Functor.category sheafify isoSheafify sheafifyLift CategoryStruct.id Category.toCategoryStruct	—	sheafifyLift_unique Category.id_comp
sheafificationAdjunction_counit_app_val 📖	mathematical	—	Sheaf.Hom.val Functor.obj Sheaf Sheaf.instCategorySheaf Functor.comp Functor Opposite Category.opposite Functor.category sheafToPresheaf presheafToSheaf Functor.id NatTrans.app Adjunction.counit sheafificationAdjunction sheafifyLift Sheaf.val CategoryStruct.id Category.toCategoryStruct Sheaf.cond	—	Sheaf.cond Adjunction.homEquiv_counit Functor.map_id Category.id_comp
sheafificationAdjunction_unit_app 📖	mathematical	—	NatTrans.app Functor Opposite Category.opposite Functor.category Functor.id Functor.comp Sheaf Sheaf.instCategorySheaf presheafToSheaf sheafToPresheaf Adjunction.unit sheafificationAdjunction toSheafify	—	—
sheafificationIso_hom_val 📖	mathematical	—	Sheaf.Hom.val Functor.obj Functor Opposite Category.opposite Functor.category Sheaf Sheaf.instCategorySheaf presheafToSheaf Sheaf.val Iso.hom sheafificationIso sheafify isoSheafify Sheaf.cond	—	—
sheafificationIso_inv_val 📖	mathematical	—	Sheaf.Hom.val Functor.obj Functor Opposite Category.opposite Functor.category Sheaf Sheaf.instCategorySheaf presheafToSheaf Sheaf.val Iso.inv sheafificationIso sheafify isoSheafify Sheaf.cond	—	—
sheafificationNatIso_hom_app_val 📖	mathematical	—	Sheaf.Hom.val Functor.obj Sheaf Sheaf.instCategorySheaf Functor.id Functor.comp Functor Opposite Category.opposite Functor.category sheafToPresheaf presheafToSheaf NatTrans.app Iso.hom sheafificationNatIso toSheafify Sheaf.val	—	—
sheafificationNatIso_inv_app_val 📖	mathematical	—	Sheaf.Hom.val Functor.obj Sheaf Sheaf.instCategorySheaf Functor.comp Functor Opposite Category.opposite Functor.category sheafToPresheaf presheafToSheaf Functor.id NatTrans.app Iso.inv sheafificationNatIso sheafifyLift Sheaf.val CategoryStruct.id Category.toCategoryStruct Sheaf.cond	—	isoSheafify_inv Sheaf.cond
sheafification_map 📖	mathematical	—	Functor.map Functor Opposite Category.opposite Functor.category sheafification sheafifyMap	—	—
sheafification_obj 📖	mathematical	—	Functor.obj Functor Opposite Category.opposite Functor.category sheafification sheafify	—	—
sheafification_reflective 📖	mathematical	—	IsIso Functor Sheaf Sheaf.instCategorySheaf Functor.category Functor.comp Opposite Category.opposite sheafToPresheaf presheafToSheaf Functor.id Adjunction.counit sheafificationAdjunction	—	NatIso.isIso_of_isIso_app isIso_sheafificationAdjunction_counit
sheafifyLift_id_toSheafify 📖	mathematical	Presheaf.IsSheaf	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category sheafify sheafifyLift CategoryStruct.id toSheafify	—	cancel_mono mono_of_strongMono strongMono_of_isIso instIsIsoFunctorOppositeValAppSheafCounitSheafificationAdjunction Sheaf.cond toSheafify_naturality sheafificationAdjunction_counit_app_val Category.assoc sheafifyMap_sheafifyLift sheafifyLift.congr_simp Category.comp_id toSheafify_sheafifyLift Category.id_comp
sheafifyLift_id_toSheafify_assoc 📖	mathematical	Presheaf.IsSheaf	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category sheafify sheafifyLift CategoryStruct.id toSheafify	—	Category.assoc Category.id_comp Mathlib.Tactic.Reassoc.eq_whisker' sheafifyLift_id_toSheafify
sheafifyLift_unique 📖	mathematical	Presheaf.IsSheaf CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category sheafify toSheafify	sheafifyLift	—	sheafifyLift.eq_1 Sheaf.Hom.ext_iff Adjunction.homEquiv_apply_eq Adjunction.homEquiv_unit toSheafify.eq_1
sheafifyMap_comp 📖	mathematical	—	sheafifyMap CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category sheafify	—	Functor.map_comp
sheafifyMap_id 📖	mathematical	—	sheafifyMap CategoryStruct.id Functor Opposite Category.opposite Category.toCategoryStruct Functor.category sheafify	—	Functor.map_id
sheafifyMap_sheafifyLift 📖	mathematical	Presheaf.IsSheaf	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category sheafify sheafifyMap sheafifyLift	—	sheafifyLift_unique Category.assoc toSheafify_naturality toSheafify_sheafifyLift
sheafifyMap_sheafifyLift_assoc 📖	mathematical	Presheaf.IsSheaf	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category sheafify sheafifyMap sheafifyLift	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' sheafifyMap_sheafifyLift
sheafify_hom_ext 📖	—	Presheaf.IsSheaf CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category sheafify toSheafify	—	—	sheafifyLift_unique
toSheafification_app 📖	mathematical	—	NatTrans.app Functor Opposite Category.opposite Functor.category Functor.id sheafification toSheafification toSheafify	—	—
toSheafify_naturality 📖	mathematical	—	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category sheafify toSheafify sheafifyMap	—	NatTrans.naturality
toSheafify_naturality_assoc 📖	mathematical	—	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category sheafify toSheafify sheafifyMap	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toSheafify_naturality
toSheafify_sheafifyLift 📖	mathematical	Presheaf.IsSheaf	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category sheafify toSheafify sheafifyLift	—	toSheafify.eq_1 sheafifyLift.eq_1 Adjunction.homEquiv_counit Adjunction.unit_naturality_assoc Adjunction.right_triangle_components Category.comp_id
toSheafify_sheafifyLift_assoc 📖	mathematical	Presheaf.IsSheaf	CategoryStruct.comp Functor Opposite Category.opposite Category.toCategoryStruct Functor.category sheafify toSheafify sheafifyLift	—	Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' toSheafify_sheafifyLift

CategoryTheory.HasSheafify

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isLeftExact 📖	mathematical	—	CategoryTheory.Limits.PreservesFiniteLimits CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.leftAdjoint CategoryTheory.sheafToPresheaf isRightAdjoint	—	—
isRightAdjoint 📖	mathematical	—	CategoryTheory.HasWeakSheafify	—	—
mk' 📖	mathematical	—	CategoryTheory.HasSheafify	—	CategoryTheory.Limits.preservesLimitsOfShape_of_natIso CategoryTheory.Limits.PreservesFiniteLimits.preservesFiniteLimits

---

← Back to Index