mathlib3 documentation

topology.category.TopCommRing

Category of topological commutative rings #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Instances for TopCommRing
@[protected, instance]
Equations
@[protected, instance]
Equations

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

Equations
@[protected, instance]
Equations
@[protected, instance]

The forgetful functor to Top.

Equations
@[protected, instance]

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