instAlgebraElemForallObjCompForgetSections

English

There is a Small instance for the subtype of all carriers lying in sectionsSubalgebra, across all objects of J.

Русский

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

LaTeX

$$Small (Subtype (fun x => SetLike.instMembership.mem (AlgCat.sectionsSubalgebra F) x))$$

Lean4

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

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