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.

source

structure TopCommRingCat :

Type (u + 1)

α : Type u
carrier of a topological commutative ring.
isCommRing : CommRing s.α
isTopologicalSpace : TopologicalSpace s.α
isTopologicalRing : TopologicalRing s.α

A bundled topological commutative ring.

Instances For

source

instance TopCommRingCat.instInhabitedTopCommRingCat :

Inhabited TopCommRingCat

source

instance TopCommRingCat.instCoeSortTopCommRingCatType :

CoeSort TopCommRingCat (Type u)

source

instance TopCommRingCat.instCategoryTopCommRingCat :

CategoryTheory.Category.{u, u + 1} TopCommRingCat

source

instance TopCommRingCat.instConcreteCategoryTopCommRingCatInstCategoryTopCommRingCat :

CategoryTheory.ConcreteCategory TopCommRingCat

source

def TopCommRingCat.of (X : Type u) [CommRing X] [TopologicalSpace X] [TopologicalRing X] :

TopCommRingCat

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

Instances For

source

@[simp]

theorem TopCommRingCat.coe_of (X : Type u) [CommRing X] [TopologicalSpace X] [TopologicalRing X] :

(TopCommRingCat.of X).α = X

source

instance TopCommRingCat.forgetTopologicalSpace (R : TopCommRingCat) :

TopologicalSpace ((CategoryTheory.forget TopCommRingCat).obj R)

source

instance TopCommRingCat.forgetCommRing (R : TopCommRingCat) :

CommRing ((CategoryTheory.forget TopCommRingCat).obj R)

source

instance TopCommRingCat.forgetTopologicalRing (R : TopCommRingCat) :

TopologicalRing ((CategoryTheory.forget TopCommRingCat).obj R)

source

instance TopCommRingCat.hasForgetToCommRingCat :

CategoryTheory.HasForget₂ TopCommRingCat CommRingCat

source

instance TopCommRingCat.forgetToCommRingCatTopologicalSpace (R : TopCommRingCat) :

TopologicalSpace ↑((CategoryTheory.forget₂ TopCommRingCat CommRingCat).obj R)

source

instance TopCommRingCat.hasForgetToTopCat :

CategoryTheory.HasForget₂ TopCommRingCat TopCat

The forgetful functor to TopCat.

source

instance TopCommRingCat.forgetToTopCatCommRing (R : TopCommRingCat) :

CommRing ↑((CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

source

instance TopCommRingCat.forgetToTopCatTopologicalRing (R : TopCommRingCat) :

TopologicalRing ↑((CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

source

instance TopCommRingCat.instReflectsIsomorphismsTopCommRingCatInstCategoryTopCommRingCatTopCatInstTopCatLargeCategoryForget₂InstConcreteCategoryTopCommRingCatInstCategoryTopCommRingCatConcreteCategoryHasForgetToTopCat :

CategoryTheory.ReflectsIsomorphisms (CategoryTheory.forget₂ TopCommRingCat TopCat)

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