Mathematics - 2015-07-29 (page 2 of 3)

Soham Chowdhury

11:00 AM

was Tarski pre-Godel?

Remember me

11:11 AM

Hey @Soham I just started cyclic groups today .. Seem very interesting

Balarka Sen

11:24 AM

@user96343 not at all.

@SohamChowdhury who knows.

Soham Chowdhury

@Rem what?

Remember me

Cyclic groups @Soham

Balarka Sen

@SohamChowdhury you know type theory more than I do, right? if so, you'd have to teach me about them sometime later.

Soham Chowdhury

nah, very little

Balarka Sen

I hardly know anything.

Remember me

11:26 AM

Is type theory similar to category theory?

Balarka Sen

I tried reading the first chapter of the HoTT book. dependent product and dependent sums are a mess.

Soham Chowdhury

i3.cpcache.com/product_zoom/6225368/…

573

Q: "What part of Milner-Hindley do you not understand?"

I can't find it now, but I swear there used to be a T-shirt for sale featuring the immortal words: What part of do you not understand? In my case, the answer would be... all of it! In particular, I often see notation like this in Haskell papers, but I have no clue what the hell any of i...

Balarka Sen

haha.

Soham Chowdhury

The answers are actually good.

Balarka Sen

I can't make sense of the first line. $\in$ doesn't make sense in dependent type theory.

Soham Chowdhury

11:29 AM

Do you know about the Curry-Howard correspondence?

Balarka Sen

yes

Soham Chowdhury

ah, good.

Balarka Sen

that's why I said propositional calculus can be interpreted in terms of dependent type theory last night.

Danu

Hi everyone

Soham Chowdhury

right.

so the $\in$ refers to something like a context.

Balarka Sen

11:31 AM

oh.

bleh. such a mix-up.

Soham Chowdhury

Milner-Hindley type inference is magical.

You actually infer what types everything has in your program, without any explicit annotations like $x:\eta$.

(or $x::\eta$ in Haskell)

Balarka Sen

what does it say, in short?

Soham Chowdhury

What?

Balarka Sen

the whole thing in the question.

or is it just fragments of statements?

Soham Chowdhury

Oh, that's the whole type system of Haskell.

Balarka Sen

11:34 AM

oh.

Soham Chowdhury

Just like the PA axioms encode Peano arith.

Balarka Sen

right, right. I see.

Soham Chowdhury

But it also outlines a type inference algorithm.

Balarka Sen

I don't get identity types completely either. The elimination for that type seems maddeningly complicated.

Soham Chowdhury

I dunno what you're talking about.

Where did you learn TT from?

the HoTT book?

Balarka Sen

11:38 AM

some lectures, a book I forgot the name of the authors of, and the first chapter of the HoTT book.

@SohamChowdhury this thing.

it seems like the stepping stone for homotopy type theory, so I gotta understand it.

Soham Chowdhury

oh, probably has something to do w/ the univalence axiom

Balarka Sen

no, that comes later on (I think?)

Soham Chowdhury

perhaps.

you know this stuff better than I.

Remember me

So this is what you mean by logic .. I guess

Soham Chowdhury

No.

This is type theory.

Remember me

11:41 AM

Oh ...

Soham Chowdhury

@Balarka, I strongly suggest you learn a little Haskell.

It'll make you comfortable with types.

Balarka Sen

@Rememberme Mathematical logic appears as a subset of type theory.

The Substitute

hi, off topic algebra. When computing the rational canonical form (RCF) of an $n\times n$ matrix $A$ the examples in Dummit/Foote (pg 486) give 2 ways to find a matrix $P$ such that $P^{-1}AP$ equals the rational canonical form of $A$: (1) The invariant factor decomposition, and (2) Converting $A$ Directly into RCF. Can the latter always be used, or are both worth knowing?

iwriteonbananas

@BalarkaSen ok, thanks, that's what i did. just wanted to see if you approach the problem in the same way.

Balarka Sen

@Soham Not sure if I should, but thanks for the suggestion. I'm just reading these as a pass-time, remember that.

