Commit 2025-05-17 13:59 dc98d77f

View on Github →

feat(Algebra/Category): the category of topological modules (#23490)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean

added def CategoryTheory.Iso.toContinuousLinearEquiv

added def TopModuleCat.Hom.Simps.hom

added structure TopModuleCat.Hom

added theorem TopModuleCat.coe_freeObj

added theorem TopModuleCat.coe_of

added def TopModuleCat.coinduced

added theorem TopModuleCat.forget₂_TopCat_obj

added def TopModuleCat.free

added def TopModuleCat.freeAdj

added def TopModuleCat.freeMap

added theorem TopModuleCat.freeMap_map

added def TopModuleCat.freeObj

added def TopModuleCat.fromInduced

added theorem TopModuleCat.hom_add

added theorem TopModuleCat.hom_comp

added theorem TopModuleCat.hom_forget₂_TopCat_map

added theorem TopModuleCat.hom_id

added theorem TopModuleCat.hom_neg

added theorem TopModuleCat.hom_nsmul

added theorem TopModuleCat.hom_ofHom

added theorem TopModuleCat.hom_smul

added theorem TopModuleCat.hom_sub

added theorem TopModuleCat.hom_zero

added theorem TopModuleCat.hom_zero_apply

added theorem TopModuleCat.hom_zsmul

added def TopModuleCat.indiscrete

added def TopModuleCat.indiscreteAdj

added def TopModuleCat.induced

added def TopModuleCat.isColimit

added def TopModuleCat.isLimit

added def TopModuleCat.ofCocone

added def TopModuleCat.ofCone

added theorem TopModuleCat.ofHom_hom

added def TopModuleCat.ofIso

added def TopModuleCat.toCoinduced

added def TopModuleCat.withModuleTopology

added def TopModuleCat.withModuleTopologyAdj

added structure TopModuleCat

Modified Mathlib/Topology/Algebra/Module/ModuleTopology.lean

Created MathlibTest/CategoryTheory/ConcreteCategory/TopModuleCat.lean