functor — Mathlib

English

There is a functor ModuleCat R ⥤ ModuleCat R sending M to its nth exterior power with action on morphisms by map f n.

Русский

Существует функтор ModuleCat R ⥤ ModuleCat R, отправляющий каждый модуль M на его n-ю внешнюю степень, а отображения f → map f n.

LaTeX

$$functor (n) : ModuleCat.{v} R ⥤ ModuleCat.{max u v} R with obj M := M.exteriorPower n and map f := map f n$$

Lean4

/-- The functor `ModuleCat R ⥤ ModuleCat R` which sends a module to its
`n`th exterior power. -/
@[simps]
noncomputable def functor (n : ℕ) : ModuleCat.{v} R ⥤ ModuleCat.{max u v} R
    where
  obj M := M.exteriorPower n
  map f := map f n

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