sectionsSubgroup

Mathlib.Algebra.Category.Grp.Limits

URI: https://scilib.ai/kg/mathlib#GrpCat.sectionsSubgroup

Lean4

/-- The flat sections of a functor into `GrpCat` form a subgroup of all sections. -/
@[to_additive /-- The flat sections of a functor into `AddGrpCat` form an additive subgroup of all sections. -/
    ]
def sectionsSubgroup : Subgroup (∀ j, F.obj j) :=
  {
    MonCat.sectionsSubmonoid
      (F ⋙ forget₂ GrpCat MonCat) with
    carrier := (F ⋙ forget GrpCat).sections
    inv_mem' := fun {a} ah j j' f => by
      simp only [Functor.comp_map, Pi.inv_apply]
      dsimp [Functor.sections] at ah ⊢
      rw [(F.map f).hom.map_inv (a j), ah f] }

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

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

Разделы

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

Аффилиация

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