## Stream: maths

### Topic: composing a list of functions

#### Kenny Lau (Aug 03 2020 at 16:59):

Can we compose a list of functions? Would this have any use?

#### Kenny Lau (Aug 03 2020 at 16:59):

Currently we can only compose two functions

#### Kenny Lau (Aug 03 2020 at 16:59):

and n times if the domain and codomain happen to be the same

#### Adam Topaz (Aug 03 2020 at 16:59):

Cant you just do a list.fold with \circ, or something like this?

#### Jalex Stark (Aug 03 2020 at 17:00):

what's the type of the list?

#### Kenny Lau (Aug 03 2020 at 17:11):

Jalex Stark said:

what's the type of the list?

exactly

#### Adam Topaz (Aug 03 2020 at 17:21):

There must be something like heterogeneous lists right?

#### Adam Topaz (Aug 03 2020 at 17:21):

And it should be traversable so you should be able to fold over it.

#### Adam Topaz (Aug 03 2020 at 17:24):

Maybe traversable isn't the right term here....

#### Mario Carneiro (Aug 03 2020 at 18:01):

I tried writing a heterogeneous list type, and decided that it wouldn't actually serve the purposes people want for it very well

#### Mario Carneiro (Aug 03 2020 at 18:02):

It's better to just use iterated prod if you want a strongly typed heterogeneous list

#### Mario Carneiro (Aug 03 2020 at 18:04):

For composing lists of functions, the solution is to use comp several times

#### Mario Carneiro (Aug 03 2020 at 18:05):

If you want a type erased heterogeneous list you can use list (Sigma A, A) but I'm not really sure what this would be good for

#### Kenny Lau (Aug 03 2020 at 19:34):

ok maybe I should talk about a potential use case to make this more clear

#### Kenny Lau (Aug 03 2020 at 19:35):

I want to be able to state (and certainly prove) the statement that a functor from [n] = {0 -> 1 -> ... -> n} to any category C is the same as n composable morphisms in C

#### Kenny Lau (Aug 03 2020 at 19:35):

Mario Carneiro said:

For composing lists of functions, the solution is to use comp several times

do you mean that if we have 3 functions then we use comp twice? this sounds like it can't work for an arbitrary n, but I might be misunderstanding your suggestion

#### Adam Topaz (Aug 03 2020 at 19:38):

Are you defining the nerve?

indeed!

Cool!

#### Adam Topaz (Aug 03 2020 at 19:39):

Presumably you can define the simplicial set by induction on n, no?

#### Kenny Lau (Aug 03 2020 at 19:39):

you don't need induction right

#### Kenny Lau (Aug 03 2020 at 19:40):

def nerve (C) := \la n, [n] \func C

(pseudocode)

#### Adam Topaz (Aug 03 2020 at 19:40):

Yeah, sure, but I want to exploit the fact that this simplicial set has some horn filling properties :)

#### Kenny Lau (Aug 03 2020 at 19:41):

what's horn filling properties and how does defining nerve inductively exploits that?

#### Reid Barton (Aug 03 2020 at 19:43):

It seems to me like you want to prove that [n] is the free category on the graph 0 -> 1 -> ... -> n

#### Kenny Lau (Aug 03 2020 at 19:45):

defining constructing the free category sounds like a cool project

#### Reid Barton (Aug 03 2020 at 19:47):

https://github.com/semorrison/lean-category-theory/blob/master/src/category_theory/graphs/category.lean

aha, inductive

#### Kenny Lau (Aug 03 2020 at 19:49):

can one even state "a list of composable morphisms"? it might have to be a type with nat.rec again, like I made before

#### Kenny Lau (Aug 03 2020 at 19:50):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Canonical.20inductive.20types.20with.200.2C1.2C2.2C3.2C4.20terms/near/204653480

#### Reid Barton (Aug 03 2020 at 19:50):

Isn't that what morphism_path in the link above is?

I guess it is

#### Reid Barton (Aug 03 2020 at 19:51):

Another option is trees of (formal) compositions modulo associativity

& unitality

#### Kenny Lau (Aug 03 2020 at 19:52):

this is syntax vs semantics again: I don't know how to put it into words, but it's sort of the difference between saying that the inductive implementation is list vs a function from fin n is a list

#### Kenny Lau (Aug 03 2020 at 19:52):

if it quacks like a list, then it's a list

#### Reid Barton (Aug 03 2020 at 19:52):

right, so there's a second presentation of categories which doesn't use dependent types but rather a type of objects and a type of (all) morphisms

