Module

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

Statistics

Metric	Count
Definitions functor, functorToPresheaves, adjunction, fullyFaithfulFunctor, functor, functorIsoDiscrete, functorIsoDiscreteAux₁, functorIsoDiscreteAux₂, functorIsoDiscreteComponents, functorToPresheaves, adjunction, fullyFaithfulFunctor, functor, functorIsoDiscrete, functorIsoDiscreteAux₁, functorIsoDiscreteAux₂, functorIsoDiscreteComponents, functorToPresheaves	18
Theorems functorToPresheaves_map_app, functorToPresheaves_obj_map, functorToPresheaves_obj_obj_carrier, functorToPresheaves_obj_obj_isAddCommGroup, functorToPresheaves_obj_obj_isModule, functor_map_val, functor_obj_val, instFaithfulModuleCatCondensedDiscrete, instFaithfulModuleCatFunctor, instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, instFullModuleCatCondensedDiscrete, instFullModuleCatFunctor, instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, instFullSheafCompHausCoherentTopologyTypeConstantSheaf, instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, instFaithfulModuleCatFunctor, instFaithfulModuleCatLightCondensedDiscrete, instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf, instFullModuleCatFunctor, instFullModuleCatLightCondensedDiscrete, instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, instHasSheafifyLightProfiniteCoherentTopologyModuleCat, instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor	26
Total	44

CompHausLike.LocallyConstantModule

Definitions

Name	Category	Theorems
functor 📖	CompOp	2 math math: functor_map_val, functor_obj_val
functorToPresheaves 📖	CompOp	7 math math: functorToPresheaves_obj_obj_isModule, functorToPresheaves_map_app, functor_map_val, functor_obj_val, functorToPresheaves_obj_map, functorToPresheaves_obj_obj_carrier, functorToPresheaves_obj_obj_isAddCommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
functorToPresheaves_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite CompHausLike CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory ModuleCat.of LocallyConstant TopCat.carrier CompHausLike.toTop ModuleCat.carrier TopCat.str LocallyConstant.instAddCommGroup ModuleCat.isAddCommGroup LocallyConstant.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule ModuleCat.ofHom Opposite.unop LocallyConstant.comapₗ TopCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom TopCat TopCat.instCategory Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Functor CategoryTheory.Functor.category functorToPresheaves LocallyConstant.mapₗ ModuleCat.Hom.hom	—	—
functorToPresheaves_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite CompHausLike CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functorToPresheaves ModuleCat.ofHom LocallyConstant TopCat.carrier CompHausLike.toTop Opposite.unop ModuleCat.carrier TopCat.str LocallyConstant.instAddCommGroup ModuleCat.isAddCommGroup LocallyConstant.instModule Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isModule LocallyConstant.comapₗ TopCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom TopCat TopCat.instCategory Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	—
functorToPresheaves_obj_obj_carrier 📖	mathematical	—	ModuleCat.carrier CategoryTheory.Functor.obj Opposite CompHausLike CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor CategoryTheory.Functor.category functorToPresheaves LocallyConstant TopCat.carrier CompHausLike.toTop Opposite.unop TopCat.str	—	—
functorToPresheaves_obj_obj_isAddCommGroup 📖	mathematical	—	ModuleCat.isAddCommGroup CategoryTheory.Functor.obj Opposite CompHausLike CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor CategoryTheory.Functor.category functorToPresheaves LocallyConstant.instAddCommGroup TopCat.carrier CompHausLike.toTop Opposite.unop ModuleCat.carrier TopCat.str	—	—
functorToPresheaves_obj_obj_isModule 📖	mathematical	—	ModuleCat.isModule CategoryTheory.Functor.obj Opposite CompHausLike CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor CategoryTheory.Functor.category functorToPresheaves LocallyConstant.instModule TopCat.carrier CompHausLike.toTop Opposite.unop ModuleCat.carrier TopCat.str Ring.toSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup	—	—
functor_map_val 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	CategoryTheory.Sheaf.Hom.val CategoryTheory.coherentTopology ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category functorToPresheaves CategoryTheory.Functor.map CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.Sheaf.instCategorySheaf functor	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular
functor_obj_val 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	CategoryTheory.Sheaf.val CategoryTheory.coherentTopology ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.Sheaf.instCategorySheaf functor CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category functorToPresheaves	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular

CondensedMod.LocallyConstant

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	1 math math: CondensedMod.isDiscrete_tfae
fullyFaithfulFunctor 📖	CompOp	—
functor 📖	CompOp	4 math math: CondensedMod.isDiscrete_tfae, instFullModuleCatFunctor, instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, instFaithfulModuleCatFunctor
functorIsoDiscrete 📖	CompOp	—
functorIsoDiscreteAux₁ 📖	CompOp	—
functorIsoDiscreteAux₂ 📖	CompOp	—
functorIsoDiscreteComponents 📖	CompOp	—
functorToPresheaves 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulModuleCatCondensedDiscrete 📖	mathematical	—	CategoryTheory.Functor.Faithful ModuleCat ModuleCat.moduleCategory Condensed instCategoryCondensed Condensed.discrete 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.Functor.Faithful.of_iso 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 instFaithfulModuleCatFunctor
instFaithfulModuleCatFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful ModuleCat ModuleCat.moduleCategory CondensedMod instCategoryCondensed functor	—	CategoryTheory.Functor.FullyFaithful.faithful
instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf 📖	mathematical	—	CategoryTheory.Functor.Faithful ModuleCat ModuleCat.moduleCategory CategoryTheory.Sheaf CompHaus CompHausLike.category CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.constantSheaf CategoryTheory.sheafToPresheaf_isRightAdjoint 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_of_max 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.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 instFaithfulModuleCatCondensedDiscrete
instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.types CategoryTheory.Sheaf CompHaus CompHausLike.category CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.constantSheaf CategoryTheory.sheafToPresheaf_isRightAdjoint 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_of_max 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.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 CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete
instFullModuleCatCondensedDiscrete 📖	mathematical	—	CategoryTheory.Functor.Full ModuleCat ModuleCat.moduleCategory Condensed instCategoryCondensed Condensed.discrete 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.Functor.Full.of_iso 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 instFullModuleCatFunctor
instFullModuleCatFunctor 📖	mathematical	—	CategoryTheory.Functor.Full ModuleCat ModuleCat.moduleCategory CondensedMod instCategoryCondensed functor	—	CategoryTheory.Functor.FullyFaithful.full
instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf 📖	mathematical	—	CategoryTheory.Functor.Full ModuleCat ModuleCat.moduleCategory CategoryTheory.Sheaf CompHaus CompHausLike.category CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.constantSheaf CategoryTheory.sheafToPresheaf_isRightAdjoint 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_of_max 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.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 instFullModuleCatCondensedDiscrete
instFullSheafCompHausCoherentTopologyTypeConstantSheaf 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.types CategoryTheory.Sheaf CompHaus CompHausLike.category CategoryTheory.coherentTopology CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHaus.instHasExplicitFiniteCoproductsTrue CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHaus.instHasExplicitPullbacksTrue CompHaus.instPreregular CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.constantSheaf CategoryTheory.sheafToPresheaf_isRightAdjoint 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_of_max 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.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 CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete
instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor 📖	mathematical	—	CategoryTheory.IsIso CondensedSet instCategoryCondensed CategoryTheory.types CategoryTheory.Functor.obj CondensedMod ModuleCat ModuleCat.moduleCategory Condensed.forget Condensed CategoryTheory.Functor.comp Condensed.underlying Condensed.discrete 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.forget ModuleCat.instIsRightAdjointForgetLinearMapIdCarrier ModuleCat.hasLimit CategoryTheory.Limits.MulticospanIndex.multicospan CategoryTheory.GrothendieckTopology.Cover.index small_subtype small_Pi 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 functor CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit Condensed.discreteUnderlyingAdj	—	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.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.constantSheafAdj_counit_w CategoryTheory.IsIso.comp_isIso' CategoryTheory.NatIso.hom_app_isIso univLE_of_max CondensedSet.LocallyConstant.instFaithfulCondensedTypeDiscrete CondensedSet.LocallyConstant.instFullCondensedTypeDiscrete CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app CategoryTheory.reflectsIsomorphisms_of_full_and_faithful CategoryTheory.Types.instFullForgetTypeHom CategoryTheory.instFaithfulForget CategoryTheory.Functor.essImage_eq_of_natIso CategoryTheory.Functor.obj_mem_essImage

LightCondMod.LocallyConstant

Definitions

