composing a list of functions

Stream: maths

[Kenny Lau]

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

[Kenny Lau]

Currently we can only compose two functions

[Kenny Lau]

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

[Adam Topaz]

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

[Jalex Stark]

what's the type of the list?

[Kenny Lau]

Jalex Stark said:

what's the type of the list?

exactly

[Adam Topaz]

There must be something like heterogeneous lists right?

[Adam Topaz]

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

[Adam Topaz]

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

[Reid Barton]

https://hackage.haskell.org/package/thrist-0.4/docs/Data-Thrist.html
https://ncatlab.org/nlab/show/free+category

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Kenny Lau]

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]

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]

Are you defining the nerve?

[Kenny Lau]

indeed!

[Adam Topaz]

Cool!

[Adam Topaz]

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

[Kenny Lau]

you don't need induction right

[Kenny Lau]

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

[Kenny Lau]

(pseudocode)

[Adam Topaz]

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

[Kenny Lau]

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

[Reid Barton]

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

[Kenny Lau]

defining constructing the free category sounds like a cool project

[Reid Barton]

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

[Kenny Lau]

aha, inductive

[Kenny Lau]

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]

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

[Reid Barton]

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

[Kenny Lau]

I guess it is

[Reid Barton]

Another option is trees of (formal) compositions modulo associativity

[Reid Barton]

& unitality

[Kenny Lau]

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]

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

[Reid Barton]

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]

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

[Reid Barton]

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

[Kenny Lau]

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]

Mathlib should really have categories internal to other categories :)

[Bhavik Mehta]

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]

i'm pretty sure it compiles on the latest mathlib

[Kenny Lau]

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

[Adam Topaz]

A category is an internal category in types :)

[Adam Topaz]

(At least in the way Reid mentioned above)

[Kenny Lau]

apart from that, I guess

[Reid Barton]

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

[Reid Barton]

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

[Adam Topaz]

@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]

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

[Adam Topaz]

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]

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

[Kenny Lau]

but there seems no other way

[Scott Morrison]

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]

yeah that sounds like a good idea

[Scott Morrison]

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

[Kenny Lau]

@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]

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

[Kenny Lau]

right

[Kenny Lau]

where in the category library should this go?

[Scott Morrison]

I guess comp_append would be harder.

[Scott Morrison]

(deleted)

[Kenny Lau]

but I just proved comp_append

[Kenny Lau]

oh, you mean for categories

[Scott Morrison]

Yes. Harder, but still easy. :-)

[Scott Morrison]

Just make a new file in category_theory/?

[Scott Morrison]

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

[Kenny Lau]

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

[Kenny Lau]

comp list.repeat = nat.iterate!

[Kenny Lau]

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

[Scott Morrison]

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

[Kenny Lau]

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]

the category theory composition is the opposite of functions iirc

[Scott Morrison]

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

[Scott Morrison]

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

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

just to make the inductive require one argument less

[Kenny Lau]

@Scott Morrison is this ok?

[Kenny Lau]

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]

turns out comp_append wasn't hard:

/-
Copyright (c) 2020 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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]

presumably rename list_fun to list_hom?

[Kenny Lau]

done

[Kenny Lau]

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

[Kenny Lau]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Kenny Lau]

is graph in mathlib?

[Kenny Lau]

@Scott Morrison

[Kevin Buzzard]

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]

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]

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

[Kenny Lau]

oh what am I doing, generalizing category theory itself

[Kenny Lau]

/-
Copyright (c) 2020 Kenny Lau. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
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]

"maximal generality"

[Kenny Lau]

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

[Kenny Lau]

aha

[Kenny Lau]

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

[Jalex Stark]

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]

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]

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]

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