#### Reid Barton (Aug 03 2020 at 19:53):

then you could consider a list of morphisms together with a bunch of equations that say the intermediate objects line up

#### Reid Barton (Aug 03 2020 at 19:53):

I suspect if you consider the nerve for long enough, you'll be sort of forced into this perspective anyways

#### Kenny Lau (Aug 03 2020 at 19:54):

I keep having the illusion that objects have some "internal representation", that the inductive and the function from fin n have some sort of difference

#### Adam Topaz (Aug 03 2020 at 20:12):

Mathlib should really have categories internal to other categories :)

#### Bhavik Mehta (Aug 03 2020 at 20:13):

https://github.com/b-mehta/topos/blob/master/src/internal_category%20copy.lean Feel free to tidy this and PR it if you want :)

#### Bhavik Mehta (Aug 03 2020 at 20:13):

i'm pretty sure it compiles on the latest mathlib

#### Kenny Lau (Aug 03 2020 at 20:15):

@Bhavik Mehta what's an example of an internal category?

#### Adam Topaz (Aug 03 2020 at 20:16):

A category is an internal category in types :)

#### Adam Topaz (Aug 03 2020 at 20:16):

(At least in the way Reid mentioned above)

#### Kenny Lau (Aug 03 2020 at 20:16):

apart from that, I guess

#### Reid Barton (Aug 03 2020 at 20:17):

a two-term chain complex is a category internal to abelian groups

#### Reid Barton (Aug 03 2020 at 20:25):

normally though you'd look at categories internal to say topological spaces

#### Adam Topaz (Aug 03 2020 at 22:08):

@Kenny Lau In case you find this helpful:

import category_theory.category
import category_theory.arrow

open category_theory

variables {C : Type*} [category C]

def composable_things {n : ℕ} : (fin (n+1) → C) → (fin n → arrow C) → Prop :=
nat.rec_on n
(λ _ _, true)
(λ n h f g, (h (f ∘ fin.succ) (g ∘ fin.succ)) ∧ (g 0).left = f 0) -- wrong


#### Adam Topaz (Aug 03 2020 at 22:09):

Wait, I may have gotten the fin.succ's wrong.

#### Adam Topaz (Aug 03 2020 at 22:10):

This is probably better:

def composable_things {n : ℕ} : (fin (n+1) → C) → (fin n → arrow C) → Prop :=
nat.rec_on n
(λ _ _, true)
(λ n h f g, (h (f ∘ fin.succ) (g ∘ fin.succ)) ∧ (g 0).right = f (fin.succ 0))


#### Kenny Lau (Aug 04 2020 at 05:21):

we will certainly run into eq.rec hell if we do this

#### Kenny Lau (Aug 04 2020 at 05:21):

but there seems no other way

#### Scott Morrison (Aug 04 2020 at 05:28):

I've used something like

inductive composable_morphisms'
(V : Type u) [category.{v} V] : V → Type (max u v)
| zero [] : Π X, composable_morphisms' X
| cons : Π {X Y : V} (f : X ⟶ Y) (C : composable_morphisms' Y), composable_morphisms' X

def composable_morphisms := Σ (X : V), (composable_morphisms' V X)


#### Kenny Lau (Aug 04 2020 at 05:31):

yeah that sounds like a good idea

#### Scott Morrison (Aug 04 2020 at 06:18):

might be better to parameterise by both endpoints, for the sake of composition

#### Kenny Lau (Aug 04 2020 at 06:25):

@Scott Morrison this is what I have now, in my livestream:

universe u

/-- A list of composable functions -/
inductive list_fun (α : Type u) : Type u → Type (u+1)
| nil : list_fun α
| cons : Π {β γ}, (β → γ) → list_fun β → list_fun γ

namespace list_fun

#check nil
#check cons (coe : ℕ → ℤ) $cons (int.nat_abs) nil /-- The composition of a list of composable functions. Set up so that comp (f :: g :: nil) = f ∘ g. -/ def comp {α} : Π {β}, list_fun α β → α → β | _ nil := id | _ (cons f L) := f ∘ L.comp @[simp] lemma comp_nil (α) : (nil : list_fun α α).comp = id := rfl @[simp] lemma comp_cons {α β γ} (f : β → γ) (L : list_fun α β) : (cons f L).comp = f ∘ L.comp := rfl /-- Concatenation of two lists of composable functions. -/ def append {α β} : Π {γ}, list_fun β γ → list_fun α β → list_fun α γ | _ nil L₂ := L₂ | _ (cons f L₁) L₂ := cons f (append L₁ L₂) @[simp] lemma comp_append {α β} : ∀ {γ} (L₁ : list_fun β γ) (L₂ : list_fun α β), (L₁.append L₂).comp = L₁.comp ∘ L₂.comp | _ nil L₂ := rfl | _ (cons f L₁) L₂ := congr_arg ((∘) f)$ comp_append L₁ L₂

end list_fun


#### Scott Morrison (Aug 04 2020 at 06:27):

Looks great, except that you could make it category polymorphic trivially, and get the current behaviour substituting Type for C. :-)

right

#### Kenny Lau (Aug 04 2020 at 06:27):

where in the category library should this go?

#### Scott Morrison (Aug 04 2020 at 06:28):

I guess comp_append would be harder.

(deleted)

#### Kenny Lau (Aug 04 2020 at 06:28):

but I just proved comp_append

#### Kenny Lau (Aug 04 2020 at 06:28):

oh, you mean for categories

#### Scott Morrison (Aug 04 2020 at 06:29):

Yes. Harder, but still easy. :-)

