instConcreteCategorySubtypeRingHomαContinuousCoe

English

The subtype of continuous ring homomorphisms carries a concrete category structure.

Русский

Подтип непрерывных кольцевых гомоморфизмов несёт структуру конкретной категории.

LaTeX

$$$\\text{Subtype\\_ContinuousRingHom} \\; \\text{has a concrete category structure}.$$$

Lean4

instance : ConcreteCategory TopCommRingCat.{u} fun R S => { f : R →+* S // Continuous f }
    where
  hom f := f
  ofHom f := f

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