mathlib documentation

topology.category.TopCommRing

Category of topological commutative rings #

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

structure TopCommRing  :
Type (u+1)

A bundled topological commutative ring.

@[instance]
Equations
@[instance]
Equations

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

Equations
@[simp]
@[instance]
Equations
@[instance]

The forgetful functor to Top.

Equations
@[instance]

The forgetful functors to Type do not reflect isomorphisms, but the forgetful functor from TopCommRing to Top does.