#### Scott Morrison (Aug 04 2020 at 06:29):

Just make a new file in category_theory/?

#### Scott Morrison (Aug 04 2020 at 06:29):

with the same name as lift_fun, or whatever you call it?

#### Kenny Lau (Aug 04 2020 at 06:30):

I'll add TODO: port every lemma about list ever (except the permutation part!)

#### Kenny Lau (Aug 04 2020 at 06:30):

comp list.repeat = nat.iterate!

#### Kenny Lau (Aug 04 2020 at 06:31):

oh right, and prove that this is the same as a functor from fin n+1 to C

#### Scott Morrison (Aug 04 2020 at 06:41):

and the equivalence with the subtype of list (arrow C) satisfying some pairwise condition

#### Kenny Lau (Aug 04 2020 at 06:46):

if I define cons f L then I lose analogy with category; if I define cons L f then I lose analogy with functions...

#### Kenny Lau (Aug 04 2020 at 06:46):

the category theory composition is the opposite of functions iirc

#### Scott Morrison (Aug 04 2020 at 06:47):

Shall we switch the order in category_theory/? :-)

#### Scott Morrison (Aug 04 2020 at 06:48):

I'm not sure it matters particularly; just pick whichever order feels most ergonomic locally.

#### Kenny Lau (Aug 04 2020 at 06:50):

I guess we want (cons f L).comp = f >> L?

#### Kenny Lau (Aug 04 2020 at 07:00):

you know what, I'll just make it so that (cons f L).comp = L.comp >> f, who cares

#### Kenny Lau (Aug 04 2020 at 07:00):

just to make the inductive require one argument less

#### Kenny Lau (Aug 04 2020 at 07:01):

@Scott Morrison is this ok?

#### Kenny Lau (Aug 04 2020 at 07:01):

import category_theory.category

universes v u

namespace category_theory

variables {C : Type u} [category.{v} C]

/-- A list of composable functions -/
inductive list_fun (X : C) : C → Type (max u v)
| nil : list_fun X
| cons : Π {Y Z}, (Y ⟶ Z) → list_fun Y → list_fun Z

namespace list_fun

/-- The composition of a list of composable functions.
Set up so that comp (f :: g :: nil) = (𝟙 ≫ g) ≫ f. -/
def comp {X : C} : Π {Y}, list_fun X Y → (X ⟶ Y)
| _ nil := 𝟙 X
| _ (cons f L) := L.comp ≫ f

end list_fun


#### Kenny Lau (Aug 04 2020 at 07:08):

turns out comp_append wasn't hard:

/-
Authors: Kenny Lau
-/

import category_theory.category

/-!
# Lists of Composable Morphisms

In this file we define lists of composable morphisms, and their composition.

We also show that a list of composable morphism is the same as a functor from [n]
(the category 0 ⟶ 1 ⟶ ... ⟶ n) to the category.

## Main Definitions

- list_fun X Y where X, Y : C for some category C is a list of composable morphisms starting
from X and ending at Y.

- list_fun.comp L where L : list_fun X Y returns the composition as a morphism X ⟶ Y.

-/

-- TODO: port every lemma about list ever

universes v u

namespace category_theory

variables {C : Type u} [category.{v} C]

