Zulip Chat Archive

Stream: maths

Topic: composing a list of functions


view this post on Zulip Kenny Lau (Aug 03 2020 at 16:59):

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

view this post on Zulip Kenny Lau (Aug 03 2020 at 16:59):

Currently we can only compose two functions

view this post on Zulip Kenny Lau (Aug 03 2020 at 16:59):

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

view this post on Zulip Adam Topaz (Aug 03 2020 at 16:59):

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

view this post on Zulip Jalex Stark (Aug 03 2020 at 17:00):

what's the type of the list?

view this post on Zulip Kenny Lau (Aug 03 2020 at 17:11):

Jalex Stark said:

what's the type of the list?

exactly

view this post on Zulip Adam Topaz (Aug 03 2020 at 17:21):

There must be something like heterogeneous lists right?

view this post on Zulip Adam Topaz (Aug 03 2020 at 17:21):

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

view this post on Zulip Adam Topaz (Aug 03 2020 at 17:24):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Aug 03 2020 at 18:02):

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

view this post on Zulip Mario Carneiro (Aug 03 2020 at 18:04):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 03 2020 at 19:34):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Aug 03 2020 at 19:38):

Are you defining the nerve?

view this post on Zulip Kenny Lau (Aug 03 2020 at 19:38):

indeed!

view this post on Zulip Adam Topaz (Aug 03 2020 at 19:38):

Cool!

view this post on Zulip Adam Topaz (Aug 03 2020 at 19:39):

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

view this post on Zulip Kenny Lau (Aug 03 2020 at 19:39):

you don't need induction right

view this post on Zulip Kenny Lau (Aug 03 2020 at 19:40):

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

view this post on Zulip Kenny Lau (Aug 03 2020 at 19:40):

(pseudocode)

view this post on Zulip 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 :)

view this post on Zulip Kenny Lau (Aug 03 2020 at 19:41):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 03 2020 at 19:45):

defining constructing the free category sounds like a cool project

view this post on Zulip Reid Barton (Aug 03 2020 at 19:47):

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

view this post on Zulip Kenny Lau (Aug 03 2020 at 19:49):

aha, inductive

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 03 2020 at 19:50):

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

view this post on Zulip Kenny Lau (Aug 03 2020 at 19:50):

I guess it is

view this post on Zulip Reid Barton (Aug 03 2020 at 19:51):

Another option is trees of (formal) compositions modulo associativity

view this post on Zulip Reid Barton (Aug 03 2020 at 19:51):

& unitality

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 03 2020 at 19:52):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Aug 03 2020 at 20:12):

Mathlib should really have categories internal to other categories :)

view this post on Zulip 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 :)

view this post on Zulip Bhavik Mehta (Aug 03 2020 at 20:13):

i'm pretty sure it compiles on the latest mathlib

view this post on Zulip Kenny Lau (Aug 03 2020 at 20:15):

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

view this post on Zulip Adam Topaz (Aug 03 2020 at 20:16):

A category is an internal category in types :)

view this post on Zulip Adam Topaz (Aug 03 2020 at 20:16):

(At least in the way Reid mentioned above)

view this post on Zulip Kenny Lau (Aug 03 2020 at 20:16):

apart from that, I guess

view this post on Zulip Reid Barton (Aug 03 2020 at 20:17):

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

view this post on Zulip Reid Barton (Aug 03 2020 at 20:25):

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

view this post on Zulip 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

view this post on Zulip Adam Topaz (Aug 03 2020 at 22:09):

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

view this post on Zulip 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))

view this post on Zulip Kenny Lau (Aug 04 2020 at 05:21):

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

view this post on Zulip Kenny Lau (Aug 04 2020 at 05:21):

but there seems no other way

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Aug 04 2020 at 05:31):

yeah that sounds like a good idea

view this post on Zulip Scott Morrison (Aug 04 2020 at 06:18):

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

view this post on Zulip 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

view this post on Zulip 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. :-)

view this post on Zulip Kenny Lau (Aug 04 2020 at 06:27):

right

view this post on Zulip Kenny Lau (Aug 04 2020 at 06:27):

where in the category library should this go?

view this post on Zulip Scott Morrison (Aug 04 2020 at 06:28):

I guess comp_append would be harder.

view this post on Zulip Scott Morrison (Aug 04 2020 at 06:28):

(deleted)

view this post on Zulip Kenny Lau (Aug 04 2020 at 06:28):

but I just proved comp_append

view this post on Zulip Kenny Lau (Aug 04 2020 at 06:28):

oh, you mean for categories

view this post on Zulip Scott Morrison (Aug 04 2020 at 06:29):

Yes. Harder, but still easy. :-)

view this post on Zulip Scott Morrison (Aug 04 2020 at 06:29):

Just make a new file in category_theory/?

view this post on Zulip Scott Morrison (Aug 04 2020 at 06:29):

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

view this post on Zulip Kenny Lau (Aug 04 2020 at 06:30):

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

view this post on Zulip Kenny Lau (Aug 04 2020 at 06:30):

comp list.repeat = nat.iterate!

view this post on Zulip 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

view this post on Zulip Scott Morrison (Aug 04 2020 at 06:41):

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

view this post on Zulip 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...

view this post on Zulip Kenny Lau (Aug 04 2020 at 06:46):

the category theory composition is the opposite of functions iirc

view this post on Zulip Scott Morrison (Aug 04 2020 at 06:47):

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

view this post on Zulip Scott Morrison (Aug 04 2020 at 06:48):

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

view this post on Zulip Kenny Lau (Aug 04 2020 at 06:50):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 04 2020 at 07:00):

just to make the inductive require one argument less

view this post on Zulip Kenny Lau (Aug 04 2020 at 07:01):

@Scott Morrison is this ok?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Aug 04 2020 at 07:10):

presumably rename list_fun to list_hom?

view this post on Zulip Kenny Lau (Aug 04 2020 at 07:16):

done

view this post on Zulip Kenny Lau (Aug 04 2020 at 07:17):

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

view this post on Zulip 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)

view this post on Zulip Scott Morrison (Aug 04 2020 at 07:18):

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

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Aug 04 2020 at 07:35):

is graph in mathlib?

view this post on Zulip Kenny Lau (Aug 04 2020 at 07:35):

@Scott Morrison

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Kenny Lau (Aug 04 2020 at 07:40):

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

view this post on Zulip Kenny Lau (Aug 04 2020 at 07:42):

oh what am I doing, generalizing category theory itself

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 04 2020 at 07:45):

"maximal generality"

view this post on Zulip Kenny Lau (Aug 04 2020 at 07:47):

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

view this post on Zulip Kenny Lau (Aug 04 2020 at 07:47):

aha

view this post on Zulip Kenny Lau (Aug 04 2020 at 07:47):

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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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]

view this post on Zulip 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: May 14 2021 at 18:28 UTC