functor — Mathlib

English

The nth functor is defined recursively by MultiInd.functor 0 = Id and MultiInd.functor (n+1) = MultiInd.functor n ⋙ I R G.

Русский

N-й функтор задаётся рекурсивно: MultiInd.functor 0 = Id, MultiInd.functor (n+1) = MultiInd.functor n ∘ I R G.

LaTeX

$$$\\text{functor} : \\mathbb{N} \\to \\text{Action}(\\text{TopModuleCat } R) G \\to \\text{Action}(\\text{TopModuleCat } R) G,\\; 0\\mapsto 𝟭,\\; n+1\\mapsto (\\text{functor } n)\\;⋙\\; I\\ R\\ G$$$

Lean4

/-- The n-th functor taking `M` to `C(G, C(G,...,C(G, M)))` (with n `G`s).
These functors form a complex, see `MultiInd.complex`. -/
def functor : ℕ → Action (TopModuleCat R) G ⥤ Action (TopModuleCat R) G
  | 0 => 𝟭 _
  | n + 1 => functor n ⋙ I R G

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