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.

The duals of the above for functors ℕᵒᵖ ⥤ C are given by Functor.ofOpSequence and NatTrans.ofOpSequence.

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

def CategoryTheory.Functor.OfSequence.map {C : Type u_1} [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 : 0 ≤ 1) => x✝ 0
• CategoryTheory.Functor.OfSequence.map x✝ 0 l.succ = fun (x : 0 ≤ l + 1) => CategoryTheory.CategoryStruct.comp (x✝ 0) (CategoryTheory.Functor.OfSequence.map (fun (n : ℕ) => x✝ (n + 1)) 0 l ⋯)
• CategoryTheory.Functor.OfSequence.map x✝ n.succ 0 = fun (a : n + 1 ≤ 0) => nomatch a
• CategoryTheory.Functor.OfSequence.map x✝ k.succ l.succ = fun (x : 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} [Category.{u_2, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (i : ℕ) : map f i i ⋯ = CategoryStruct.id (X i)

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

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

theorem CategoryTheory.Functor.OfSequence.map_comp_assoc {C : Type u_1} [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) : CategoryStruct.comp (map f i k ⋯) h = CategoryStruct.comp (map f i j hij) (CategoryStruct.comp (map f j k hjk) h)

def CategoryTheory.Functor.ofSequence {C : Type u_1} [Category.{u_2, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) : 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_obj {C : Type u_1} [Category.{u_2, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (a✝ : ℕ) : (ofSequence f).obj a✝ = X a✝

@[simp]

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

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

@[simp]

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

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

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

Equations

• CategoryTheory.Functor.ofOpSequence f = (CategoryTheory.Functor.ofSequence fun (n : ℕ) => (f n).op).leftOp

@[simp]

theorem CategoryTheory.Functor.ofOpSequence_obj {C : Type u_1} [Category.{u_2, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X (n + 1) ⟶ X n) (X✝ : ℕᵒᵖ) : (ofOpSequence f).obj X✝ = X (Opposite.unop X✝)

@[simp]

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

def CategoryTheory.NatTrans.ofOpSequence {C : Type u_1} [Category.{u_2, u_1} C] {F G : Functor ℕᵒᵖ C} (app : (n : ℕ) → F.obj (Opposite.op n) ⟶ G.obj (Opposite.op n)) (naturality : ∀ (n : ℕ), CategoryStruct.comp (F.map (homOfLE ⋯).op) (app n) = CategoryStruct.comp (app (n + 1)) (G.map (homOfLE ⋯).op)) : 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.ofOpSequence app naturality = { app := fun (n : ℕᵒᵖ) => app (Opposite.unop n), naturality := ⋯ }

@[simp]

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