instPreservesEffectiveEpiFamiliesOfIsEquivalence

Mathlib.CategoryTheory.EffectiveEpi.Preserves

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.instPreservesEffectiveEpiFamiliesOfIsEquivalence

English

If F is an equivalence, then F preserves effective epi families.

Русский

Если F — эквивалентность, тогда F сохраняет эффективные эпиморфные семейства.

LaTeX

$$$[IsEquivalence F] \Rightarrow F.PreservesEffectiveEpiFamilies$$$

Lean4

instance (F : C ⥤ D) [IsEquivalence F] : F.PreservesEffectiveEpiFamilies where preserves _ _ := inferInstance

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

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

Разделы

Аффилиация

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