instFullModuleCatEmbeddingRingFunctor

Mathlib.CategoryTheory.Abelian.FreydMitchell

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

← MathLib Explorer

English

The Freyd–Mitchell embedding functor is full.

Русский

Функтор Фрейда–Митчелла является полным.

LaTeX

$$$\mathrm{FreydMitchell.functor}(C)\ \text{is full}$$$

Lean4

instance : (functor C).Full := by
  rw [functor]
  have : (F C).Full := by rw [F]; infer_instance
  have : (G C).Full := by rw [G]; infer_instance
  have : (G C ⋙ H C).Full := IsGrothendieckAbelian.OppositeModuleEmbedding.full_embedding _
  infer_instance

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

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

Разделы

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

Аффилиация

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