Characterization

📁 Source: Mathlib/Condensed/Discrete/Characterization.lean

Statistics

Metric	Count
Definitions IsDiscrete, adjunction, adjunction, IsDiscrete	4
Theorems instHasLimitsOfSizeModuleCat, isDiscrete_iff_isDiscrete_forget, isDiscrete_tfae, isDiscrete_tfae, mem_locallyConstant_essImage_of_isColimit_mapCocone, isDiscrete_iff_isDiscrete_forget, isDiscrete_tfae, isDiscrete_tfae, mem_locallyConstant_essImage_of_isColimit_mapCocone	9
Total	13

Condensed

Definitions

Name	Category	Theorems
IsDiscrete 📖	MathDef	3 math math: CondensedMod.isDiscrete_tfae, CondensedMod.isDiscrete_iff_isDiscrete_forget, CondensedSet.isDiscrete_tfae

CondensedMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasLimitsOfSizeModuleCat 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfSize ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.Limits.hasLimitsOfSizeShrink ModuleCat.hasLimits'
isDiscrete_iff_isDiscrete_forget 📖	mathematical	—	Condensed.IsDiscrete ModuleCat ModuleCat.moduleCategory CategoryTheory.sheafToPresheaf_isRightAdjoint CompHaus CompHausLike.category CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.types CategoryTheory.forget ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier ModuleCat.hasLimit CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index small_subtype small_Pi CategoryTheory.Functor.obj CategoryTheory.Functor.comp UnivLE.small UnivLE.self Set Set.instMembership CategoryTheory.Functor.sections ModuleCat.hasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits ModuleCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf CategoryTheory.GrothendieckTopology.Cover.instInhabited ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Functor.corepresentable_preservesLimitsOfShape CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.Limits.Types.hasLimit CategoryTheory.Limits.Types.hasColimitsOfShape CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.instReflectsIsomorphismsForgetTypeHom CondensedMod instCategoryCondensed CondensedSet Condensed.forget	—	CategoryTheory.Sheaf.isConstant_iff_forget CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular CategoryTheory.sheafToPresheaf_isRightAdjoint CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier ModuleCat.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self ModuleCat.hasColimitsOfShape AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits ModuleCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier CategoryTheory.Functor.corepresentable_preservesLimitsOfShape CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.Limits.Types.hasLimit CategoryTheory.Limits.Types.hasColimitsOfShape CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.instReflectsIsomorphismsForgetTypeHom CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms ModuleCat.forget_preservesLimits CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits ModuleCat.hasLimits' CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf CategoryTheory.instReflectsIsomorphismsSheafSheafCompose Finite.compactSpace Finite.of_fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace
isDiscrete_tfae 📖	mathematical	—	List.TFAE Condensed.IsDiscrete ModuleCat ModuleCat.moduleCategory CategoryTheory.sheafToPresheaf_isRightAdjoint CompHaus CompHausLike.category CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.types CategoryTheory.forget ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier ModuleCat.hasLimit CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index small_subtype small_Pi CategoryTheory.Functor.obj CategoryTheory.Functor.comp UnivLE.small UnivLE.self Set Set.instMembership CategoryTheory.Functor.sections ModuleCat.hasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits ModuleCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder CategoryTheory.GrothendieckTopology.Cover.instSemilatticeInf CategoryTheory.GrothendieckTopology.Cover.instInhabited ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier CategoryTheory.IsIso Condensed instCategoryCondensed Condensed.underlying Condensed.discrete CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit Condensed.discreteUnderlyingAdj CategoryTheory.Functor.essImage CondensedMod LocallyConstant.functor LocallyConstant.adjunction CategoryTheory.Sheaf.IsConstant Profinite TotallyDisconnectedSpace TopCat.carrier TopCat.str Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier Profinite.instPreregular CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Equivalence.inverse Condensed.ProfiniteCompHaus.equivalence CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits CategoryTheory.StructuredArrow CategoryTheory.Functor.op profiniteToCompHaus CategoryTheory.instCategoryStructuredArrow instHasLimitsOfSizeModuleCat	—	CategoryTheory.sheafToPresheaf_isRightAdjoint CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier ModuleCat.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self ModuleCat.hasColimitsOfShape AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits ModuleCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app LocallyConstant.instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf LocallyConstant.instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf CategoryTheory.Sheaf.isConstant_iff_mem_essImage Finite.compactSpace Finite.of_fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace LocallyConstant.instFaithfulModuleCatFunctor LocallyConstant.instFullModuleCatFunctor CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app' Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier Profinite.instPreregular CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits instHasLimitsOfSizeModuleCat CategoryTheory.coherentTopology.instIsDenseSubsite CategoryTheory.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis CompHausLike.instPreservesFiniteCoproductsToCompHausLike Profinite.instPreservesEffectiveEpisCompHausProfiniteToCompHaus CategoryTheory.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis Profinite.instReflectsEffectiveEpisCompHausProfiniteToCompHaus CompHausLike.instFullToCompHausLike CompHausLike.instFaithfulToCompHausLike Profinite.instEffectivelyEnoughCompHausProfiniteToCompHaus CategoryTheory.Sheaf.isConstant_iff_of_equivalence TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit CategoryTheory.Functor.corepresentable_preservesLimitsOfShape CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.Limits.Types.hasLimit CategoryTheory.Limits.Types.hasColimitsOfShape CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.instReflectsIsomorphismsForgetTypeHom isDiscrete_iff_isDiscrete_forget List.TFAE.out CategoryTheory.Limits.Types.hasLimitsOfShape CondensedSet.isDiscrete_tfae CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.preservesFilteredColimitsOfSize_shrink CategoryTheory.Limits.reflectsColimit_of_reflectsColimitsOfShape CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.reflects_filtered_colimits CategoryTheory.Limits.reflectsFilteredColimitsOfSize_shrink ModuleCat.FilteredColimits.forget_reflectsFilteredColimits List.tfae_of_cycle

CondensedSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDiscrete_tfae 📖	mathematical	—	List.TFAE Condensed.IsDiscrete CategoryTheory.types CategoryTheory.sheafToPresheaf_isRightAdjoint CompHaus CompHausLike.category CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Types.instFunLike CategoryTheory.Types.instConcreteCategory CategoryTheory.Functor.corepresentable_preservesLimitsOfShape CategoryTheory.forget CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.Limits.WalkingMulticospan CategoryTheory.GrothendieckTopology.Cover.shape CategoryTheory.Limits.WalkingMulticospan.instSmallCategory CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index CategoryTheory.Limits.Types.hasColimitsOfShape Opposite CategoryTheory.GrothendieckTopology.Cover CategoryTheory.Category.opposite Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover Opposite.small CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.instReflectsIsomorphismsForgetTypeHom CategoryTheory.IsIso Condensed instCategoryCondensed CategoryTheory.Functor.obj CategoryTheory.Functor.comp Condensed.underlying Condensed.discrete CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit Condensed.discreteUnderlyingAdj CategoryTheory.Functor.essImage CondensedSet LocallyConstant.functor LocallyConstant.adjunction CategoryTheory.Sheaf.IsConstant Profinite TotallyDisconnectedSpace TopCat.carrier TopCat.str Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier Profinite.instPreregular CategoryTheory.Sheaf CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.Equivalence.inverse Condensed.ProfiniteCompHaus.equivalence CategoryTheory.Limits.Types.hasLimitsOfShape CategoryTheory.StructuredArrow CategoryTheory.Functor.op profiniteToCompHaus CategoryTheory.instCategoryStructuredArrow	—	CategoryTheory.sheafToPresheaf_isRightAdjoint CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular CategoryTheory.Functor.corepresentable_preservesLimitsOfShape CategoryTheory.Types.instIsCorepresentableForgetTypeHom CategoryTheory.Limits.Types.hasLimit UnivLE.small UnivLE.self CategoryTheory.Limits.Types.hasColimitsOfShape Opposite.small CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.instReflectsIsomorphismsForgetTypeHom CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app CondensedMod.LocallyConstant.instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf CondensedMod.LocallyConstant.instFullSheafCompHausCoherentTopologyTypeConstantSheaf CategoryTheory.Sheaf.isConstant_iff_mem_essImage Finite.compactSpace Finite.of_fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace LocallyConstant.instFaithfulFunctor LocallyConstant.instFullFunctor CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app' Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier Profinite.instPreregular CategoryTheory.Limits.Types.hasLimitsOfShape CategoryTheory.coherentTopology.instIsDenseSubsite CategoryTheory.instPreservesFiniteEffectiveEpiFamiliesOfPreservesEffectiveEpis CompHausLike.instPreservesFiniteCoproductsToCompHausLike Profinite.instPreservesEffectiveEpisCompHausProfiniteToCompHaus CategoryTheory.instReflectsFiniteEffectiveEpiFamiliesOfReflectsEffectiveEpis Profinite.instReflectsEffectiveEpisCompHausProfiniteToCompHaus CompHausLike.instFullToCompHausLike CompHausLike.instFaithfulToCompHausLike Profinite.instEffectivelyEnoughCompHausProfiniteToCompHaus CategoryTheory.Sheaf.isConstant_iff_of_equivalence TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit mem_locallyConstant_essImage_of_isColimit_mapCocone List.tfae_of_cycle
mem_locallyConstant_essImage_of_isColimit_mapCocone 📖	mathematical	—	CategoryTheory.Functor.essImage CondensedSet CategoryTheory.types instCategoryCondensed LocallyConstant.functor	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions Profinite.instHasExplicitFiniteCoproductsTotallyDisconnectedSpaceCarrier CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks Profinite.instHasExplicitPullbacksTotallyDisconnectedSpaceCarrier Profinite.instPreregular CategoryTheory.Limits.Types.hasLimitsOfShape UnivLE.small univLE_of_max UnivLE.self CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeVal CategoryTheory.Equivalence.full_functor CategoryTheory.Equivalence.faithful_functor CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf

CondensedSet.LocallyConstant

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	1 math math: CondensedSet.isDiscrete_tfae

LightCondMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDiscrete_iff_isDiscrete_forget 📖	mathematical	—	LightCondensed.IsDiscrete ModuleCat ModuleCat.moduleCategory CategoryTheory.instHasWeakSheafifyOfHasSheafify LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat CategoryTheory.types LightProfinite.hasSheafify_type CategoryTheory.Functor.obj LightCondMod instCategoryLightCondensed LightCondSet LightCondensed.forget	—	CategoryTheory.Sheaf.isConstant_iff_forget CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular CategoryTheory.instHasWeakSheafifyOfHasSheafify LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat LightProfinite.hasSheafify_type CategoryTheory.GrothendieckTopology.instPreservesSheafification_1 instEssentiallySmallLightProfinite CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits ModuleCat.hasLimits' CategoryTheory.Limits.Types.hasLimitsOfShape UnivLE.small UnivLE.self CategoryTheory.GrothendieckTopology.instPreservesSheafificationForgetOfPreservesLimitsOfHasColimitsOfShapeOfPreservesColimitsOfShapeOppositeCoverOfHasLimitsOfShapeWalkingMulticospanOfReflectsIsomorphisms 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 ModuleCat.forget_preservesLimits ModuleCat.hasColimitsOfShape AddCommGrpCat.hasColimitsOfShape Opposite.small CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits ModuleCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_op_of_isCofiltered CategoryTheory.isCofiltered_of_directed_ge_nonempty SemilatticeInf.instIsCodirectedOrder ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier CategoryTheory.hasSheafCompose_of_preservesMulticospan CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf CategoryTheory.instReflectsIsomorphismsSheafSheafCompose Finite.compactSpace Finite.of_fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace
isDiscrete_tfae 📖	mathematical	—	List.TFAE LightCondensed.IsDiscrete ModuleCat ModuleCat.moduleCategory CategoryTheory.instHasWeakSheafifyOfHasSheafify LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat CategoryTheory.IsIso LightCondensed instCategoryLightCondensed CategoryTheory.Functor.obj CategoryTheory.Functor.comp LightCondensed.underlying LightCondensed.discrete CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit LightCondensed.discreteUnderlyingAdj CategoryTheory.Functor.essImage LightCondMod LocallyConstant.functor LocallyConstant.adjunction	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular LocallyConstant.instHasSheafifyLightProfiniteCoherentTopologyModuleCat CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app LocallyConstant.instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf LocallyConstant.instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CategoryTheory.Sheaf.isConstant_iff_mem_essImage Finite.compactSpace Finite.of_fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace LocallyConstant.instFaithfulModuleCatFunctor LocallyConstant.instFullModuleCatFunctor CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app' LightProfinite.hasSheafify_type isDiscrete_iff_isDiscrete_forget List.TFAE.out LightCondSet.isDiscrete_tfae CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesFilteredColimitsOfSize.preserves_filtered_colimits CategoryTheory.Limits.preservesFilteredColimitsOfSize_shrink ModuleCat.FilteredColimits.forget_preservesFilteredColimits CategoryTheory.isFiltered_of_directed_le_nonempty instIsDirectedOrder IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing instArchimedeanNat CategoryTheory.Limits.reflectsColimit_of_reflectsColimitsOfShape CategoryTheory.Limits.ReflectsFilteredColimitsOfSize.reflects_filtered_colimits CategoryTheory.Limits.reflectsFilteredColimitsOfSize_shrink ModuleCat.FilteredColimits.forget_reflectsFilteredColimits List.tfae_of_cycle

