sectionsSubsemiring — Mathlib

English

The carrier of the limit cone object in SemiRingCat becomes a semiring (via forgetful functor and construction from Subsemirings).

Русский

Носитель предельного конуса в SemiRingCat наделяется структурой полусредства.

LaTeX

$$$\text{Semiring}(\mathrm{Types.Small.limitCone} (F \!\to\! \text{forget SemiRingCat})) .pt$$$

Lean4

/-- The flat sections of a functor into `SemiRingCat` form a subsemiring of all sections. -/
def sectionsSubsemiring : Subsemiring (∀ j, F.obj j) :=
  { (MonCat.sectionsSubmonoid (J := J) (F ⋙ forget₂ SemiRingCat.{u} MonCat.{u})),
    (AddMonCat.sectionsAddSubmonoid (J := J)
      (F ⋙ forget₂ SemiRingCat.{u} AddCommMonCat.{u} ⋙ forget₂ AddCommMonCat AddMonCat)) with
    carrier := (F ⋙ forget SemiRingCat).sections }

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