Functors out of the natural numbers from step data

A sequence of objects and one-step transition morphisms assembles into a functor from ℕ — the shape of the Key Lemma's δ-multiplication colimit. The map on an arbitrary inequality is defined by recursion on its length, with the composition law proved once and the one-step computation exposed as a simp lemma.

noncomputable def RS.chainMap {D : Type u} [CategoryTheory.Category.{v, u} D] (B : ℕ → D) (δ : (n : ℕ) → B n ⟶ B (n + 1)) {m n : ℕ} : m ≤ n → (B m ⟶ B n)

The morphism of a chain along an inequality, by recursion on its length.

Equations

• RS.chainMap B δ h = Nat.leRecOn h (fun {k : ℕ} (f : B m ⟶ B k) => CategoryTheory.CategoryStruct.comp f (δ k)) (CategoryTheory.CategoryStruct.id (B m))

@[simp]

theorem RS.chainMap_self {D : Type u} [CategoryTheory.Category.{v, u} D] (B : ℕ → D) (δ : (n : ℕ) → B n ⟶ B (n + 1)) (n : ℕ) : chainMap B δ ⋯ = CategoryTheory.CategoryStruct.id (B n)

theorem RS.chainMap_succ_of_le {D : Type u} [CategoryTheory.Category.{v, u} D] (B : ℕ → D) (δ : (n : ℕ) → B n ⟶ B (n + 1)) {m n : ℕ} (h : m ≤ n) (h' : m ≤ n + 1) : chainMap B δ h' = CategoryTheory.CategoryStruct.comp (chainMap B δ h) (δ n)

@[simp]

theorem RS.chainMap_le_succ {D : Type u} [CategoryTheory.Category.{v, u} D] (B : ℕ → D) (δ : (n : ℕ) → B n ⟶ B (n + 1)) (n : ℕ) : chainMap B δ ⋯ = δ n

theorem RS.chainMap_trans {D : Type u} [CategoryTheory.Category.{v, u} D] (B : ℕ → D) (δ : (n : ℕ) → B n ⟶ B (n + 1)) {l m n : ℕ} (h₁ : l ≤ m) (h₂ : m ≤ n) : chainMap B δ ⋯ = CategoryTheory.CategoryStruct.comp (chainMap B δ h₁) (chainMap B δ h₂)

noncomputable def RS.chainFunctor {D : Type u} [CategoryTheory.Category.{v, u} D] (B : ℕ → D) (δ : (n : ℕ) → B n ⟶ B (n + 1)) : CategoryTheory.Functor ℕ D

The functor out of ℕ assembled from objects and one-step transitions.

Equations

• RS.chainFunctor B δ = { obj := B, map := fun {X Y : ℕ} (f : X ⟶ Y) => RS.chainMap B δ ⋯, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem RS.chainFunctor_obj {D : Type u} [CategoryTheory.Category.{v, u} D] (B : ℕ → D) (δ : (n : ℕ) → B n ⟶ B (n + 1)) (n : ℕ) : (chainFunctor B δ).obj n = B n

@[simp]

theorem RS.chainFunctor_map_le_succ {D : Type u} [CategoryTheory.Category.{v, u} D] (B : ℕ → D) (δ : (n : ℕ) → B n ⟶ B (n + 1)) (n : ℕ) : (chainFunctor B δ).map (CategoryTheory.homOfLE ⋯) = δ n