obj₂ — Mathlib

English

The Γ₀ construction assigns to a chain complex K and a simplex Δ the direct sum, over all A in the index set of Δ, of the summands of KΔA, producing an object in C.

Русский

Конструкция Γ₀.Obj.obj₂ каждому комплексe K и простому Δ ставит прямую сумму по всем A из индексов Δ и суммам KΔA, получая новый объект в C.

LaTeX

$$$$ \text{obj}_2(K, \Delta) = \bigoplus_{A \in \mathrm{Splitting.IndexSet}(\Delta)} \mathrm{summand}(K, \Delta, A) $$$$

Lean4

/-- The functor `Γ₀` sends a chain complex `K` to the simplicial object which
sends `Δ` to the direct sum of the objects `summand K Δ A` for all `A : Splitting.IndexSet Δ` -/
def obj₂ (K : ChainComplex C ℕ) (Δ : SimplexCategoryᵒᵖ) [HasFiniteCoproducts C] : C :=
  ∐ fun A : Splitting.IndexSet Δ => summand K Δ A

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