Category types question

Stream: new members

[Julia Scheaffer]

I have been trying to learn some category theory recently and I am trying to apply what I am learning in lean. Unfortunately, I am getting caught up on some type system issues with categories in lean. I defined a category I would like to work with, but I am having difficulties actually using these categories (I think) because they have the same types of objects but different types of morphisms.

import Mathlib.Tactic
import Mathlib.Logic.Function.Basic
import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Functor.Basic

universe u
variable {α : Type u}

def IteratesTo (f : α -> α) (a b : α) :=
  { i : Nat // f^[i] a = b }

def IteratesTo.cat (F : α -> α) : CategoryTheory.Category α where
  Hom := IteratesTo F
  id x := ⟨0, Function.iterate_zero_apply F x⟩
  comp f g := ⟨g.val + f.val, by
    rw [Function.iterate_add_apply, f.property, g.property]⟩
  id_comp _ := by ring_nf; rfl
  comp_id _ := by ring_nf; rfl
  assoc _ _ _ := by ring_nf

def f (n : Nat) : Nat := 2 * n
instance f.iterationCat : CategoryTheory.Category Nat := IteratesTo.cat f

def g (n : Nat) : Nat := 4 * n
instance g.iterationCat : CategoryTheory.Category Nat := IteratesTo.cat g

-- How do I create a functor between g.iterationCat and f.iterationCat?
-- It should map each object to the same value, and map each morphism to double it's previous value

-- My first attempt:
-- I need to specify the categories here, and they are inferred by default
example : CategoryTheory.Functor Nat Nat where
  obj := id
  map {X Y : Nat} (i : IteratesTo g X Y) : IteratesTo f (id X) (id Y) := sorry

This is my first attempt at trying to do category theory in lean with mathlib, so please let me know if I am defining my categories or functors incorrectly.

[Joël Riou]

Syntactically, when Lean sees α, it cannot know which category structure to use because it depends on F : α -> α. The standard procedure would be define a type synonym by def IteratesToCat (F : α -> α) := α and then define the category structure by instance : Category (IteratesToCat F) where .... Then, you may define a functor from IteratesToCat (fun (n : Nat) => 4 * n) to IteratesToCat (fun (n : Nat) => 2 * n).

[Julia Scheaffer]

That worked great, Thank you!

Here's the fully fixed code:

import Mathlib.Tactic
import Mathlib.Logic.Function.Basic
import Mathlib.CategoryTheory.Category.Basic
import Mathlib.CategoryTheory.Functor.Basic

universe u
variable {α : Type u}

def IteratesTo (f : α -> α) (a b : α) :=
  { i : Nat // f^[i] a = b }

def IteratesToCat (_ : α -> α) := α

instance IteratesTo.cat (F : α -> α) : CategoryTheory.Category (IteratesToCat F) where
  Hom := IteratesTo F
  id x := ⟨0, Function.iterate_zero_apply F x⟩
  comp f g := ⟨g.val + f.val, by
    rw [Function.iterate_add_apply, f.property, g.property]⟩
  id_comp _ := by ring_nf; rfl
  comp_id _ := by ring_nf; rfl
  assoc _ _ _ := by ring_nf

def f (n : Nat) : Nat := 2 * n
def g (n : Nat) : Nat := 4 * n

theorem double_f_eq_g : f^[2] = g := by
  funext x
  change f (f x) = g x
  dsimp only [f, g]
  ring_nf

example : CategoryTheory.Functor (IteratesToCat g) (IteratesToCat f) where
  obj := id
  map {X Y : Nat} (i : IteratesTo g X Y) : IteratesTo f X Y :=
    ⟨2 * i.val, by rw [Function.iterate_mul, double_f_eq_g, i.property]⟩
  map_comp _ _ := by
    dsimp [CategoryTheory.CategoryStruct.comp]
    ring_nf

[Aaron Liu]

probably the category it inferred is the preorder category, where there is a unique arrow a --> b iff a <= b