comap

Mathlib.CategoryTheory.Monoidal.Mod_

URI: https://scilib.ai/kg/mathlib#Mod_.comap

Lean4

/-- A morphism of monoid objects induces a "restriction" or "comap" functor
between the categories of module objects.
-/
@[simps]
def comap {A B : C} [MonObj A] [MonObj B] (f : A ⟶ B) [IsMonHom f] : Mod_ D B ⥤ Mod_ D A
    where
  obj
    M :=
    letI := scalarRestriction f M.X
    ⟨M.X⟩
  map {M N}
    g :=
    letI := scalarRestriction_hom f M.X N.X g.hom
    ⟨g.hom⟩
      -- Lots more could be said about `comap`, e.g. how it interacts with
      -- identities, compositions, and equalities of monoid object morphisms.

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

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

Разделы

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

Аффилиация

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