instFaithfulActionFintypeCatAutFunctorFunctorToAction

Mathlib.CategoryTheory.Galois.Action

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

← MathLib Explorer

English

The functor functorToAction F is faithful.

Русский

Функтор functorToAction F верен (фиделен).

LaTeX

$$$\\text{Functor.Faithful} (functorToAction F)$$$

Lean4

instance : Functor.Faithful (functorToAction F) :=
  have : Functor.Faithful (functorToAction F ⋙ forget₂ _ FintypeCat) := inferInstanceAs <| Functor.Faithful F
  Functor.Faithful.of_comp (functorToAction F) (forget₂ _ FintypeCat)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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