Name	Category	Theorems
adjunction 📖	CompOp	1 math math: LightCondMod.isDiscrete_tfae
fullyFaithfulFunctor 📖	CompOp	—
functor 📖	CompOp	4 math math: LightCondMod.isDiscrete_tfae, instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, instFaithfulModuleCatFunctor, instFullModuleCatFunctor
functorIsoDiscrete 📖	CompOp	—
functorIsoDiscreteAux₁ 📖	CompOp	—
functorIsoDiscreteAux₂ 📖	CompOp	—
functorIsoDiscreteComponents 📖	CompOp	—
functorToPresheaves 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulModuleCatFunctor 📖	mathematical	—	CategoryTheory.Functor.Faithful ModuleCat ModuleCat.moduleCategory LightCondMod instCategoryLightCondensed functor	—	CategoryTheory.Functor.FullyFaithful.faithful
instFaithfulModuleCatLightCondensedDiscrete 📖	mathematical	—	CategoryTheory.Functor.Faithful ModuleCat ModuleCat.moduleCategory LightCondensed instCategoryLightCondensed LightCondensed.discrete instHasSheafifyLightProfiniteCoherentTopologyModuleCat	—	CategoryTheory.Functor.Faithful.of_iso instHasSheafifyLightProfiniteCoherentTopologyModuleCat instFaithfulModuleCatFunctor
instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf 📖	mathematical	—	CategoryTheory.Functor.Faithful ModuleCat ModuleCat.moduleCategory CategoryTheory.Sheaf 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 CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.constantSheaf CategoryTheory.instHasWeakSheafifyOfHasSheafify instHasSheafifyLightProfiniteCoherentTopologyModuleCat	—	instHasSheafifyLightProfiniteCoherentTopologyModuleCat instFaithfulModuleCatLightCondensedDiscrete
instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf 📖	mathematical	—	CategoryTheory.Functor.Faithful CategoryTheory.types CategoryTheory.Sheaf 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 CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.constantSheaf CategoryTheory.instHasWeakSheafifyOfHasSheafify LightProfinite.hasSheafify_type	—	LightProfinite.hasSheafify_type LightCondSet.LocallyConstant.instFaithfulLightCondensedTypeDiscrete
instFullModuleCatFunctor 📖	mathematical	—	CategoryTheory.Functor.Full ModuleCat ModuleCat.moduleCategory LightCondMod instCategoryLightCondensed functor	—	CategoryTheory.Functor.FullyFaithful.full
instFullModuleCatLightCondensedDiscrete 📖	mathematical	—	CategoryTheory.Functor.Full ModuleCat ModuleCat.moduleCategory LightCondensed instCategoryLightCondensed LightCondensed.discrete instHasSheafifyLightProfiniteCoherentTopologyModuleCat	—	CategoryTheory.Functor.Full.of_iso instHasSheafifyLightProfiniteCoherentTopologyModuleCat instFullModuleCatFunctor
instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf 📖	mathematical	—	CategoryTheory.Functor.Full ModuleCat ModuleCat.moduleCategory CategoryTheory.Sheaf 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 CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.constantSheaf CategoryTheory.instHasWeakSheafifyOfHasSheafify instHasSheafifyLightProfiniteCoherentTopologyModuleCat	—	instHasSheafifyLightProfiniteCoherentTopologyModuleCat instFullModuleCatLightCondensedDiscrete
instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf 📖	mathematical	—	CategoryTheory.Functor.Full CategoryTheory.types CategoryTheory.Sheaf 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 CategoryTheory.Sheaf.instCategorySheaf CategoryTheory.constantSheaf CategoryTheory.instHasWeakSheafifyOfHasSheafify LightProfinite.hasSheafify_type	—	LightProfinite.hasSheafify_type LightCondSet.LocallyConstant.instFullLightCondensedTypeDiscrete
instHasSheafifyLightProfiniteCoherentTopologyModuleCat 📖	mathematical	—	CategoryTheory.HasSheafify 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 ModuleCat ModuleCat.moduleCategory	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular LightProfinite.hasSheafify ModuleCat.hasLimits' ModuleCat.hasColimitsOfSize AddCommGrpCat.hasColimitsOfSize UnivLE.self ModuleCat.FilteredColimits.forget_preservesFilteredColimits ModuleCat.forget_preservesLimits ModuleCat.instReflectsIsomorphismsForgetLinearMapIdCarrier
instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor 📖	mathematical	—	CategoryTheory.IsIso LightCondSet instCategoryLightCondensed CategoryTheory.types CategoryTheory.Functor.obj LightCondMod ModuleCat ModuleCat.moduleCategory LightCondensed.forget LightCondensed CategoryTheory.Functor.comp LightCondensed.underlying LightCondensed.discrete instHasSheafifyLightProfiniteCoherentTopologyModuleCat functor CategoryTheory.Functor.id CategoryTheory.Functor.map CategoryTheory.NatTrans.app CategoryTheory.Adjunction.counit LightCondensed.discreteUnderlyingAdj	—	instHasSheafifyLightProfiniteCoherentTopologyModuleCat LightProfinite.instHasPropAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CategoryTheory.instHasWeakSheafifyOfHasSheafify 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.constantSheafAdj_counit_w CategoryTheory.IsIso.comp_isIso' CategoryTheory.NatIso.hom_app_isIso CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions LightProfinite.instHasExplicitFiniteCoproductsAndTotallyDisconnectedSpaceCarrierSecondCountableTopology CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks LightProfinite.instHasExplicitPullbacksAndTotallyDisconnectedSpaceCarrierSecondCountableTopology LightProfinite.instPreregular LightCondSet.LocallyConstant.instFaithfulLightCondensedTypeDiscrete LightCondSet.LocallyConstant.instFullLightCondensedTypeDiscrete CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app CategoryTheory.Functor.essImage_eq_of_natIso CategoryTheory.Functor.obj_mem_essImage

---

← Back to Index