/-- A list of composable functions -/
inductive list_fun (X : C) : C → Type (max u v)
| nil : list_fun X
| cons : Π {Y Z}, (Y ⟶ Z) → list_fun Y → list_fun Z

notation a :: b := list_fun.cons a b

namespace list_fun

/-- The composition of a list of composable functions.
Set up so that comp (f :: g :: nil) = (𝟙 ≫ g) ≫ f. -/
def comp {X : C} : Π {Y}, list_fun X Y → (X ⟶ Y)
| _ nil := 𝟙 X
| _ (f :: L) := L.comp ≫ f

@[simp] lemma comp_nil (X : C) : (nil : list_fun X X).comp = 𝟙 X := rfl
@[simp] lemma comp_cons {X Y Z : C} (f : Y ⟶ Z) (L : list_fun X Y) :
(cons f L).comp = L.comp ≫ f := rfl

/-- Concatenation of two lists of composable functions. -/
def append {X Y : C} : Π {Z}, list_fun Y Z → list_fun X Y → list_fun X Z
| _ nil         L₂ := L₂
| _ (cons f L₁) L₂ := cons f (append L₁ L₂)

@[simp] lemma nil_append {X Y : C} (L : list_fun X Y) : nil.append L = L := rfl
@[simp] lemma cons_append {X Y Z W : C} (f : Z ⟶ W) (L₁ : list_fun Y Z) (L₂ : list_fun X Y) :
(cons f L₁).append L₂ = cons f (L₁.append L₂) := rfl

@[simp] lemma comp_append {X Y : C} : ∀ {Z} (L₁ : list_fun Y Z) (L₂ : list_fun X Y),
(L₁.append L₂).comp = L₂.comp ≫ L₁.comp
| _ nil         L₂ := by rw [comp_nil, nil_append, category.comp_id]
| _ (cons f L₁) L₂ := by rw [cons_append, comp_cons, comp_cons, comp_append, category.assoc]

end list_fun

end category_theory


#### Scott Morrison (Aug 04 2020 at 07:10):

presumably rename list_fun to list_hom?

done

#### Kenny Lau (Aug 04 2020 at 07:17):

@Scott Morrison what sort of structure does list_hom form, given append and map?

#### Kenny Lau (Aug 04 2020 at 07:17):

def map {X : C} : Π {Y : C}, list_hom X Y → list_hom (F.obj X) (F.obj Y)


#### Scott Morrison (Aug 04 2020 at 07:18):

I think list_hom is just the free category on a category_struct.

#### Scott Morrison (Aug 04 2020 at 07:19):

so maybe you could set it up as a functor from Graph to Cat, adjoint to the forgetful functor?

#### Kenny Lau (Aug 04 2020 at 07:35):

is graph in mathlib?

@Scott Morrison

#### Kevin Buzzard (Aug 04 2020 at 07:37):

Even if someone had "put graphs in mathlib" the chances that they would be the kind of graph you wanted is i guess low

#### Kenny Lau (Aug 04 2020 at 07:39):

structure functor (C : Type u₁) [category.{v₁} C] (D : Type u₂) [category.{v₂} D] :
Type (max v₁ v₂ u₁ u₂) :=
(obj []    : C → D)
(map       : Π {X Y : C}, (X ⟶ Y) → ((obj X) ⟶ (obj Y)))
(map_id'   : ∀ (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(map_comp' : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), map (f ≫ g) = (map f) ≫ (map g) . obviously)


#### Kenny Lau (Aug 04 2020 at 07:40):

you don't need C and D to be a category! ;)

#### Kenny Lau (Aug 04 2020 at 07:42):

oh what am I doing, generalizing category theory itself

#### Kenny Lau (Aug 04 2020 at 07:45):

/-
Authors: Kenny Lau
-/

import category_theory.functor_category

/-!
# Lists of Composable Morphisms

In this file we define lists of composable morphisms, and their composition.

We also show that a list of composable morphism is the same as a functor from [n]
(the category 0 ⟶ 1 ⟶ ... ⟶ n) to the category.

## Main Definitions

- list_hom X Y where X, Y : C for some category C is a list of composable morphisms starting
from X and ending at Y.

- list_hom.comp L where L : list_hom X Y returns the composition as a morphism X ⟶ Y.

-/

-- TODO: port every lemma about list ever

universes v₁ v₂ u₁ u₂

namespace category_theory

variables {C : Type u₁} {D : Type u₂}

