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.

• of :: (
• α : Type u

  carrier of a topological commutative ring.

• isCommRing : CommRing self.α
• isTopologicalSpace : TopologicalSpace self.α
• isTopologicalRing : IsTopologicalRing self.α
• )

def TopCommRingCat.delabOf : Lean.PrettyPrinter.Delaborator.Delab

This prevents TopCommRingCat.of R being printed as { α := R, ... } by delabStructureInstance.

@[implicit_reducible]

instance TopCommRingCat.instInhabited : Inhabited TopCommRingCat

@[implicit_reducible]

instance TopCommRingCat.instCoeSortType : CoeSort TopCommRingCat (Type u)

@[implicit_reducible]

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

@[implicit_reducible]

instance TopCommRingCat.instFunLikeSubtypeRingHomαContinuousCoe (R S : TopCommRingCat) : FunLike { f : R.α →+* S.α // Continuous ⇑f } R.α S.α

@[implicit_reducible]

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

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

@[implicit_reducible]

instance TopCommRingCat.hasForgetToCommRingCat : CategoryTheory.HasForget₂ TopCommRingCat CommRingCat

@[implicit_reducible]

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

@[implicit_reducible]

instance TopCommRingCat.hasForgetToTopCat : CategoryTheory.HasForget₂ TopCommRingCat TopCat

The forgetful functor to TopCat.

@[implicit_reducible]

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

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

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

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