Zulip Chat Archive

Stream: maths

Topic: quivers and diagrams


view this post on Zulip Johan Commelin (May 01 2018 at 10:00):

I've got the following snippet

import data.list

universes u v w

structure quiver :=
(V : Type u)
(E : Type v)
(s : E  V)
(t : E  V)

variable {Q : quiver}

definition is_a_path : (list Q.E)  Prop
| [] := true
| [e] := true
| (e₁ :: e₂ :: es) := Q.s e₁ = Q.t e₂  is_a_path (e₂ :: es)

structure diagram :=
(D : Q.V  Type w)
(m : Π (e : Q.E), D (Q.s e)  D (Q.t e))

view this post on Zulip Johan Commelin (May 01 2018 at 10:00):

But now I realise that I actually only want to consider finite lists

view this post on Zulip Kenny Lau (May 01 2018 at 10:00):

why don't you use chain lol

view this post on Zulip Kenny Lau (May 01 2018 at 10:00):

aha

view this post on Zulip Johan Commelin (May 01 2018 at 10:00):

How would I best go about that

view this post on Zulip Kenny Lau (May 01 2018 at 10:00):

but lists are all finite

view this post on Zulip Johan Commelin (May 01 2018 at 10:00):

Why?

view this post on Zulip Kenny Lau (May 01 2018 at 10:01):

because they're defined inductively

view this post on Zulip Kenny Lau (May 01 2018 at 10:01):

inductive list : Type u  Type u
constructors:
list.nil : Π {T : Type u}, list T
list.cons : Π {T : Type u}, T  list T  list T

view this post on Zulip Kenny Lau (May 01 2018 at 10:01):

and I can inductively prove that they are finite :P

view this post on Zulip Johan Commelin (May 01 2018 at 10:01):

I see

view this post on Zulip Johan Commelin (May 01 2018 at 10:01):

Crazy...

view this post on Zulip Kenny Lau (May 01 2018 at 10:02):

you want lazy lists?

view this post on Zulip Kenny Lau (May 01 2018 at 10:02):

I see you want everything to be lazy

view this post on Zulip Kenny Lau (May 01 2018 at 10:02):

maybe that's why you think they're crazy

view this post on Zulip Johan Commelin (May 01 2018 at 10:02):

Hmm, maybe now I'm happy that they aren't lazy (-;

view this post on Zulip Kenny Lau (May 01 2018 at 10:02):

maybe your ideas are a bit hazy

view this post on Zulip Johan Commelin (May 01 2018 at 10:02):

That.

view this post on Zulip Kenny Lau (May 01 2018 at 10:03):

http://www.rhymezone.com/r/rhyme.cgi?Word=lazy&typeofrhyme=perfect

view this post on Zulip Johan Commelin (May 01 2018 at 10:03):

That is definitely true. It's one of my defining properties

view this post on Zulip Kenny Lau (May 01 2018 at 10:03):

not many words rhyme with lazy though

view this post on Zulip Kenny Lau (May 01 2018 at 10:03):

so I'm done coz I can't use daisy

view this post on Zulip Mario Carneiro (May 01 2018 at 10:03):

I guess you just did

view this post on Zulip Johan Commelin (May 01 2018 at 10:03):

And you don't wanna look like jay z

view this post on Zulip Johan Commelin (May 01 2018 at 10:05):

Anyway... I am going to try and define the set of all paths, and then try to figure out how to define commutative diagrams

view this post on Zulip Kenny Lau (May 01 2018 at 10:05):

hmm... I would rather use categories to define diagrams

view this post on Zulip Kenny Lau (May 01 2018 at 10:06):

https://github.com/kckennylau/category-theory/blob/master/src/natural_transformation.lean

view this post on Zulip Kenny Lau (May 01 2018 at 10:06):

@[reducible] def product {α} (C : category.{u v} α) (ι) (f : ι  α) :=
limit (discrete ι) C (functor.of_discrete C f)

view this post on Zulip Kenny Lau (May 01 2018 at 10:07):

product is the limit of the discrete diagram

view this post on Zulip Johan Commelin (May 01 2018 at 10:07):

But that is not how we use them, I think

view this post on Zulip Kenny Lau (May 01 2018 at 10:07):

is it not?


Last updated: May 12 2021 at 07:17 UTC