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_hom_app_hom_apply_apply, functor_obj_obj_map_hom_apply_apply, functor_obj_obj_obj_carrier, functor_obj_obj_obj_isAddCommGroup_add_apply, functor_obj_obj_obj_isAddCommGroup_neg_apply, functor_obj_obj_obj_isAddCommGroup_nsmul_apply, functor_obj_obj_obj_isAddCommGroup_sub_apply, functor_obj_obj_obj_isAddCommGroup_zero_apply, functor_obj_obj_obj_isAddCommGroup_zsmul_apply, functor_obj_obj_obj_isModule_smul_apply, instFaithfulModuleCatCondensedDiscrete, instFaithfulModuleCatFunctor, instFaithfulModuleCatSheafCompHausCoherentTopologyConstantSheaf, instFaithfulSheafCompHausCoherentTopologyTypeConstantSheaf, instFullModuleCatCondensedDiscrete, instFullModuleCatFunctor, instFullModuleCatSheafCompHausCoherentTopologyConstantSheaf, instFullSheafCompHausCoherentTopologyTypeConstantSheaf, instIsIsoCondensedSetMapForgetAppCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, instFaithfulModuleCatFunctor, instFaithfulModuleCatLightCondensedDiscrete, instFaithfulModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, instFaithfulSheafLightProfiniteCoherentTopologyTypeConstantSheaf, instFullModuleCatFunctor, instFullModuleCatLightCondensedDiscrete, instFullModuleCatSheafLightProfiniteCoherentTopologyConstantSheaf, instFullSheafLightProfiniteCoherentTopologyTypeConstantSheaf, instHasSheafifyLightProfiniteCoherentTopologyModuleCat, instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor	34
Total	52

CompHausLike.LocallyConstantModule

Definitions

