ofOpSequence — Mathlib

English

From a sequence of morphisms f(n+1) ⟶ f(n) in C, form a functor from the opposite of Nat to C by reversing the direction.

Русский

Из последовательности морфизмов f(n+1) ⟶ f(n) в C образуется функтор из противоположного Nat в C, разворачивая направление.

LaTeX

$$$\\text{ofOpSequence} : \\mathbb{N}^{op} ⥤ C$ with $\\text{map}$ given by $(f(n)^{op})$-based construction.$$

Lean4

/-- The functor `ℕᵒᵖ ⥤ C` constructed from a sequence of
morphisms `f : X (n + 1) ⟶ X n` for all `n : ℕ`. -/
@[simps! obj]
def ofOpSequence : ℕᵒᵖ ⥤ C :=
  (ofSequence (fun n ↦ (f n).op)).leftOp

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