Zulip Chat Archive

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....

Reid Barton (Aug 03 2020 at 17:24):

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

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?

Kenny Lau (Aug 03 2020 at 19:38):

indeed!

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

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

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

(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

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

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?

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

I guess it is

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

Another option is trees of (formal) compositions modulo associativity

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

& 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. :-)

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

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.

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

(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:

/-
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 (Aug 04 2020 at 07:10):

presumably rename list_fun to list_hom?

Kenny Lau (Aug 04 2020 at 07:16):

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?

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

@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):

/-
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 (Aug 04 2020 at 07:45):

"maximal generality"

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

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

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

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 GG and construct the free category associated to it.


Last updated: Dec 20 2023 at 11:08 UTC