instRingElemForallObjCompForgetSections

English

There is a Small instance for the subtype describing carrier elements that lie in sectionsSubalgebra, for all objects in J.

Русский

Существует объект Small для подтипа, описывающего носители, принадлежащие sectionsSubalgebra, для всех объектов J.

LaTeX

$$Small (Subtype (λ x, x ∈ AlgCat.sectionsSubalgebra F))$$

Lean4

instance (F : J ⥤ AlgCat.{w} R) : Ring (F ⋙ forget _).sections :=
  inferInstanceAs <| Ring (sectionsSubalgebra F)

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