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.α

theorem TopCommRingCat.isTopologicalRing (self : TopCommRingCat) : TopologicalRing self.α

instance TopCommRingCat.instInhabited : Inhabited TopCommRingCat

Equations

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

instance TopCommRingCat.instCoeSortType : CoeSort TopCommRingCat (Type u)

Equations

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

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

Equations

• TopCommRingCat.instCategory = CategoryTheory.Category.mk @TopCommRingCat.instCategory.proof_3 @TopCommRingCat.instCategory.proof_4 @TopCommRingCat.instCategory.proof_5

instance TopCommRingCat.instConcreteCategory : 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).obj R)

Equations

• R.forgetTopologicalSpace = R.isTopologicalSpace

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

Equations

• R.forgetCommRing = R.isCommRing

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

Equations

• ⋯ = ⋯

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).obj R)

Equations

• R.forgetToCommRingCatTopologicalSpace = 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).obj R)

Equations

• R.forgetToTopCatCommRing = R.isCommRing

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

Equations

• ⋯ = ⋯

instance TopCommRingCat.instReflectsIsomorphismsTopCatForget₂ : (CategoryTheory.forget₂ TopCommRingCat TopCat).ReflectsIsomorphisms

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

Equations

• TopCommRingCat.instReflectsIsomorphismsTopCatForget₂ = ⋯