instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction

Mathlib.CategoryTheory.Galois.Action

URI: https://scilib.ai/kg/mathlib#CategoryTheory.PreGaloisCategory.instReflectsMonomorphismsActionFintypeCatAutFunctorFunctorToAction

English

The action functor functorToAction F preserves monomorphisms.

Русский

Функтор действия сохраняет мономорфизмы.

LaTeX

$$$Functor.PreservesMonomorphisms (functorToAction F)$$$

Lean4

instance : ReflectsMonomorphisms (functorToAction F) :=
  reflectsMonomorphisms_of_faithful _

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

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

Разделы

Аффилиация

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