Instances

📁 Source: Mathlib/Condensed/Light/Instances.lean

Statistics

Metric	Count
Definitions	0
Theorems hasSheafify, hasSheafify_type, instWEqualsLocallyBijectiveCoherentTopology	3
Total	3

LightProfinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasSheafify 📖	mathematical	—	CategoryTheory.HasSheafify LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology instPreregular	—	CategoryTheory.hasSheafifyEssentiallySmallSite CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology instPreregular instEssentiallySmallLightProfinite CategoryTheory.instHasSheafifyOfPreservesLimitsForgetOfHasFiniteLimitsOfSmallOppositeCover CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full CategoryTheory.Equivalence.full_inverse CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Functor.IsLocallyFaithful.of_faithful CategoryTheory.Equivalence.faithful_inverse CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasFiniteLimits_of_hasCountableLimits CategoryTheory.Limits.hasCountableLimits_of_hasLimits Opposite.small UnivLE.small UnivLE.self
hasSheafify_type 📖	mathematical	—	CategoryTheory.HasSheafify LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology instPreregular CategoryTheory.types	—	CategoryTheory.hasSheafifyEssentiallySmallSite CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology instPreregular instEssentiallySmallLightProfinite CategoryTheory.instHasSheafifyType CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full CategoryTheory.Equivalence.full_inverse CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Functor.IsLocallyFaithful.of_faithful CategoryTheory.Equivalence.faithful_inverse
instWEqualsLocallyBijectiveCoherentTopology 📖	mathematical	—	CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology instPreregular	—	CategoryTheory.GrothendieckTopology.WEqualsLocallyBijective.ofEssentiallySmall CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology instPreregular instEssentiallySmallLightProfinite CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.GrothendieckTopology.instWEqualsLocallyBijectiveOfHasWeakSheafifyOfHasSheafComposeOfPreservesSheafificationOfReflectsIsomorphismsForget CategoryTheory.Functor.locallyCoverDense_of_isCoverDense CategoryTheory.Functor.IsLocallyFull.of_full CategoryTheory.Equivalence.full_inverse CategoryTheory.Equivalence.instIsCoverDenseOfIsEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Functor.IsLocallyFaithful.of_faithful CategoryTheory.Equivalence.faithful_inverse CategoryTheory.sheafToPresheaf_isRightAdjoint CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms

---

← Back to Index