Functors from the category of the ordered set ℕ

In this file, we provide a constructor Functor.ofSequence for functors ℕ ⥤ C which takes as an input a sequence of morphisms f : X n ⟶ X (n + 1) for all n : ℕ.

We also provide a constructor NatTrans.ofSequence for natural transformations between functors ℕ ⥤ C which allows to check the naturality condition only for morphisms n ⟶ n + 1.

theorem CategoryTheory.Functor.OfSequence.congr_f {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (i : ℕ) (j : ℕ) (h : i = j) : f i = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (f j) (CategoryTheory.eqToHom ⋯))

def CategoryTheory.Functor.OfSequence.map {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : ℕ → C} : ((n : ℕ) → X n ⟶ X (n + 1)) → (i j : ℕ) → i ≤ j → (X i ⟶ X j)

The morphism X i ⟶ X j obtained by composing morphisms of the form X n ⟶ X (n + 1) when i ≤ j.

Equations

• CategoryTheory.Functor.OfSequence.map x 0 0 = fun (x : 0 ≤ 0) => CategoryTheory.CategoryStruct.id (x✝ 0)
• CategoryTheory.Functor.OfSequence.map x 0 1 = fun (x_1 : 0 ≤ 1) => x 0
• CategoryTheory.Functor.OfSequence.map x 0 l.succ = fun (x_1 : 0 ≤ l + 1) => CategoryTheory.CategoryStruct.comp (x 0) (CategoryTheory.Functor.OfSequence.map (fun (n : ℕ) => x (n + 1)) 0 l ⋯)
• CategoryTheory.Functor.OfSequence.map x k.succ 0 = fun (a : k + 1 ≤ 0) => nomatch a
• CategoryTheory.Functor.OfSequence.map x k.succ l.succ = fun (x_1 : k + 1 ≤ l + 1) => CategoryTheory.Functor.OfSequence.map (fun (n : ℕ) => x (n + 1)) k l ⋯

theorem CategoryTheory.Functor.OfSequence.map_id {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (i : ℕ) : CategoryTheory.Functor.OfSequence.map f i i ⋯ = CategoryTheory.CategoryStruct.id (X i)

theorem CategoryTheory.Functor.OfSequence.map_le_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (i : ℕ) : CategoryTheory.Functor.OfSequence.map f i (i + 1) ⋯ = f i

theorem CategoryTheory.Functor.OfSequence.map_comp_assoc {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (i : ℕ) (j : ℕ) (k : ℕ) (hij : i ≤ j) (hjk : j ≤ k) {Z : C} (h : X k ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OfSequence.map f i k ⋯) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OfSequence.map f i j hij) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OfSequence.map f j k hjk) h)

theorem CategoryTheory.Functor.OfSequence.map_comp {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (i : ℕ) (j : ℕ) (k : ℕ) (hij : i ≤ j) (hjk : j ≤ k) : CategoryTheory.Functor.OfSequence.map f i k ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OfSequence.map f i j hij) (CategoryTheory.Functor.OfSequence.map f j k hjk)

@[simp]

theorem CategoryTheory.Functor.ofSequence_obj {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) : ∀ (a : ℕ), (CategoryTheory.Functor.ofSequence f).obj a = X a

def CategoryTheory.Functor.ofSequence {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) : CategoryTheory.Functor ℕ C

The functor ℕ ⥤ C constructed from a sequence of morphisms f : X n ⟶ X (n + 1) for all n : ℕ.

Equations

• CategoryTheory.Functor.ofSequence f = { obj := X, map := fun {i j : ℕ} (φ : i ⟶ j) => CategoryTheory.Functor.OfSequence.map f i j ⋯, map_id := ⋯, map_comp := ⋯ }

@[simp]

theorem CategoryTheory.Functor.ofSequence_map_homOfLE_succ {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (n : ℕ) : (CategoryTheory.Functor.ofSequence f).map (CategoryTheory.homOfLE ⋯) = f n

@[simp]

theorem CategoryTheory.NatTrans.ofSequence_app {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.Functor ℕ C} {G : CategoryTheory.Functor ℕ C} (app : (n : ℕ) → F.obj n ⟶ G.obj n) (naturality : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) (app (n + 1)) = CategoryTheory.CategoryStruct.comp (app n) (G.map (CategoryTheory.homOfLE ⋯))) (n : ℕ) : (CategoryTheory.NatTrans.ofSequence app naturality).app n = app n

def CategoryTheory.NatTrans.ofSequence {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] {F : CategoryTheory.Functor ℕ C} {G : CategoryTheory.Functor ℕ C} (app : (n : ℕ) → F.obj n ⟶ G.obj n) (naturality : ∀ (n : ℕ), CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) (app (n + 1)) = CategoryTheory.CategoryStruct.comp (app n) (G.map (CategoryTheory.homOfLE ⋯))) : F ⟶ G

Constructor for natural transformations F ⟶ G in ℕ ⥤ C which takes as inputs the morphisms F.obj n ⟶ G.obj n for all n : ℕ and the naturality condition only for morphisms of the form n ⟶ n + 1.

Equations

• CategoryTheory.NatTrans.ofSequence app naturality = { app := app, naturality := ⋯ }