instFunLikeSubtypeRingHomαContinuousCoe

English

There exists a forgetful functor from TopCommRingCat to CommRingCat.

Русский

Существует функтор забывания от TopCommRingCat к CommRingCat.

LaTeX

$$$\\text{forget}_{\\mathrm{TopCommRingCat} \\to \\mathrm{CommRingCat}} : \\text{TopCommRingCat} \\to \\mathrm{CommRingCat}$$$

Lean4

instance (R S : TopCommRingCat.{u}) : FunLike { f : R →+* S // Continuous f } R S
    where
  coe f := f.val
  coe_injective' _ _ h := Subtype.ext (DFunLike.coe_injective h)

Похожие утверждения