instSymmetricCategory — Mathlib

English

If V is symmetric, then Action V G is symmetric; the symmetric structure is transported from V via the forgetful functor.

Русский

Если V симметрична, то Action V G симметрична; симметрическая структура переносится через забывающий функтор.

LaTeX

$$$\text{SymmetricCategory}(\mathrm{Action}(V,G))$$$

Lean4

instance [SymmetricCategory V] : SymmetricCategory (Action V G) :=
  symmetricCategoryOfFaithful (Action.forget V G)

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