Zero objects in TopModuleCat #
A topological module whose carrier is a subsingleton is a zero object of TopModuleCat R
(TopModuleCat.isZero_of_subsingleton), the counterpart for TopModuleCat R of
ModuleCat.isZero_of_subsingleton. It turns the vanishing of a cohomology module of
TopModuleCat R, recorded as a Subsingleton instance on its carrier, into the categorical
statement IsZero used by bundled interfaces.
theorem
TopModuleCat.isZero_of_subsingleton
{R : Type u_1}
[Ring R]
[TopologicalSpace R]
(M : TopModuleCat R)
[Subsingleton ↑M.toModuleCat]
:
A topological module whose carrier is a subsingleton is a zero object, as in
ModuleCat.isZero_of_subsingleton.