Documentation Verification Report

TopCommRingCat

📁 Source: Mathlib/Topology/Category/TopCommRingCat.lean

Statistics

Metric	Count
Definitions `TopCommRingCat`, `forgetToCommRingCatTopologicalSpace`, `forgetToTopCatCommRing`, `hasForgetToCommRingCat`, `hasForgetToTopCat`, `instCategory`, `instCoeSortType`, `instConcreteCategorySubtypeRingHomαContinuousCoe`, `instFunLikeSubtypeRingHomαContinuousCoe`, `instInhabited`, `isCommRing`, `isTopologicalSpace`, `α`	13
Theorems `coe_of`, `forgetToTopCatTopologicalRing`, `instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier`, `isTopologicalRing`	4
Total	17

TopCommRingCat

Definitions

Name	Category	Theorems
`forgetToCommRingCatTopologicalSpace` 📖	CompOp	—
`forgetToTopCatCommRing` 📖	CompOp	1 math math: `forgetToTopCatTopologicalRing`
`hasForgetToCommRingCat` 📖	CompOp	—
`hasForgetToTopCat` 📖	CompOp	2 math math: `instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier`, `forgetToTopCatTopologicalRing`
`instCategory` 📖	CompOp	2 math math: `instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier`, `forgetToTopCatTopologicalRing`
`instCoeSortType` 📖	CompOp	—
`instConcreteCategorySubtypeRingHomαContinuousCoe` 📖	CompOp	2 math math: `instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier`, `forgetToTopCatTopologicalRing`
`instFunLikeSubtypeRingHomαContinuousCoe` 📖	CompOp	2 math math: `instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier`, `forgetToTopCatTopologicalRing`
`instInhabited` 📖	CompOp	—
`isCommRing` 📖	CompOp	3 math math: `instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier`, `forgetToTopCatTopologicalRing`, `isTopologicalRing`
`isTopologicalSpace` 📖	CompOp	3 math math: `instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier`, `forgetToTopCatTopologicalRing`, `isTopologicalRing`
`α` 📖	CompOp	4 math math: `instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier`, `coe_of`, `forgetToTopCatTopologicalRing`, `isTopologicalRing`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_of` 📖	mathematical	—	`α` `of`	—	—
`forgetToTopCatTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `TopCat.carrier` `CategoryTheory.Functor.obj` `TopCommRingCat` `instCategory` `TopCat` `TopCat.instCategory` `CategoryTheory.forget₂` `RingHom` `α` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `isCommRing` `Continuous` `isTopologicalSpace` `DFunLike.coe` `RingHom.instFunLike` `instFunLikeSubtypeRingHomαContinuousCoe` `instConcreteCategorySubtypeRingHomαContinuousCoe` `ContinuousMap` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `hasForgetToTopCat` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `forgetToTopCatCommRing`	—	`isTopologicalRing`
`instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier` 📖	mathematical	—	`CategoryTheory.Functor.ReflectsIsomorphisms` `TopCommRingCat` `instCategory` `TopCat` `TopCat.instCategory` `CategoryTheory.forget₂` `RingHom` `α` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `isCommRing` `Continuous` `isTopologicalSpace` `DFunLike.coe` `RingHom.instFunLike` `instFunLikeSubtypeRingHomαContinuousCoe` `instConcreteCategorySubtypeRingHomαContinuousCoe` `ContinuousMap` `TopCat.carrier` `TopCat.str` `ContinuousMap.instFunLike` `TopCat.instConcreteCategoryContinuousMapCarrier` `hasForgetToTopCat`	—	`Equiv.left_inv` `Equiv.right_inv` `MonoidHom.map_mul'` `RingHom.map_add'` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `ContinuousMap.continuous_toFun` `CategoryTheory.ConcreteCategory.ext` `RingHom.ext`
`isTopologicalRing` 📖	mathematical	—	`IsTopologicalRing` `α` `isTopologicalSpace` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `isCommRing`	—	—

(root)

Definitions

Name	Category	Theorems
`TopCommRingCat` 📖	CompData	2 math math: `TopCommRingCat.instReflectsIsomorphismsTopCatForget₂SubtypeRingHomαContinuousCoeContinuousMapCarrier`, `TopCommRingCat.forgetToTopCatTopologicalRing`

---

← Back to Index