ComposableArrows — Mathlib

English

The assignment ComposableArrows(C) is the type of functors Fin(n+1) ⇒ C, for varying n, encoding the idea of a diagram of objects and morphisms in C of a fixed length n+1.

Русский

Обозначение ComposableArrows(C) описывает множество функторов Fin(n+1) ⇒ C для каждого n, задавая длину схемы объектов и морфизмов в C.

LaTeX

$$$\text{ComposableArrows}(C) = \{ n \mapsto (Fin(n+1) \to C) \}$$$

Lean4

/-- `ComposableArrows C n` is the type of functors `Fin (n + 1) ⥤ C`. -/
abbrev ComposableArrows (n : ℕ) :=
  Fin (n + 1) ⥤ C

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