ofSequence — Mathlib

English

The functor sending n to X(n) with maps given by the sequence f defines a functor ℕ ⥤ C.

Русский

Функтор, отправляющий n ↦ X(n) с отображениями, заданными последовательностью f, определяет функтор ℕ ⥤ C.

LaTeX

$$$\\mathrm{ofSequence} : \\mathbb{N} \\to C$ with $\\mathrm{map}$ given by OfSequence.map$.$$

Lean4

/-- The functor `ℕ ⥤ C` constructed from a sequence of
morphisms `f : X n ⟶ X (n + 1)` for all `n : ℕ`. -/
@[simps obj]
def ofSequence : ℕ ⥤ C where
  obj := X
  map {i j} φ := OfSequence.map f i j (leOfHom φ)
  map_id i := OfSequence.map_id f i
  map_comp {i j k} α β := OfSequence.map_comp f i j k (leOfHom α) (leOfHom β)

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