instEpiModuleCatCarrierObjOppositeRingCatApp

Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono

URI: https://scilib.ai/kg/mathlib#PresheafOfModules.instEpiModuleCatCarrierObjOppositeRingCatApp

English

A morphism f is epic iff each component f.app X is surjective.

Русский

Морфизм f есть эпиморфизм тогда и только тогда, когда каждый компонент f.app X сюръективен.

LaTeX

$$$\\mathrm{Epi}(f) \\iff \\forall X, \\mathrm{Surjective}(f.app X)$$$

Lean4

instance [Epi f] (X : Cᵒᵖ) : Epi (f.app X) :=
  inferInstanceAs (Epi ((evaluation R X).map f))

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

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

Разделы

Аффилиация

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