Theorems · Definition · category theory
TopModuleCat.toModuleCat
{R : Type u} → [inst : Ring R] → [inst_1 : TopologicalSpace R] → TopModuleCat R → ModuleCat R- Cited by
- 29 results in Mathlib
- Foundations
- Depth 2 from the axioms · uses no axioms
- Assumes
- RingTopologicalSpace
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites4
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- TopologicalSpacestatement and proof · cited by 24,529
- Ringstatement and proof · cited by 7,463
- ModuleCatstatement · cited by 1,429
- TopModuleCatstatement and proof · cited by 45
Cited by56
Results whose statement or proof uses this declaration.
- TopModuleCat.Hom.homstatement · cited by 22
- TopModuleCat.cokerproof · cited by 3
- TopModuleCat.endRingEquivstatement · cited by 2
- ContinuousCohomology.cochainsMap_idproof · cited by 2
- TopModuleCat.kerproof · cited by 2
- TopRep.homogeneousCochains.d_applystatement and proof · cited by 2
- ContinuousCohomology.cochainsMap_compproof · cited by 1
- TopModuleCat.ofIsostatement and proof · cited by 0
- TopModuleCat.toCoinducedstatement and proof · cited by 0
- TopModuleCat.withModuleTopologyAdjstatement · cited by 0
- CategoryTheory.Iso.toContinuousLinearEquivstatement and proof · cited by 0
- TopModuleCat.coe_freeObjstatement · cited by 0