EmbeddingRing

Mathlib.CategoryTheory.Abelian.FreydMitchell

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Abelian.FreydMitchell.EmbeddingRing

Lean4

/-- Given an abelian category `C`, this is a ring such that there is a full, faithful and exact
embedding `C ⥤ ModuleCat (EmbeddingRing C)`.

It is probably not a good idea to unfold this. -/
def EmbeddingRing : Type (max u v) :=
  IsGrothendieckAbelian.OppositeModuleEmbedding.EmbeddingRing (Ind.yoneda (C := (AsSmall.{max u v} C)ᵒᵖ)).rightOp

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

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

Разделы

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

Аффилиация

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