Basic

📁 Source: Mathlib/Algebra/Category/ModuleCat/Topology/Basic.lean

Statistics

Metric	Count
Definitions toContinuousLinearEquiv, hom, hom, hom', coinduced, free, freeAdj, freeMap, freeObj, fromInduced, indiscrete, indiscreteAdj, induced, instAddCommGroupHom, instCategory, instCoeSortType, instConcreteCategoryContinuousLinearMapIdCarrier, instHasForget₂ContinuousLinearMapIdCarrierModuleCatLinearMap, instHasForget₂ContinuousLinearMapIdCarrierTopCatContinuousMapCarrier, instLinear, instModuleHom, instPreadditive, instTopologicalSpaceCarrier, isColimit, isLimit, of, ofCocone, ofCone, ofHom, ofIso, toCoinduced, toModuleCat, topologicalSpace, withModuleTopology, withModuleTopologyAdj	35
Theorems coe_freeObj, coe_of, continuousSMul, forget₂_TopCat_obj, freeMap_map, free_map, free_obj, hasLimit_of_hasLimit_forget₂, hom_add, hom_comp, hom_forget₂_TopCat_map, hom_id, hom_neg, hom_nsmul, hom_ofHom, hom_smul, hom_sub, hom_zero, hom_zero_apply, hom_zsmul, instHasColimitOfModuleCatCompForget₂ContinuousLinearMapIdCarrierLinearMap, instHasColimits, instHasColimitsOfShapeOfModuleCat, instHasLimits, instHasLimitsOfShapeOfModuleCat, instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, instIsLeftAdjointModuleCatWithModuleTopology, instIsLeftAdjointTopCatFree, instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, instIsRightAdjointModuleCatIndiscrete, instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, instIsTopologicalAddGroupCarrier, instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget, instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap, instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, isTopologicalAddGroup, ofHom_hom	38
Total	73

CategoryTheory.Iso

Definitions

Name	Category	Theorems
toContinuousLinearEquiv 📖	CompOp	—

TopModuleCat

Definitions

