instPreservesFiniteProductsActionFintypeCatAutFunctorFunctorToAction

Mathlib.CategoryTheory.Galois.Action

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

← MathLib Explorer

English

The functor functorToAction F preserves finite products.

Русский

Функтор functorToAction F сохраняет конечные произведения.

LaTeX

$$$\\text{PreservesFiniteProducts} (functorToAction F)$$$

Lean4

noncomputable instance : PreservesFiniteProducts (functorToAction F) :=
  ⟨fun _ ↦
    Action.preservesLimitsOfShape_of_preserves (functorToAction F)
      (inferInstanceAs <| PreservesLimitsOfShape (Discrete _) F)⟩

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

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

Разделы

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

Аффилиация

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