instEffectiveEpiOfRegularEpi

Mathlib.CategoryTheory.EffectiveEpi.RegularEpi

URI: https://scilib.ai/kg/mathlib#CategoryTheory.instEffectiveEpiOfRegularEpi

English

In any category, every RegularEpi morphism is an EffectiveEpi morphism.

Русский

В любой категории каждый регулярный эпиморфизм является эффективным эпиморфизмом.

LaTeX

$$$\\forall {C} [\\mathbf{Category} C] {f : X \\to B} [RegularEpi f], \\operatorname{EffectiveEpi} f$$

Lean4

instance {B X : C} (f : X ⟶ B) [RegularEpi f] : EffectiveEpi f :=
  ⟨⟨effectiveEpiStructOfRegularEpi f⟩⟩

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

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

Разделы

Аффилиация

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