/-- A list of composable functions -/
inductive list_hom [has_hom.{v₁} C] (X : C) : C → Type (max u₁ v₁)
| nil  : list_hom X
| cons : Π {Y Z}, (Y ⟶ Z) → list_hom Y → list_hom Z

namespace list_hom

notation a :: b := cons a b

section has_hom

variables [has_hom.{v₁} C] [has_hom.{v₂} D]

/-- Concatenation of two lists of composable functions. -/
def append {X Y : C} : Π {Z}, list_hom Y Z → list_hom X Y → list_hom X Z
| _ nil       L₂ := L₂
| _ (f :: L₁) L₂ := f :: (append L₁ L₂)

notation a ++ b := append a b

@[simp] lemma nil_append {X Y : C} (L : list_hom X Y) : nil ++ L = L := rfl
@[simp] lemma cons_append {X Y Z W : C} (f : Z ⟶ W) (L₁ : list_hom Y Z) (L₂ : list_hom X Y) :
(f :: L₁) ++ L₂ = f :: (L₁ ++ L₂) := rfl

end has_hom

section category_struct

variables [category_struct.{v₁} C] [category_struct.{v₂} D]

/-- The composition of a list of composable functions.
Set up so that comp (f :: g :: nil) = (𝟙 ≫ g) ≫ f. -/
def comp {X : C} : Π {Y}, list_hom X Y → (X ⟶ Y)
| _ nil      := 𝟙 X
| _ (f :: L) := L.comp ≫ f

@[simp] lemma comp_nil (X : C) : (nil : list_hom X X).comp = 𝟙 X := rfl
@[simp] lemma comp_cons {X Y Z : C} (f : Y ⟶ Z) (L : list_hom X Y) :
(f :: L).comp = L.comp ≫ f := rfl

end category_struct

section category

variables [category.{v₁} C] [category.{v₂} D]

@[simp] lemma comp_append {X Y : C} : ∀ {Z} (L₁ : list_hom Y Z) (L₂ : list_hom X Y),
(L₁.append L₂).comp = L₂.comp ≫ L₁.comp
| _ nil       L₂ := by rw [comp_nil, nil_append, category.comp_id]
| _ (f :: L₁) L₂ := by rw [cons_append, comp_cons, comp_cons, comp_append, category.assoc]

variables (F : C ⥤ D)

def map {X : C} : Π {Y : C}, list_hom X Y → list_hom (F.obj X) (F.obj Y)
| _ nil      := nil
| _ (f :: L) := F.map f :: L.map

@[simp] lemma map_nil {X : C} : (nil : list_hom X X).map F = nil := rfl
@[simp] lemma map_cons {X Y Z : C} (f : Y ⟶ Z) (L : list_hom X Y) :
(f :: L).map F = F.map f :: L.map F := rfl

@[simp] lemma map_append {X Y : C} : ∀ {Z} (L₁ : list_hom Y Z) (L₂ : list_hom X Y),
(L₁ ++ L₂).map F = L₁.map F ++ L₂.map F
| _ nil       L₂ := rfl
| _ (f :: L₁) L₂ := congr_arg (cons (F.map f)) \$ map_append L₁ L₂

end category

end list_hom

end category_theory


#### Kenny Lau (Aug 04 2020 at 07:45):

"maximal generality"

#### Kenny Lau (Aug 04 2020 at 07:47):

so Func([n], -) is a functor $\mathsf{Cat} \to \mathsf{Type}$?

aha

#### Kenny Lau (Aug 04 2020 at 07:47):

then list_hom would also have to be one...?

#### Jalex Stark (Aug 04 2020 at 14:44):

Kevin Buzzard said:

Even if someone had "put graphs in mathlib" the chances that they would be the kind of graph you wanted is i guess low

indeed, the most recent PR attempting to put graphs in mathlib implements loopless graphs, but for the category Graph you really ought to allow loops.

#### Jalex Stark (Aug 04 2020 at 14:50):

this makes it, uh, "cartesian closed" might be the right word? The graph 1 with one vertex and one edge is a terminal object, and this terminal object gives rise to a sensible notion of point. e.g. there is a good bijection between Hom(1, G^H) and Hom(H, G)

#### Adam Topaz (Aug 04 2020 at 14:55):

Mathlib already has something like a (pre-)graph (whatever that means):

import category_theory.category
open category_theory
variables (G : Type*) [has_hom G]


#### Adam Topaz (Aug 04 2020 at 14:57):

It's certainly possible to take such a $G$ and construct the free category associated to it.

Last updated: May 14 2021 at 18:28 UTC