Name	Category	Theorems
functor 📖	CompOp	10 math math: functor_obj_obj_map_hom_apply_apply, functor_obj_obj_obj_carrier, functor_obj_obj_obj_isAddCommGroup_sub_apply, functor_obj_obj_obj_isAddCommGroup_zero_apply, functor_obj_obj_obj_isAddCommGroup_add_apply, functor_obj_obj_obj_isAddCommGroup_nsmul_apply, functor_obj_obj_obj_isAddCommGroup_neg_apply, functor_obj_obj_obj_isModule_smul_apply, functor_obj_obj_obj_isAddCommGroup_zsmul_apply, functor_map_hom_app_hom_apply_apply
functorToPresheaves 📖	CompOp	6 math math: functorToPresheaves_obj_obj_isModule, functorToPresheaves_map_app, functorToPresheaves_obj_map, functorToPresheaves_obj_obj_carrier, functorToPresheaves_obj_obj_isAddCommGroup, functor_map_hom_app_hom_apply_apply

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_hom_app_hom_apply_apply 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	DFunLike.coe LocallyConstant TopCat.carrier CompHausLike.toTop Opposite.unop CompHausLike ModuleCat.carrier TopCat.str LocallyConstant.instFunLike LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant.instAddCommMonoid AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup LocallyConstant.instModule ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom ModuleCat.of LocallyConstant.instAddCommGroup CategoryTheory.NatTrans.app Opposite CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category functorToPresheaves CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.map CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.ObjectProperty.FullSubcategory.category functor	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular
functor_obj_obj_map_hom_apply_apply 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	DFunLike.coe LocallyConstant TopCat.carrier CompHausLike.toTop Opposite.unop CompHausLike ModuleCat.carrier TopCat.str LocallyConstant.instFunLike LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring LocallyConstant.instAddCommMonoid AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup LocallyConstant.instModule ModuleCat.isModule LinearMap.instFunLike ModuleCat.Hom.hom ModuleCat.of LocallyConstant.instAddCommGroup CategoryTheory.Functor.map Opposite CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.ObjectProperty.FullSubcategory.category functor ContinuousMap ContinuousMap.instFunLike TopCat.Hom.hom CategoryTheory.InducedCategory.Hom.hom TopCat TopCat.instCategory Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular
functor_obj_obj_obj_carrier 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	ModuleCat.carrier CategoryTheory.Functor.obj Opposite CompHausLike CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.ObjectProperty.FullSubcategory.category functor LocallyConstant TopCat.carrier CompHausLike.toTop Opposite.unop TopCat.str	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular
functor_obj_obj_obj_isAddCommGroup_add_apply 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	DFunLike.coe LocallyConstant TopCat.carrier CompHausLike.toTop Opposite.unop CompHausLike ModuleCat.carrier TopCat.str LocallyConstant.instFunLike AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.ObjectProperty.FullSubcategory.category functor AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular
functor_obj_obj_obj_isAddCommGroup_neg_apply 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	DFunLike.coe LocallyConstant TopCat.carrier CompHausLike.toTop Opposite.unop CompHausLike ModuleCat.carrier TopCat.str LocallyConstant.instFunLike SubNegMonoid.toNeg AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.ObjectProperty.FullSubcategory.category functor NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular
functor_obj_obj_obj_isAddCommGroup_nsmul_apply 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	DFunLike.coe LocallyConstant TopCat.carrier CompHausLike.toTop Opposite.unop CompHausLike ModuleCat.carrier TopCat.str LocallyConstant.instFunLike AddMonoid.toNSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.ObjectProperty.FullSubcategory.category functor	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular
functor_obj_obj_obj_isAddCommGroup_sub_apply 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	DFunLike.coe LocallyConstant TopCat.carrier CompHausLike.toTop Opposite.unop CompHausLike ModuleCat.carrier TopCat.str LocallyConstant.instFunLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.ObjectProperty.FullSubcategory.category functor	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular
functor_obj_obj_obj_isAddCommGroup_zero_apply 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	DFunLike.coe LocallyConstant TopCat.carrier CompHausLike.toTop Opposite.unop CompHausLike ModuleCat.carrier TopCat.str LocallyConstant.instFunLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.ObjectProperty.FullSubcategory.category functor NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular
functor_obj_obj_obj_isAddCommGroup_zsmul_apply 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	DFunLike.coe LocallyConstant TopCat.carrier CompHausLike.toTop Opposite.unop CompHausLike ModuleCat.carrier TopCat.str LocallyConstant.instFunLike SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.ObjectProperty.FullSubcategory.category functor	—	CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular
functor_obj_obj_obj_isModule_smul_apply 📖	mathematical	DFunLike.coe CategoryTheory.ConcreteCategory.hom CompHausLike CompHausLike.category ContinuousMap TopCat.carrier CompHausLike.toTop TopCat.str ContinuousMap.instFunLike CompHausLike.concreteCategory	DFunLike.coe LocallyConstant TopCat.carrier CompHausLike.toTop Opposite.unop CompHausLike ModuleCat.carrier TopCat.str LocallyConstant.instFunLike SemigroupAction.toSMul Monoid.toSemigroup MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid LocallyConstant.instAddCommMonoid AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup Module.toDistribMulAction ModuleCat.isModule CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CompHausLike.category ModuleCat ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Sheaf CategoryTheory.instPrecoherentOfFinitaryPreExtensiveOfPreregular CategoryTheory.FinitaryExtensive.toFinitaryPreExtensive CompHausLike.instFinitaryExtensiveOfHasExplicitPullbacksOfInclusions CompHausLike.instHasExplicitPullbacksOfInclusionsOfHasExplicitPullbacks CompHausLike.preregular CategoryTheory.ObjectProperty.FullSubcategory.category functor SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	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.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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 CategoryTheory.GrothendieckTopology.Cover 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	—	—
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.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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 CategoryTheory.GrothendieckTopology.Cover Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover Opposite.small CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.instReflectsIsomorphismsForgetTypeHom	—	—
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.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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 CategoryTheory.GrothendieckTopology.Cover 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	—	—
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.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf 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 CategoryTheory.GrothendieckTopology.Cover Preorder.smallCategory CategoryTheory.GrothendieckTopology.instPreorderCover Opposite.small CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Types.instIsEquivalenceForgetTypeHom CategoryTheory.instReflectsIsomorphismsForgetTypeHom	—	—
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 instCompactSpace instIndiscreteTopologyPUnit 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 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.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.constantSheaf CategoryTheory.instHasWeakSheafifyOfHasSheafify instHasSheafifyLightProfiniteCoherentTopologyModuleCat	—	—
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.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.constantSheaf CategoryTheory.instHasWeakSheafifyOfHasSheafify LightProfinite.hasSheafify_type	—	—
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.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.constantSheaf CategoryTheory.instHasWeakSheafifyOfHasSheafify instHasSheafifyLightProfiniteCoherentTopologyModuleCat	—	—
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.ObjectProperty.FullSubcategory.category CategoryTheory.Functor Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.constantSheaf CategoryTheory.instHasWeakSheafifyOfHasSheafify LightProfinite.hasSheafify_type	—	—
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 instCompactSpace instIndiscreteTopologyPUnit 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 CategoryTheory.Sheaf.isConstant_iff_isIso_counit_app CategoryTheory.Functor.essImage_eq_of_natIso CategoryTheory.Functor.obj_mem_essImage

---

← Back to Index