summand — Mathlib

English

On a chain complex K, the summand associated to an index A in Δ is the object K.X A.1.len, i.e., the component at the length of A. This expresses how Γ₀ builds a simplicial object by assembling these pieces.

Русский

Для пары K и индекса A в Δ суммация β содержит компоненту K.X A.1.len, т.е. объект на длине A. Это часть конструирования Γ₀, собирая эти кусочки в единое симплициальное множество.

LaTeX

$$$\operatorname{summand}(Δ,A) := K.X(A.1).len$$$

Lean4

/-- In the definition of `(Γ₀.obj K).obj Δ` as a direct sum indexed by `A : Splitting.IndexSet Δ`,
the summand `summand K Δ A` is `K.X A.1.len`. -/
def summand (Δ : SimplexCategoryᵒᵖ) (A : Splitting.IndexSet Δ) : C :=
  K.X A.1.unop.len

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