LightCondSet

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isDiscrete_tfae 📖	mathematical	—	List.TFAE LightCondensed.IsDiscrete CategoryTheory.types CategoryTheory.instHasWeakSheafifyOfHasSheafify LightProfinite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular LightProfinite.hasSheafify_type CategoryTheory.IsIso LightCondensed instCategoryLightCondensed CategoryTheory.Functor.obj CategoryTheory.Functor.comp LightCondensed.underlying LightCondensed.discrete CategoryTheory.Functor.id CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit LightCondensed.discreteUnderlyingAdj CategoryTheory.Functor.essImage LightCondSet LocallyConstant.functor LocallyConstant.adjunction	—	CategoryTheory.instHasWeakSheafifyOfHasSheafify CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular LightProfinite.hasSheafify_type CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app LightCondMod.LocallyConstant.instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf LightCondMod.LocallyConstant.instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CategoryTheory.Sheaf.isConstant_iff_mem_essImage Finite.compactSpace Finite.of_fintype TopologicalSpace.t2Space_of_metrizableSpace EMetricSpace.metrizableSpace TotallySeparatedSpace.totallyDisconnectedSpace TotallySeparatedSpace.of_discrete instDiscreteTopologyPUnit TopologicalSpace.instSecondCountableTopologyOfLindelofSpaceOfPseudoMetrizableSpace Countable.LindelofSpace instCountablePUnit PseudoEMetricSpace.pseudoMetrizableSpace LocallyConstant.instFaithfulFunctor LocallyConstant.instFullFunctor CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app' mem_locallyConstant_essImage_of_isColimit_mapCocone List.tfae_of_cycle
mem_locallyConstant_essImage_of_isColimit_mapCocone 📖	mathematical	—	CategoryTheory.Functor.essImage LightCondSet CategoryTheory.types instCategoryLightCondensed LocallyConstant.functor	—	CategoryTheory.Presheaf.instPreservesFiniteProductsOppositeVal LightProfinite.instPreregular CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CategoryTheory.instFullSheafFunctorOppositeSheafToPresheaf CategoryTheory.instFaithfulSheafFunctorOppositeSheafToPresheaf

LightCondSet.LocallyConstant

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	1 math math: LightCondSet.isDiscrete_tfae

LightCondensed

Definitions

Name	Category	Theorems
IsDiscrete 📖	MathDef	3 math math: LightCondMod.isDiscrete_tfae, LightCondSet.isDiscrete_tfae, LightCondMod.isDiscrete_iff_isDiscrete_forget

---

← Back to Index