algebraObj — Mathlib

English

For a functor F: J ⥤ AlgCat R, the sectionsSubalgebra F forms a small subalgebra of all sections; i.e., its underlying type is small in universe w.

Русский

Для F: J ⥤ AlgCat R множество секций образует малую подалгебру всех секций, т.е. её носитель мал в вселенной w.

LaTeX

$$Small (sectionsSubalgebra F)$$

Lean4

instance algebraObj (j) : Algebra R ((F ⋙ forget (AlgCat R)).obj j) :=
  inferInstanceAs <| Algebra R (F.obj j)

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