instIsStableUnderBaseChangeEpimorphisms

Mathlib.CategoryTheory.Abelian.Monomorphisms

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

← MathLib Explorer

English

Epimorphisms are stable under base change in an abelian category.

Русский

Эпиморфизм сохраняется при базовом изменении в абелевой категории.

LaTeX

$$$\\text{epimorphisms} \\text{ is stable under base change}$$$

Lean4

instance : (epimorphisms C).IsStableUnderBaseChange :=
  IsStableUnderBaseChange.mk'
    (fun _ _ _ f g _ hf ↦ by
      simp only [epimorphisms.iff] at hf ⊢
      infer_instance)

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

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

Разделы

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

Аффилиация

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