Name	Category	Theorems
coinduced 📖	CompOp	—
free 📖	CompOp	3 math math: free_map, instIsLeftAdjointTopCatFree, free_obj
freeAdj 📖	CompOp	—
freeMap 📖	CompOp	2 math math: free_map, freeMap_map
freeObj 📖	CompOp	3 math math: coe_freeObj, freeMap_map, free_obj
fromInduced 📖	CompOp	—
indiscrete 📖	CompOp	1 math math: instIsRightAdjointModuleCatIndiscrete
indiscreteAdj 📖	CompOp	—
induced 📖	CompOp	—
instAddCommGroupHom 📖	CompOp	6 math math: hom_add, hom_zsmul, hom_sub, hom_nsmul, hom_smul, hom_neg
instCategory 📖	CompOp	52 math math: hom_zero, ContinuousCohomology.I_obj_V_isAddCommGroup, instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget, ContinuousCohomology.I_obj_V_carrier, hom_zero_apply, free_map, hasLimit_of_hasLimit_forget₂, instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, ContinuousCohomology.I_obj_ρ_apply, ContinuousCohomology.instLinearActionTopModuleCatInvariants, ContinuousCohomology.Iobj_ρ_apply, ContinuousCohomology.I_obj_V_isModule, hom_add, instHasColimits, instIsRightAdjointModuleCatIndiscrete, instIsLeftAdjointModuleCatWithModuleTopology, hom_zsmul, ContinuousCohomology.instAdditiveActionTopModuleCatInvariants, ContinuousCohomology.MultiInd.d_comp_d_assoc, instIsLeftAdjointTopCatFree, hom_id, comp_cokerπ, ContinuousCohomology.I_map_hom, freeMap_map, instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap, instCategoryWithHomology, hom_sub, forget₂_TopCat_obj, hom_nsmul, instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, hom_smul, free_obj, ContinuousCohomology.instLinearActionTopModuleCatI, instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, kerι_apply, ContinuousCohomology.I_obj_V_topologicalSpace, instEpiCokerπ, instHasColimitsOfShapeOfModuleCat, ContinuousCohomology.MultiInd.d_comp_d, instHasLimitsOfShapeOfModuleCat, instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, instHasColimitOfModuleCatCompForget₂ContinuousLinearMapIdCarrierLinearMap, instMonoKerι, hom_comp, instHasLimits, ContinuousCohomology.MultiInd.d_succ, kerι_comp, hom_neg, ContinuousCohomology.const_app_hom, hom_forget₂_TopCat_map, ContinuousCohomology.instAdditiveActionTopModuleCatI
instCoeSortType 📖	CompOp	—
instConcreteCategoryContinuousLinearMapIdCarrier 📖	CompOp	12 math math: instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget, instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, hom_id, freeMap_map, instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap, forget₂_TopCat_obj, instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, kerι_apply, instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, hom_forget₂_TopCat_map
instHasForget₂ContinuousLinearMapIdCarrierModuleCatLinearMap 📖	CompOp	2 math math: instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap
instHasForget₂ContinuousLinearMapIdCarrierTopCatContinuousMapCarrier 📖	CompOp	7 math math: instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget, instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap, forget₂_TopCat_obj, instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, hom_forget₂_TopCat_map
instLinear 📖	CompOp	2 math math: ContinuousCohomology.instLinearActionTopModuleCatInvariants, ContinuousCohomology.instLinearActionTopModuleCatI
instModuleHom 📖	CompOp	1 math math: hom_smul
instPreadditive 📖	CompOp	12 math math: hom_zero, hom_zero_apply, ContinuousCohomology.instLinearActionTopModuleCatInvariants, ContinuousCohomology.instAdditiveActionTopModuleCatInvariants, ContinuousCohomology.MultiInd.d_comp_d_assoc, comp_cokerπ, instCategoryWithHomology, ContinuousCohomology.instLinearActionTopModuleCatI, ContinuousCohomology.MultiInd.d_comp_d, ContinuousCohomology.MultiInd.d_succ, kerι_comp, ContinuousCohomology.instAdditiveActionTopModuleCatI
instTopologicalSpaceCarrier 📖	CompOp	9 math math: ContinuousCohomology.I_obj_V_isAddCommGroup, ContinuousCohomology.I_obj_V_carrier, ContinuousCohomology.I_obj_ρ_apply, ContinuousCohomology.Iobj_ρ_apply, ContinuousCohomology.I_obj_V_isModule, ContinuousCohomology.I_map_hom, instIsTopologicalAddGroupCarrier, ContinuousCohomology.I_obj_V_topologicalSpace, ContinuousCohomology.const_app_hom
isColimit 📖	CompOp	—
isLimit 📖	CompOp	—
of 📖	CompOp	3 math math: ContinuousCohomology.I_obj_ρ_apply, coe_of, hom_ofHom
ofCocone 📖	CompOp	—
ofCone 📖	CompOp	—
ofHom 📖	CompOp	5 math math: ContinuousCohomology.I_obj_ρ_apply, ofHom_hom, ContinuousCohomology.I_map_hom, hom_ofHom, ContinuousCohomology.const_app_hom
ofIso 📖	CompOp	—
toCoinduced 📖	CompOp	—
toModuleCat 📖	CompOp	37 math math: hom_cokerπ, hom_zero, ContinuousCohomology.I_obj_V_isAddCommGroup, instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget, ContinuousCohomology.I_obj_V_carrier, hom_zero_apply, instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, coe_freeObj, continuousSMul, ContinuousCohomology.I_obj_ρ_apply, coe_of, ofHom_hom, ContinuousCohomology.Iobj_ρ_apply, ContinuousCohomology.I_obj_V_isModule, hom_add, hom_zsmul, hom_id, ContinuousCohomology.I_map_hom, freeMap_map, instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap, isTopologicalAddGroup, hom_sub, forget₂_TopCat_obj, hom_nsmul, instIsTopologicalAddGroupCarrier, instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, cokerπ_surjective, hom_smul, instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, kerι_apply, ContinuousCohomology.I_obj_V_topologicalSpace, instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, hom_comp, hom_neg, ContinuousCohomology.const_app_hom, hom_forget₂_TopCat_map
topologicalSpace 📖	CompOp	30 math math: hom_cokerπ, hom_zero, instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget, hom_zero_apply, instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, continuousSMul, ContinuousCohomology.I_obj_ρ_apply, ofHom_hom, ContinuousCohomology.Iobj_ρ_apply, hom_add, hom_zsmul, hom_id, freeMap_map, instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap, isTopologicalAddGroup, hom_sub, forget₂_TopCat_obj, hom_nsmul, instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap, cokerπ_surjective, hom_smul, instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, kerι_apply, ContinuousCohomology.I_obj_V_topologicalSpace, instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier, hom_comp, hom_neg, ContinuousCohomology.const_app_hom, hom_forget₂_TopCat_map
withModuleTopology 📖	CompOp	1 math math: instIsLeftAdjointModuleCatWithModuleTopology
withModuleTopologyAdj 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_freeObj 📖	mathematical	—	ModuleCat.carrier toModuleCat freeObj Finsupp TopCat.carrier MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—
coe_of 📖	mathematical	—	ModuleCat.carrier toModuleCat of	—	—
continuousSMul 📖	mathematical	—	ContinuousSMul ModuleCat.carrier toModuleCat SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup ModuleCat.isAddCommGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid ModuleCat.isModule topologicalSpace	—	—
forget₂_TopCat_obj 📖	mathematical	—	TopCat.carrier CategoryTheory.Functor.obj TopModuleCat instCategory TopCat TopCat.instCategory CategoryTheory.forget₂ ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike instConcreteCategoryContinuousLinearMapIdCarrier ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier instHasForget₂ContinuousLinearMapIdCarrierTopCatContinuousMapCarrier	—	—
freeMap_map 📖	mathematical	—	DFunLike.coe freeObj CategoryTheory.ConcreteCategory.hom TopModuleCat instCategory ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike instConcreteCategoryContinuousLinearMapIdCarrier freeMap Finsupp.mapDomain TopCat.carrier NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ContinuousMap TopCat.str ContinuousMap.instFunLike TopCat.Hom.hom	—	—
free_map 📖	mathematical	—	CategoryTheory.Functor.map TopCat TopCat.instCategory TopModuleCat instCategory free freeMap	—	—
free_obj 📖	mathematical	—	CategoryTheory.Functor.obj TopCat TopCat.instCategory TopModuleCat instCategory free freeObj	—	—
hasLimit_of_hasLimit_forget₂ 📖	mathematical	—	CategoryTheory.Limits.HasLimit TopModuleCat instCategory	—	—
hom_add 📖	mathematical	—	Hom.hom Quiver.Hom TopModuleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid instAddCommGroupHom ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.add IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup isTopologicalAddGroup	—	—
hom_comp 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp TopModuleCat CategoryTheory.Category.toCategoryStruct instCategory ContinuousLinearMap.comp Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule RingHomCompTriple.ids	—	—
hom_forget₂_TopCat_map 📖	mathematical	—	TopCat.Hom.hom CategoryTheory.Functor.obj TopModuleCat instCategory TopCat TopCat.instCategory CategoryTheory.forget₂ ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike instConcreteCategoryContinuousLinearMapIdCarrier ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier instHasForget₂ContinuousLinearMapIdCarrierTopCatContinuousMapCarrier CategoryTheory.Functor.map toContinuousMap ContinuousSemilinearMapClass.toContinuousMapClass ContinuousLinearMap.continuousSemilinearMapClass Hom.hom	—	—
hom_id 📖	mathematical	—	CategoryTheory.ConcreteCategory.hom TopModuleCat instCategory ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike instConcreteCategoryContinuousLinearMapIdCarrier CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct ContinuousLinearMap.id	—	—
hom_neg 📖	mathematical	—	Hom.hom Quiver.Hom TopModuleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid instAddCommGroupHom ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.neg isTopologicalAddGroup	—	—
hom_nsmul 📖	mathematical	—	Hom.hom Quiver.Hom TopModuleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory AddMonoid.toNatSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupHom ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.addCommGroup isTopologicalAddGroup	—	—
hom_ofHom 📖	mathematical	—	Hom.hom of ofHom	—	—
hom_smul 📖	mathematical	—	Hom.hom CommRing.toRing Quiver.Hom TopModuleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupHom DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction AddCommGroup.toAddCommMonoid instModuleHom ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.instSMul AddCommMonoid.toAddMonoid smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid ContinuousSMul.continuousConstSMul continuousSMul	—	—
hom_sub 📖	mathematical	—	Hom.hom Quiver.Hom TopModuleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupHom ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.sub isTopologicalAddGroup	—	—
hom_zero 📖	mathematical	—	Hom.hom Quiver.Hom TopModuleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.zero	—	—
hom_zero_apply 📖	mathematical	—	DFunLike.coe ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike Hom.hom Quiver.Hom TopModuleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms instPreadditive NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
hom_zsmul 📖	mathematical	—	Hom.hom Quiver.Hom TopModuleCat CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct instCategory SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddCommGroup.toAddGroup instAddCommGroupHom ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.addCommGroup isTopologicalAddGroup	—	—
instHasColimitOfModuleCatCompForget₂ContinuousLinearMapIdCarrierLinearMap 📖	mathematical	—	CategoryTheory.Limits.HasColimit TopModuleCat instCategory	—	—
instHasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits TopModuleCat instCategory	—	instHasColimitsOfShapeOfModuleCat ModuleCat.hasColimitsOfShape AddCommGrpCat.hasColimitsOfShape UnivLE.small UnivLE.self
instHasColimitsOfShapeOfModuleCat 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape TopModuleCat instCategory	—	instHasColimitOfModuleCatCompForget₂ContinuousLinearMapIdCarrierLinearMap CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
instHasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits TopModuleCat instCategory	—	hasLimit_of_hasLimit_forget₂ ModuleCat.hasLimit small_subtype small_Pi UnivLE.small UnivLE.self
instHasLimitsOfShapeOfModuleCat 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape TopModuleCat instCategory	—	hasLimit_of_hasLimit_forget₂ CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
instIsLeftAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint TopModuleCat instCategory ModuleCat ModuleCat.moduleCategory CategoryTheory.forget₂ ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike instConcreteCategoryContinuousLinearMapIdCarrier LinearMap LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier instHasForget₂ContinuousLinearMapIdCarrierModuleCatLinearMap	—	—
instIsLeftAdjointModuleCatWithModuleTopology 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint ModuleCat ModuleCat.moduleCategory TopModuleCat instCategory withModuleTopology	—	—
instIsLeftAdjointTopCatFree 📖	mathematical	—	CategoryTheory.Functor.IsLeftAdjoint TopCat TopCat.instCategory TopModuleCat instCategory free	—	—
instIsRightAdjointModuleCatForget₂ContinuousLinearMapIdCarrierLinearMap 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint ModuleCat ModuleCat.moduleCategory TopModuleCat instCategory CategoryTheory.forget₂ ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike instConcreteCategoryContinuousLinearMapIdCarrier LinearMap LinearMap.instFunLike ModuleCat.instConcreteCategoryLinearMapIdCarrier instHasForget₂ContinuousLinearMapIdCarrierModuleCatLinearMap	—	—
instIsRightAdjointModuleCatIndiscrete 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint TopModuleCat instCategory ModuleCat ModuleCat.moduleCategory indiscrete	—	—
instIsRightAdjointTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier 📖	mathematical	—	CategoryTheory.Functor.IsRightAdjoint TopCat TopCat.instCategory TopModuleCat instCategory CategoryTheory.forget₂ ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike instConcreteCategoryContinuousLinearMapIdCarrier ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier instHasForget₂ContinuousLinearMapIdCarrierTopCatContinuousMapCarrier	—	—
instIsTopologicalAddGroupCarrier 📖	mathematical	—	IsTopologicalAddGroup ModuleCat.carrier toModuleCat instTopologicalSpaceCarrier AddCommGroup.toAddGroup ModuleCat.isAddCommGroup	—	isTopologicalAddGroup
instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit TopModuleCat instCategory TopCat TopCat.instCategory CategoryTheory.forget₂ ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike instConcreteCategoryContinuousLinearMapIdCarrier ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier instHasForget₂ContinuousLinearMapIdCarrierTopCatContinuousMapCarrier	—	CategoryTheory.Limits.preservesLimit_of_preserves_limit_cone
instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfShape TopModuleCat instCategory TopCat TopCat.instCategory CategoryTheory.forget₂ ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike instConcreteCategoryContinuousLinearMapIdCarrier ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier instHasForget₂ContinuousLinearMapIdCarrierTopCatContinuousMapCarrier	—	instPreservesLimitTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitOfModuleCatCompLinearMapForget CategoryTheory.Limits.hasLimitOfHasLimitsOfShape CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit
instPreservesLimitsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier 📖	mathematical	—	CategoryTheory.Limits.PreservesLimits TopModuleCat instCategory TopCat TopCat.instCategory CategoryTheory.forget₂ ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike instConcreteCategoryContinuousLinearMapIdCarrier ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier instHasForget₂ContinuousLinearMapIdCarrierTopCatContinuousMapCarrier	—	instPreservesLimitsOfShapeTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrierOfHasLimitsOfShapeOfModuleCatForgetLinearMap CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits ModuleCat.hasLimits CategoryTheory.Limits.PreservesLimitsOfSize.preservesLimitsOfShape ModuleCat.forget_preservesLimits
instReflectsIsomorphismsTopCatForget₂ContinuousLinearMapIdCarrierContinuousMapCarrier 📖	mathematical	—	CategoryTheory.Functor.ReflectsIsomorphisms TopModuleCat instCategory TopCat TopCat.instCategory CategoryTheory.forget₂ ContinuousLinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddCommMonoid ModuleCat.isAddCommGroup ModuleCat.isModule ContinuousLinearMap.funLike instConcreteCategoryContinuousLinearMapIdCarrier ContinuousMap TopCat.carrier TopCat.str ContinuousMap.instFunLike TopCat.instConcreteCategoryContinuousMapCarrier instHasForget₂ContinuousLinearMapIdCarrierTopCatContinuousMapCarrier	—	RingHomInvPair.ids Equiv.left_inv Equiv.right_inv Homeomorph.continuous_toFun Homeomorph.continuous_invFun CategoryTheory.Iso.isIso_hom
isTopologicalAddGroup 📖	mathematical	—	IsTopologicalAddGroup ModuleCat.carrier toModuleCat topologicalSpace AddCommGroup.toAddGroup ModuleCat.isAddCommGroup	—	—
ofHom_hom 📖	mathematical	—	ofHom ModuleCat.carrier toModuleCat ModuleCat.isAddCommGroup ModuleCat.isModule topologicalSpace IsTopologicalAddGroup.toContinuousAdd AddCommGroup.toAddGroup isTopologicalAddGroup continuousSMul Hom.hom	—	IsTopologicalAddGroup.toContinuousAdd isTopologicalAddGroup continuousSMul

TopModuleCat.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	18 math math: TopModuleCat.hom_cokerπ, TopModuleCat.hom_zero, TopModuleCat.hom_zero_apply, ContinuousCohomology.I_obj_ρ_apply, TopModuleCat.ofHom_hom, ContinuousCohomology.Iobj_ρ_apply, TopModuleCat.hom_add, TopModuleCat.hom_zsmul, ContinuousCohomology.I_map_hom, TopModuleCat.hom_sub, TopModuleCat.hom_nsmul, TopModuleCat.hom_ofHom, TopModuleCat.cokerπ_surjective, TopModuleCat.hom_smul, TopModuleCat.kerι_apply, TopModuleCat.hom_comp, TopModuleCat.hom_neg, TopModuleCat.hom_forget₂_TopCat_map
hom' 📖	CompOp	—

TopModuleCat.Hom.Simps

Definitions

Name	Category	Theorems
hom 📖	CompOp	—

---

← Back to Index