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.

• α : Type u

  carrier of a topological commutative ring.

• isCommRing : CommRing self.α
• isTopologicalSpace : TopologicalSpace self.α
• isTopologicalRing : TopologicalRing self.α

instance TopCommRingCat.instInhabitedTopCommRingCat : Inhabited TopCommRingCat

Equations

• TopCommRingCat.instInhabitedTopCommRingCat = { default := TopCommRingCat.mk PUnit.{u_1 + 1} }

instance TopCommRingCat.instCoeSortTopCommRingCatType : CoeSort TopCommRingCat (Type u)

Equations

• TopCommRingCat.instCoeSortTopCommRingCatType = { coe := TopCommRingCat.α }

instance TopCommRingCat.instCategoryTopCommRingCat : CategoryTheory.Category.{u, u + 1} TopCommRingCat

Equations

• TopCommRingCat.instCategoryTopCommRingCat = CategoryTheory.Category.mk

instance TopCommRingCat.instConcreteCategoryTopCommRingCatInstCategoryTopCommRingCat : CategoryTheory.ConcreteCategory TopCommRingCat

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• TopCommRingCat.of X = TopCommRingCat.mk X

@[simp]

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

instance TopCommRingCat.forgetTopologicalSpace (R : TopCommRingCat) : TopologicalSpace ((CategoryTheory.forget TopCommRingCat).toPrefunctor.obj R)

Equations

• TopCommRingCat.forgetTopologicalSpace R = R.isTopologicalSpace

instance TopCommRingCat.forgetCommRing (R : TopCommRingCat) : CommRing ((CategoryTheory.forget TopCommRingCat).toPrefunctor.obj R)

Equations

• TopCommRingCat.forgetCommRing R = R.isCommRing

instance TopCommRingCat.forgetTopologicalRing (R : TopCommRingCat) : TopologicalRing ((CategoryTheory.forget TopCommRingCat).toPrefunctor.obj R)

Equations

• (_ : TopologicalRing ((CategoryTheory.forget TopCommRingCat).toPrefunctor.obj R)) = (_ : TopologicalRing R.α)

instance TopCommRingCat.hasForgetToCommRingCat : CategoryTheory.HasForget₂ TopCommRingCat CommRingCat

Equations

• One or more equations did not get rendered due to their size.

instance TopCommRingCat.forgetToCommRingCatTopologicalSpace (R : TopCommRingCat) : TopologicalSpace ↑((CategoryTheory.forget₂ TopCommRingCat CommRingCat).toPrefunctor.obj R)

Equations

• TopCommRingCat.forgetToCommRingCatTopologicalSpace R = R.isTopologicalSpace

instance TopCommRingCat.hasForgetToTopCat : CategoryTheory.HasForget₂ TopCommRingCat TopCat

The forgetful functor to TopCat.

Equations

• One or more equations did not get rendered due to their size.

instance TopCommRingCat.forgetToTopCatCommRing (R : TopCommRingCat) : CommRing ↑((CategoryTheory.forget₂ TopCommRingCat TopCat).toPrefunctor.obj R)

Equations

• TopCommRingCat.forgetToTopCatCommRing R = R.isCommRing

instance TopCommRingCat.forgetToTopCatTopologicalRing (R : TopCommRingCat) : TopologicalRing ↑((CategoryTheory.forget₂ TopCommRingCat TopCat).toPrefunctor.obj R)

Equations

• (_ : TopologicalRing ↑((CategoryTheory.forget₂ TopCommRingCat TopCat).toPrefunctor.obj R)) = (_ : TopologicalRing R.α)

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.

Equations

• One or more equations did not get rendered due to their size.