instMonoModuleCatCarrierObjOppositeRingCatApp

Mathlib.Algebra.Category.ModuleCat.Presheaf.EpiMono

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

English

A morphism f is mono iff each component f.app X is injective.

Русский

Монообраз функторa равносилен тому, что каждый компонент инъективен.

LaTeX

$$$\\mathrm{Mono}(f) \\iff \\forall X, \\mathrm{Injective}(f.app X)$$$

Lean4

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

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

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

Разделы

Аффилиация

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