Module

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

Statistics

Metric	Count
Definitions LightCondAb, LightCondMod, forget, free, freeForgetAdjunction, instAbelianLightCondMod	6
Theorems hom_naturality_apply, forget_map_hom_app, forget_obj_obj_map	3
Total	9

LightCondMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_naturality_apply 📖	mathematical	—	DFunLike.coe CategoryTheory.Functor.obj Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology ModuleCat ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology ModuleCat.carrier CategoryTheory.ConcreteCategory.hom LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.NatTrans.app CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.Functor.map	—	CategoryTheory.NatTrans.naturality_apply

LightCondensed

Definitions

Name	Category	Theorems
forget 📖	CompOp	8 math math: ihomPoints_apply, LightCondMod.instPreservesEpimorphismsLightCondSetForget, forget_map_hom_app, LightCondMod.instReflectsEpimorphismsLightCondSetForget, forget_obj_obj_map, LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, ihomPoints_symm_apply, LightCondMod.isDiscrete_iff_isDiscrete_forget
free 📖	CompOp	10 math math: free_internallyProjective_iff_tensor_condition, ihomPoints_apply, ihomPoints_symm_comp, free_lightProfinite_internallyProjective_iff_tensor_condition, internallyProjective_iff_tensor_condition, free_lightProfinite_internallyProjective_iff_tensor_condition', free_internallyProjective_iff_tensor_condition', ihomPoints_symm_apply, ihom_map_val_app, internallyProjective_iff_tensor_condition'
freeForgetAdjunction 📖	CompOp	2 math math: ihomPoints_apply, ihomPoints_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
forget_map_hom_app 📖	mathematical	—	CategoryTheory.NatTrans.app Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.types CategoryTheory.Functor.obj CategoryTheory.Sheaf CategoryTheory.coherentTopology ModuleCat ModuleCat.moduleCategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.Functor.comp CategoryTheory.sheafToPresheaf CategoryTheory.Functor.whiskeringRight CategoryTheory.forget LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier CategoryTheory.InducedCategory.Hom.hom CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor.map LightCondMod instCategoryLightCondensed LightCondSet forget DFunLike.coe CategoryTheory.ConcreteCategory.hom	—	—
forget_obj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map Opposite LightProfinite CategoryTheory.Category.opposite CompHausLike.category TotallyDisconnectedSpace TopCat.carrier TopCat.str SecondCountableTopology CategoryTheory.types CategoryTheory.ObjectProperty.FullSubcategory.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Presheaf.IsSheaf CategoryTheory.coherentTopology CategoryTheory.Functor.obj LightCondMod instCategoryLightCondensed ModuleCat ModuleCat.moduleCategory LightCondSet forget DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule LinearMap.instFunLike CategoryTheory.ConcreteCategory.hom ModuleCat.instConcreteCategoryLinearMapIdCarrier	—	—

(root)

Definitions

Name	Category	Theorems
LightCondAb 📖	CompOp	—
LightCondMod 📖	CompOp	28 math math: LightCondensed.free_internallyProjective_iff_tensor_condition, LightCondensed.ihomPoints_apply, LightCondensed.ihomPoints_symm_comp, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition, LightCondMod.instPreservesEpimorphismsLightCondSetForget, LightCondMod.isDiscrete_tfae, LightCondensed.internallyProjective_iff_tensor_condition, LightCondensed.instPreservesEpimorphismsFunctorDiscreteNatLightCondModLim, LightCondensed.free_lightProfinite_internallyProjective_iff_tensor_condition', LightCondensed.forget_map_hom_app, LightCondMod.instReflectsEpimorphismsLightCondSetForget, LightCondensed.forget_obj_obj_map, LightCondensed.free_internallyProjective_iff_tensor_condition', LightCondMod.LocallyConstant.instIsIsoLightCondSetMapForgetAppLightCondensedModuleCatCounitDiscreteUnderlyingAdjObjFunctor, instHasLimitsOfSizeLightCondMod_1, LightCondMod.LocallyConstant.instFaithfulModuleCatFunctor, LightCondensed.ihomPoints_symm_apply, LightCondMod.LocallyConstant.instFullModuleCatFunctor, LightCondMod.epi_iff_locallySurjective_on_lightProfinite, LightCondensed.ihom_map_val_app, instHasFiniteLimitsLightCondMod, LightCondensed.epi_π_app_zero_of_epi, instHasLimitsOfSizeLightCondMod, LightCondensed.instCountableAB4StarLightCondMod, LightCondensed.internallyProjective_iff_tensor_condition', LightCondensed.instIsGrothendieckAbelianLightCondMod, LightCondMod.isDiscrete_iff_isDiscrete_forget, LightCondensed.instEpiLightCondModMapNat
instAbelianLightCondMod 📖	CompOp	1 math math: LightCondensed.instIsGrothendieckAbelianLightCondMod

---

← Back to Index