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.

Equations

• TopCommRingCat.delabOf = Lean.PrettyPrinter.Delaborator.delabApp

@[implicit_reducible]

instance TopCommRingCat.instInhabited : Inhabited TopCommRingCat

Equations

• TopCommRingCat.instInhabited = { default := TopCommRingCat.of PUnit.{?u.3 + 1} }

@[implicit_reducible]

instance TopCommRingCat.instCoeSortType : CoeSort TopCommRingCat (Type u)

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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' := ⋯ }

@[implicit_reducible]

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.

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

Equations

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

@[implicit_reducible]

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

Equations

• R.forgetToCommRingCatTopologicalSpace = R.isTopologicalSpace

@[implicit_reducible]

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.

@[implicit_reducible]

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