SheafEquiv

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

Statistics

Metric	Count
Definitions	0
Theorems instIsEquivalenceSheafSheafPushforwardContinuous, instIsIsoSheafAppCounitSheafAdjunctionCocontinuous, isIso_ranCounit_app_of_isDenseSubsite	3
Total	3

CategoryTheory.Functor.IsDenseSubsite

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.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.sheafPushforwardContinuous instIsContinuous	—	CategoryTheory.Equivalence.isEquivalence_functor instIsContinuous instIsCocontinuous CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Adjunction.instIsIsoAppUnitOfFullOfFaithful full_sheafPushforwardContinuous faithful_sheafPushforwardContinuous instIsIsoSheafAppCounitSheafAdjunctionCocontinuous
instIsIsoSheafAppCounitSheafAdjunctionCocontinuous 📖	mathematical	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.StructuredArrow Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.instCategoryStructuredArrow	CategoryTheory.IsIso CategoryTheory.Sheaf CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.obj CategoryTheory.Functor.comp CategoryTheory.Functor.sheafPushforwardCocontinuous instIsCocontinuous CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.StructuredArrow CategoryTheory.Functor.op CategoryTheory.instCategoryStructuredArrow CategoryTheory.StructuredArrow.proj CategoryTheory.Functor.sheafPushforwardContinuous instIsContinuous CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit CategoryTheory.Functor.sheafAdjunctionCocontinuous	—	CategoryTheory.Functor.ReflectsIsomorphisms.reflects CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.ObjectProperty.full_ι CategoryTheory.ObjectProperty.faithful_ι instIsCocontinuous CategoryTheory.Limits.hasLimitOfHasLimitsOfShape instIsContinuous CategoryTheory.NatTrans.isIso_iff_isIso_app CategoryTheory.Yoneda.yoneda_full CategoryTheory.Yoneda.yoneda_faithful CategoryTheory.Functor.instHasRightKanExtension CategoryTheory.Functor.sheafAdjunctionCocontinuous_counit_app_hom 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 Opposite CategoryTheory.Category.opposite CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda CategoryTheory.Functor.comp CategoryTheory.Functor.ran CategoryTheory.Functor.op CategoryTheory.Functor.instHasRightKanExtension CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.StructuredArrow CategoryTheory.instCategoryStructuredArrow CategoryTheory.StructuredArrow.proj CategoryTheory.Functor.whiskeringLeft CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Presheaf.IsSheaf 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.ObjectProperty.FullSubcategory.property 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

---

← Back to Index