exteriorPower — Mathlib

English

For a ring R, the nth exterior power defines a functor on ModuleCat R sending M to its nth exterior power ∧^n M.

Русский

Для кольца R и натурального n существует канонический функтор на ModuleCat R, отправляющий модуль M в его n-ю внешнюю степень ∧^n M и отображающий f в ∧^n f.

LaTeX

$$$F_n: \\mathrm{Mod}_R \\to \\mathrm{Mod}_R$, $F_n(M) = \\bigwedge^n M$, $F_n(f) = \\bigwedge^n f$.$$

Lean4

/-- The exterior power of an object in `ModuleCat R`. -/
def exteriorPower (M : ModuleCat.{v} R) (n : ℕ) : ModuleCat.{max u v} R :=
  ModuleCat.of R
    (⋀[R]^n M)
      -- this could be an abbrev, but using a def eases automation

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