Remember me

11:43 AM

Ahh... So type theory can be said as something trying to unify maths?

Soham Chowdhury

"pastime" or "to pass the time"

learnyouahaskell.com

You can learn Idris later. It's almost the same as Haskell, but it has dep. types.

Balarka Sen

@Rememberme type theory unifyies a lot of foundations of mathematics, but not all of it. the thing that's conjectured to unify all of the foundations of mathematics is homotopy type theory.

Soham Chowdhury

(The Idris tutorial assumes familiarity with Haskell :P)

Nothing like doing computations, right? Programming will help you do that.

Balarka Sen

we'll see if this HoTT-mania survives after the exams.

Soham Chowdhury

haha

"Voevodsky is Jesus"

Balarka Sen

11:45 AM

Voevodsky is a mad guy.

He first proved the Bloch-Kato conjectures, and now he's onto this stuff. Holy hell.

Remember me

I got to see what this homotopy type theory is all about ...

Balarka Sen

I recommend you not to.

Soham Chowdhury

Ah, let him look at the book.

Remember me

Oh Okay ... Any reasons for that

Soham Chowdhury

It f**ked my mind when I first did. I was in eighth grade. :P

@Rem: homotopytypetheory.org/book

Remember me

11:47 AM

I will look at that ... If @Balarka allows

Soham Chowdhury

The cover is pretty.

Balarka Sen

I am not stopping you. I just mean that you won't understand much of the stuff if you don't know homotopy theory. Learn type theory (and some logic), perhaps.

Soham Chowdhury

Yeah.

Are you secretly trying to push me back towards my temporary AT-mania? :P

Remember me

Oh okay .. I will see . Anyway thanks @Balarka

Soham Chowdhury

