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 : IsTopologicalRing self.α

instance TopCommRingCat.instInhabited : Inhabited TopCommRingCat

Equations

• TopCommRingCat.instInhabited = { default := TopCommRingCat.mk PUnit.{?u.3 + 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.instFunLikeSubtypeRingHomαContinuousCoe (R S : TopCommRingCat) : FunLike { f : R.α →+* S.α // Continuous ⇑f } R.α S.α

Equations

• R.instFunLikeSubtypeRingHomαContinuousCoe S = { coe := fun (f : { f : R.α →+* S.α // Continuous ⇑f }) => ⇑↑f, coe_injective' := ⋯ }

instance TopCommRingCat.instConcreteCategorySubtypeRingHomαContinuousCoe : CategoryTheory.ConcreteCategory TopCommRingCat fun (R S : TopCommRingCat) => { f : R.α →+* S.α // Continuous ⇑f }

Equations

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

@[reducible, inline]

abbrev TopCommRingCat.of (X : Type u) [CommRing X] [TopologicalSpace X] [IsTopologicalRing X] : TopCommRingCat

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

Equations

• TopCommRingCat.of X = TopCommRingCat.mk X

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

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) : IsTopologicalRing ↑((CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

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.