inverse

Mathlib.CategoryTheory.Monoidal.Internal.Types.Grp_

URI: https://scilib.ai/kg/mathlib#GrpTypeEquivalenceGrp.inverse

Lean4

/-- Converting a group into a group object in `Type u`. -/
noncomputable def inverse : GrpCat.{u} ⥤ Grp_ (Type u)
    where
  obj
    A :=
    { MonTypeEquivalenceMon.inverse.obj ((forget₂ GrpCat MonCat).obj A) with
      grp :=
        { inv := ((·⁻¹) : A → A)
          left_inv := by
            ext x
            exact inv_mul_cancel (G := A) x
          right_inv := by
            ext x
            exact mul_inv_cancel (G := A) x } }
  map f := MonTypeEquivalenceMon.inverse.map ((forget₂ GrpCat MonCat).map f)

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

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

Разделы

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

Аффилиация

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