preregular

Mathlib.CategoryTheory.Sites.Coherent.Equivalence

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Equivalence.preregular

English

Preregular property is preserved by equivalence of categories.

Русский

Свойство preregular сохраняется при эквивалентности категорий.

LaTeX

$$$\text{Preregular}(D) \text{ if } \text{Preregular}(C) \text{ and } e: C \simeq D$$$

Lean4

/-- `Preregular` is preserved by equivalence of categories. -/
theorem preregular (e : C ≌ D) : Preregular D :=
  e.inverse.reflects_preregular

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

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

Разделы

Аффилиация

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