adjoinOne

Mathlib.Algebra.Category.MonCat.Adjunctions

URI: https://scilib.ai/kg/mathlib#MonCat.adjoinOne

Lean4

/-- The functor of adjoining a neutral element `one` to a semigroup. -/
@[to_additive (attr := simps) /-- The functor of adjoining a neutral element `zero` to a semigroup -/
    ]
def adjoinOne : Semigrp.{u} ⥤ MonCat.{u} where
  obj S := MonCat.of (WithOne S)
  map f := ofHom (WithOne.mapMulHom f.hom)
  map_id _ := MonCat.hom_ext WithOne.mapMulHom_id
  map_comp _ _ := MonCat.hom_ext (WithOne.mapMulHom_comp _ _)

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

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

Разделы

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

Аффилиация

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