Category of topological commutative rings #

We introduce the category TopCommRingCat of topological commutative rings together with the relevant forgetful functors to topological spaces and commutative rings.

structure TopCommRingCat :
Type (u + 1)

A bundled topological commutative ring.

Instances For

    Construct a bundled TopCommRingCat from the underlying type and the appropriate typeclasses.

    Instances For