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.
A bundled topological commutative ring.
- α : Type u
carrier of a topological commutative ring.
- isTopologicalSpace : TopologicalSpace self.α
- isTopologicalRing : TopologicalRing self.α
Instances For
Equations
- TopCommRingCat.instInhabited = { default := TopCommRingCat.mk PUnit.{?u.3 + 1} }
Equations
- TopCommRingCat.instCoeSortType = { coe := TopCommRingCat.α }
Equations
- One or more equations did not get rendered due to their size.
Construct a bundled TopCommRingCat
from the underlying type and the appropriate typeclasses.
Instances For
@[simp]
Equations
- One or more equations did not get rendered due to their size.
The forgetful functor to TopCat
.
Equations
- One or more equations did not get rendered due to their size.
The forgetful functors to Type
do not reflect isomorphisms,
but the forgetful functor from TopCommRingCat
to TopCat
does.