instCommRingHomObjTopCommRingCatForget₂

English

The hom-set inherits a commutative ring structure from the underlying forgetful construction.

Русский

Множество гом имеет структуру коммутативного кольца, полученную из соответствующей забывающей конструкии.

LaTeX

$$$\\mathrm{Hom}(X, (forget\\_2 TopCommRingCat TopCat).obj(R)) \\cong \\text{CommRing}$$$

Lean4

instance : CommRing (X ⟶ (forget₂ TopCommRingCat TopCat).obj R) :=
  Function.Injective.commRing _ ConcreteCategory.hom_injective rfl rfl (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
    (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ _ => rfl) (fun _ => rfl)
    (fun _ => rfl)
      -- TODO upgrade the result to TopCommRing?

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