(I know you aren't)

Didn't Voevodsky find some mistake in a paper of his or something?

Balarka Sen

11:50 AM

@SohamChowdhury I am definitely not.

Soham Chowdhury

Martin-Loef is alive?!

Balarka Sen

I don't know if he did.

Soham Chowdhury

Yes.

That's what made him so interested in formalization.

Remember me

You guys keep on talking about people I have no idea about .... I really know very less people from this mathematical community

Soham Chowdhury

Ah, Emily Riehl attended the IAS special year.

Balarka Sen

11:51 AM

oh, I see. well, all this theory is very good, but I'm not going as far as believing his "vision".

Soham Chowdhury

I'm reading her CT notes.

Ah, neither am I.

But formal checking would be nice, after you've done the work the "normal" way.

Balarka Sen

I don't believe HoTT would be able to do that. Neither does Lurie! (although for different reasons, I guess)

Soham Chowdhury

Lurie said he's never needed to work with those things, afaik.

Do you understand Lurie's work?

Balarka Sen

Not really just that.

Soham Chowdhury

The main ideas, at least? Like what he's trying to do?

Balarka Sen

11:54 AM

No, of course not. I don't even know what a topos is, let alone higher topoi.

I just saw one of his lectures on TQFTs, and understand what he proved about them.

Soham Chowdhury

Ah.

In his MacArthur video he said he was trying to unify AG and AT. :P

Balarka Sen

derived algebraic geometry, yeah. dunno anything about it.

Soham Chowdhury

heh.

Have you ever played with the $\lambda$-calculus?

Balarka Sen

I'm going to stop this discussion, or we'll soon be talking about thousands of names of which we know nothing (except the names).

Remember me

haha

Soham Chowdhury

12:00 PM

Hehe. But, seriously, the lambda calculus isn't advanced or anything.

Have you seriously never played around with it?

Balarka Sen

yes, but I am dropping any discussion about logic too. I've never "seriously" played with it, but yeah, I did, when I first read this stuff.

Soham Chowdhury

k

Huy

12:17 PM

@robjohn: The physics way of writing integrals is a lot clearer than the other way when integrating wrt. to many variables though, imo.

robjohn

@Huy To each their own.

Khallil

Could you show me an example, @Huy?

(I've only seen it done with one variable)

Huy

@Khallil: It's only one or two variables here but personally I'd find it a lot less easy to read if I didn't know in advance wrt. which variable we're integrating (from where to where).

Khallil

Hahahahahahahahaha!

That's messy either way :-P

Huy

@Khallil: It's just a basic computation in some of my work. When I started, I used the common mathematical notation and I was confused very quickly during computations.

It made it a lot simpler to reread and evaluate using the physics-way.

Remember me

12:30 PM

Well homotopy type theory is kind of an alternative to ZFC .. But what was the reason to create this alternative. What problems were we facing in set theory?

Huy

Or something like this, @Khallil. Just makes it immediately obvious wrt. which variable we're integrating to, which is useful, imo.

Khallil

I get what you mean, @Huy!

Huy

But yeah, for very short expressions like the one robjohn linked, I'd prefer mathematical notation too.

Semiclassical

Ahh, two-point correlators at finite temperature. Very nice to see that here :)

Another advantage of that second expression is that it lends itself to writing down Feynman diagrams

Huy

@Semiclassical: Yeah, that was actually the main work that I did there. I worked out some Feynman diagrams for the first and second derivative.

Semiclassical

12:35 PM

With that delta function constraint on momenta giving rise to a vertex with four legs

Ah, nice

That first one is more reminiscent of a path integral calculation, though of course statistical field theory and quantum field theory have a lot in common

Huy

@Semiclassical: It's actually just a Lemma for general operators on Fermionic Fock space I needed to compute the Fourier coefficients of a Green's function wrt. Matusbara frequencies.

*Matsubara

Remember me

1:00 PM

Lambda Jam 2014 - Gershom Bazerman - Homotopy Type Theory: What's the Big Idea

►

@Soham So that is what it is all about ^^

Soham Chowdhury

Yes, except that vid is aimed at people familiar with functional programming. Look at the book if you want an idea of what it's really like.

Remember me

Yes true

Soham Chowdhury

@Huy: I grew up familiar with my mother's physics books.

Especially Sakurai, if you know it.

Balarka Sen

@Rememberme no, HoTT is not an alternative to ZFC

Soham Chowdhury

Maybe that's why I prefer the "physics way" of writing integrals too.

Huy

1:06 PM

Nope, don't know Sakurai.

Soham Chowdhury

It's a QM book.

amazon.com/Modern-Quantum-Mechanics-2nd-Edition/dp/0805382917

Remember me

Hey@Balarka Is type theory a branch of computer science or maths?

Soham Chowdhury

I obviously never understood it.

But the Michelson-Morley thing at the beginning was nice.

Probably the greatest advantage was not being scared by pages full of unknown notation.

:P

Khallil

Sakurai sounds like a special move!

Like Byakurai! :-P

Huy

On a different note: Has anyone managed to install Win10 here?

I've been trying for the past 7 hours.

Balarka Sen

1:09 PM

ZFC is a set theory, @Remember. It's very weak in the sense that you can't do algebraic geometry in it. Type theory is something close to the hypothetical objects that "unifies foundations of mathematics". The techinique of incorporating homotopy theory grew out of trying to take account to, say, Grothendieck universes in a unified logical system. At least, this is the motivation, as I understand it.

Khallil

The past 7 hours?!?

Huy

Yes, the past 7 hours, no kidding.

Balarka Sen

@Rememberme Both.

Remember me

Oh that is what type theory is all about ..

Huy

One reason more to switch to Apple as soon as my PC requires replacement. I have been too spoiled by iOS updates that I am more frustrated than ever now trying to upgrade to Windows 10.

user2597879

1:11 PM

anyone here good with the chinese remainder theorem / extended gcd?

Khallil

Mac > PC for sure.

Huy

I used to be a heavy gamer, so that's why I always needed a PC.

Remember me

Why cant we do algebraic geometry in ZFC @Balarka

Balarka Sen

Too hard to explain (I don't understand it completely either). Keyword : topos.

Remember me

@BalarkaSen Any reading you would suggest for that .. A light kind of reading ?

Balarka Sen

1:17 PM

this is no light subject.

you have to learn a buckload of algebraic topology, higher category theory, topos theory to understand HoTT completely. at least, some classical algebraic topology is required to understand the "gist" of HoTT.

Remember me

Thats some prereqs

Balarka Sen

@Remember If you're so interested in this, start with some mathematical logic. That stuff was in Hammack. Then learn some axiomatic set theory maybe (I don't know of a good source, because I am not familiar with much axiomatic set theory).

But no way to learn HoTT without knowing some amount of algebraic topology.

I'd recommend you not to try to learn it.

Semiclassical

@BalarkaSen re: topos---topos approach to quantum mechanics is something which is beyond me but which you might find neat

Balarka Sen

haha, I hardly know what a topos is.

Semiclassical

heh, i don't know period :P

Remember me

1:23 PM

I looked at the definition on wiki and it made me go haywire ..

Balarka Sen

but I can believe that you can use topos to study quantum mechanics.

after all, extended TQFTs are functors between higher categories

(do you know how topological qunatum field theories relate to physics? because I don't)

Semiclassical

not really, no. i know that topological terms in QFTs are a big thing, but TQFT is outside my knowledge

Remember me

@Balarka There is something which my bro told me today...
Something by the name cosmic galois group ... Is this something related to QFT (just out of curiosity)

Balarka Sen

yeesh, motives

don't ask me about them

Semiclassical

on a similar note, page 6 of this review of topos QM gives a quick sketch of what topos theory is

Balarka Sen

1:27 PM

nah, I don't think I want to read it. I'm quickly getting over my HoTT-obsession, so all the previous discussions of mine are looking like "stating big things without knowing much" to me, and I'm trying to get over the shame.

:P

Semiclassical

snerk

fair enough

user2597879

@robjohn Is it easier if I make a new question?

Semiclassical

i do like the following snippet of it:

"Therefore, a topos is a category for which all the categorical versions of set constructs exist and are well defined. It is precisely in this sense that a topos “looks like” Sets. For example, there are topos analogues of the set-theoretic notions of cartesian product, $S\times T$, disjoint union, $S\sqcup T$, and exponential $S^T$—the set of all functions from $T$ to $S$."

robjohn

@user2597879 easier to do what? work a new example? we could do that.

@user2597879 I need to walk the dog before heading into UCLA to proctor an exam, I will be able to write up a bit in between, but I apologize if I seem somewhat unresponsive today.

Semiclassical

which is about the only part of that which i can actually understand :P

robjohn

1:32 PM

@user2597879 I could also work an example in chat

user147690

Does $[y,-[x,z]]=-[y,[x,z]]$ as lie brackets? Seems it has to if I want $\text{ad}_x \circ \text{ad}_y - \text{ad}_y \circ \text{ad}_x = \text{ad}_{[x,y]}$

Balarka Sen

all I understand from this one-day trip to type theory is that topoi are similar to dependent types theories. (they're saying things about "internal language" which bit goes ahead of me, once again)

Semiclassical

nod

user147690

Nod to me?

Semiclassical

no

user2597879

1:38 PM

@robjohn math.stackexchange.com/questions/1377996/…

the program is the result of my talks with anon last night here in the chat

but it still isn't quite right

Normally I would not bother with any of this and just use the standard chinese remainder theorem algorithm but it does not work when elements are not coprime (the standard algorithm uses inverse mod)

robjohn

2:32 PM

@user2597879 I have answered that question in the same way. I need to get to UCLA now. I will look when I get there.

user147690

@Huy You can probably answer my question on lie brackets above right?

user147690

Generic lie algebra over a field

Mike Miller

yeah misread

this is just bilinearity

user147690

Oh I see

user147690

I am taking a -1 out to the right

user147690

2:37 PM

Ignore that :P

user147690

I just meant to say $[y,-[x,z]]=[y,-1\cdot[x,z]]= [y,[x,z]]\cdot -1 = -[y,[x,z]]$

Mike Miller

sure, you don't need to pull it out to the right

the definition of bilinearity is that $[ax+by,z] = a[x,z]+b[y,z]$ and $[x,ay+bz] = a[x,y] + b[x,z]$

user147690

Oh? I thought since we don't have commutativity, we can pull out a field element in the left position to the left, and right to the right

Mike Miller

you don't have commutativity of the lie bracket, so that $[a,b]$ is not necessarily $[b,a]$, but you still have commutativity of scalar multiplication...

so it's sort of silly to even bother to talk about which side you're pulling out a scalar on. that's all I was saying

alternatively: nobody ever writes scalar multiplication on the right

user147690

Odd, my definition of bilinear map does haha

Huy

2:42 PM

What textbook are you using?

I've never seen that on the right either.

user147690

Ahh it's an old notes for a class, was for module admittedly in that case

user147690

$B(r\cdot m, n )= r\cdot B(m,n)$

$B(m,n\cdot s)=B(m,n)\cdot s$

Mike Miller

okay, that's fine, where $s$ is the element of the ground ring

in this case the Lie algebra is an $R$-bimodule so if you're multiplying with something on the right, that shouldn't change

but you're working with a field so meh

user147690

Okay fair enough

user147690

Thanks for that!

Random Variable

2:48 PM

@Chris'ssistheartist Using the Fermi-Dirac integral is what I suggested to robjohn the other day as a way to evaluate those integrals involving polylog derivatives. Using the series definition seemingly won't work since it doesn't define the polylog on the entire negative real axis.

Chris's sis the artist

@RandomVariable Yeah, that works, and it's not the only way to go.

Alec Teal

@AlexClark maths.kisogo.com/index.php?title=External_direct_sum maths.kisogo.com/index.php?title=Vector_space and my fav maths.kisogo.com/index.php?title=Addition_of_vector_spaces

user147690

Haha you looking at my 29th day stuff?

FizzledOut

Can anybody help me solve a trig problem? I need to use the Double or Half angle formulas to solve this. I spent over an hour jumping between texts and videos, none of which answered how to find the answers to this problem:

$tan(θ) + cot(θ) = 4*sin(2θ)$

These are my steps:
$sin(θ)/cos(θ) + cos(θ)/sin(θ) = 4*sin(2θ)$
$(sin^2(θ)cos^2(θ))/(sin(θ)cos(θ)) = 4*sin(2θ)$ by trig definitions
$1/(sin(θ)cos(θ)) = 4 * sin(2θ)$ by Pythagorean Identity

That's where I get stuck.

Alec Teal

@AlexClark of course. But don't worry I don't judge.

user147690

2:52 PM

xD thanks, I'll read them

user147690

Probably tomorrow since it's 1am

Alec Teal

It's more of comparing them to alexpclark.com/index.php?title=Vector_spaces

user147690

It's had two edits admittedly :P

Alec Teal

Yeah I noticed that

user147690

I am pretty much just compiling my thoughts

Alec Teal

2:54 PM

According to stats page (that''s why I have the "Notes:" namespace BTW - compiling thoughts) you have just under 6 edits per page average. Which is good, it was 6.5 yesterday

user147690

Oh there is an error I just saw

Alec Teal

(see edit)

user147690

I'll probably push it towards 20 over time :P

Alec Teal

maths.kisogo.com/index.php?title=Special:Statistics is much lower, at 3.2

Lower is better

Because you'll link to pages (and subsections of pages) later and edits can always break this or make it make less sense. So you want pages to be pretty static. Less small edits like "see also" sections

TBH it's more of "I spent 3 months doing all the footwork of adding groups, vector spaces, linear maps... all the primitives and you've just gone "Nah I'll do it from scratch"

user147690

I am pretty surprised I have reached 57 pages already

user147690

2:58 PM

Although there are only 32 content pages

Alec Teal

32

57 includes specials

Random Variable

@Chris'ssistheartist It's the only good way I can think of at the moment. You probably came up with a simpler way.

user147690

Oh okay, 32 is still pretty good

Alec Teal

alexpclark.com/index.php?title=Metric_space metric is a separate page.... not sure why.

user147690

Hmm why not?

user147690

2:59 PM

I can talk plenty more about metric spaces surely

Alec Teal

If you edit this maths.kisogo.com/index.php?title=Metric_space#Discrete_Metric you'll see that I've not actually written the definition or the table into the page code. That way they can be reused

(this link will take you to source) maths.kisogo.com/…

maths.kisogo.com/index.php?title=Discrete_metric_and_topology/… so this is the table, see the subpage - you can see where I use it by clicking "What links here" on the left.

user147690

Oh that's pretty cool

user147690

I see now. Although I am trying not to obsess over those sort of things since it's too easy to lose heaps of time xD

Alec Teal

Another good use is this maths.kisogo.com/index.php?title=Pre-measure/… it's a list and proofs of properties both a pre-measure and a measure share. By using a subpage I can transclude it in both

But it's an important thing... if you're going to re-use stuff (like say the definition of metric) you really only want to write it once. Copy-and-pasting runs the risk of changes not being carried forward.

user147690

Oh well, instead I was just going to write [[Metric|metric]] every time

user147690

3:04 PM

And since it is pretty much solely for my purpose it doesn't really need to be rewritten

Alec Teal

That only links to it.

user147690

Pretty much I just wanted to write out things in my own words, so I know what I know

Alec Teal

If you write {{:Metric}} it'll transclude the page/.

user147690

Yeah I.e. "This is actually a [[Metric|metric]] blah blah"

Alec Teal

Yeah but:
"Recall the definition of metric:
(copy paste here)"
is bad.

user147690

3:05 PM

Yeah I just mean I would never say that, I wouldn't ever say recall the definition, I would just assume it is known

user147690

Since it's just for me and I know it :P

Alec Teal

Good luck with that.

user147690

With what?

Alec Teal

That isn't how my project started at all...

But seriously, I was hoping for some competition to keep us both sharp. Getcho shit together boy.

user147690

Competition? Not interested haha

Alec Teal

3:07 PM

I can tell!

I am totally not threatened

user147690

Ok?

Alec Teal

Competition is good.

user147690

What competition?

Alec Teal

It doesn't mean like "with a prize" it stops us from stagnating.

So seriously try harder.

user147690

Try harder at what?

Deathslice

3:08 PM

I need a little help in determining if those two graphs are isomorphic. Here is how the graphs look roughly speaking(I drew it in google docs).

user147690

Setting up my website? We have different objectives?

Deathslice

Alec Teal

Try harder at notes. That's how I started.

Chris's sis the artist

@RandomVariable I didn't think of which is better, but your way is definitely good.

Alec Teal

maths.kisogo.com/index.php?title=Pre-measure/… <--see the source for use of <noinclude>

user147690

3:09 PM

@AlecTeal The whole purpose of the website is to stop myself from obsessing, and it's working, so it's purpose is being achieved

user147690

You have a different purpose

Alec Teal

No that's how it started.

Deathslice

Looks like I forgot to name the second graph so just call it graph H.

user147690

To stop yourself from obsessing?

user147690

If it moves in your direction it is literally failing, since I would be obsessing again

Alec Teal

3:10 PM

In the front of all my notebooks there's a 3 page table of pagenumbers. EOF means end of file, otherwise it's the next page in that file. So I can always append to things and come back later. It also has directories.

BUT IT WASN'T ENOUGH

So then I started the wiki thinking "Knowledge management system FTW" and at first ... I was like you. Which is why I'm doing this now. To accelerate you along the path.

Deathslice

What I've done so far is checked to see if they both have the same vertices and edges and they do.

user147690

They aren't isomorphic

user147690

The latter isn't even a standard graph, it is a multi-graph

Deathslice

Is it because graph H has a vertex that has a degree of

2

To be fair, graph H is suppose to have two ovals.

user147690

Where?