chainsFunctor — Mathlib

English

There is a functor from Rep k G to ChainComplex(k) that assigns to A the inhomogeneous chains complex and to morphisms φ the induced chains maps at level n.

Русский

Существует функтор от Rep k G к цепному комплексному пространству, сопоставляющий A комплекс ин-гомогенных цепей, а морфизм φ — индуцированные отображения цепей на уровне n.

LaTeX

$$$ \text{chainsFunctor}: \mathrm{Rep}\;k\;G \to \mathrm{ChainComplex}(\mathrm{ModuleCat}\;k)\;\mathbb{N} $$$

Lean4

/-- The functor sending a representation to its complex of inhomogeneous chains. -/
@[simps]
noncomputable def chainsFunctor : Rep k G ⥤ ChainComplex (ModuleCat k) ℕ
    where
  obj A := inhomogeneousChains A
  map f := chainsMap (MonoidHom.id _) f
  map_id _ := chainsMap_id
  map_comp φ ψ := chainsMap_comp (MonoidHom.id G) (MonoidHom.id G) φ ψ

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