sectionsSubring

Mathlib.Algebra.Category.Ring.Limits

URI: https://scilib.ai/kg/mathlib#RingCat.sectionsSubring

Lean4

/-- The flat sections of a functor into `RingCat` form a subring of all sections.
-/
def sectionsSubring : Subring (∀ j, F.obj j) :=
  let f : J ⥤ AddGrpCat.{u} := F ⋙ forget₂ RingCat.{u} AddCommGrpCat.{u} ⋙ forget₂ AddCommGrpCat.{u} AddGrpCat.{u}
  let g : J ⥤ SemiRingCat.{u} := F ⋙ forget₂ RingCat.{u} SemiRingCat.{u}
  { AddGrpCat.sectionsAddSubgroup (J := J) f, SemiRingCat.sectionsSubsemiring (J := J) g with
    carrier := (F ⋙ forget RingCat.{u}).sections }

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru