SheafEquiv

📁 Source: Mathlib/CategoryTheory/Sites/DenseSubsite/SheafEquiv.lean

Statistics

Metric	Count
Definitions sheafEquiv, sheafEquivSheafificationCompatibility	2
Theorems instIsEquivalenceSheafSheafPushforwardContinuous, instIsIsoSheafAppCounitSheafAdjunctionCocontinuous, isIso_ranCounit_app_of_isDenseSubsite, sheafEquiv_functor, sheafEquiv_inverse	5
Total	7

CategoryTheory.Functor.IsDenseSubsite

Definitions

Name	Category	Theorems
sheafEquiv 📖	CompOp	3 math math: sheafEquiv_functor, sheafEquiv_inverse, CategoryTheory.Sheaf.isConstant_iff_of_equivalence
sheafEquivSheafificationCompatibility 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instIsEquivalenceSheafSheafPushforwardContinuous 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.StructuredArrow Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.instCategoryStructuredArrow	CategoryTheory.Functor.IsEquivalence CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.sheafPushforwardContinuous instIsContinuous	—	CategoryTheory.Equivalence.isEquivalence_inverse
instIsIsoSheafAppCounitSheafAdjunctionCocontinuous 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.StructuredArrow Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.instCategoryStructuredArrow	CategoryTheory.IsIso CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor.sheafPushforwardCocontinuous instIsCocontinuous CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.StructuredArrow.proj CategoryTheory.Functor.sheafPushforwardContinuous instIsContinuous CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit CategoryTheory.Functor.sheafAdjunctionCocontinuous	—	CategoryTheory.Functor.ReflectsIsomorphisms.reflects CategoryTheory.instReflectsIsomorphismsSheafFunctorOppositeSheafToPresheaf instIsCocontinuous CategoryTheory.Limits.hasLimitOfHasLimitsOfShape instIsContinuous CategoryTheory.NatTrans.isIso_iff_isIso_app CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Yoneda.yoneda_full CategoryTheory.Yoneda.yoneda_faithful CategoryTheory.Functor.instHasRightKanExtension CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_val CategoryTheory.Functor.ranAdjunction_counit isIso_ranCounit_app_of_isDenseSubsite
isIso_ranCounit_app_of_isDenseSubsite 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.StructuredArrow Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.instCategoryStructuredArrow	CategoryTheory.IsIso CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.comp CategoryTheory.Functor.ran CategoryTheory.Functor.instHasRightKanExtension CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.StructuredArrow.proj CategoryTheory.Functor.whiskeringLeft CategoryTheory.Sheaf.val Opposite.op CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Functor.ranCounit	—	CategoryTheory.Functor.instHasRightKanExtension CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.isIso_iff_bijective CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.Presieve.IsSeparatedFor.ext CategoryTheory.Presieve.IsSheafFor.isSeparatedFor CategoryTheory.Sheaf.cond imageSieve_mem CategoryTheory.Category.assoc CategoryTheory.GrothendieckTopology.Cover.Arrow.hf equalizer_mem CategoryTheory.Functor.map_comp CategoryTheory.GrothendieckTopology.Cover.Arrow.Relation.w CategoryTheory.Category.id_comp CategoryTheory.Presheaf.IsSheaf.hom_ext CategoryTheory.Presheaf.IsSheaf.amalgamate_map CategoryTheory.Limits.IsLimit.fac CategoryTheory.Functor.map_id CategoryTheory.Category.comp_id
sheafEquiv_functor 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.StructuredArrow Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.instCategoryStructuredArrow	CategoryTheory.Equivalence.functor CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafEquiv CategoryTheory.Functor.sheafPushforwardCocontinuous instIsCocontinuous	—	—
sheafEquiv_inverse 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.StructuredArrow Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.instCategoryStructuredArrow	CategoryTheory.Equivalence.inverse CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf sheafEquiv CategoryTheory.Functor.sheafPushforwardContinuous instIsContinuous	—	—

---

← Back to Index