Zulip Chat Archive

Stream: general

Topic: random math question

Andrew Ashworth (Mar 31 2018 at 18:51):

so, seeing as how there are many mathematicians here, can anyone recommend a textbook on algebraic topology? I'd like to be able to read https://arxiv.org/pdf/1802.04443.pdf

Kenny Lau (Mar 31 2018 at 18:51):

Hatcher, of course

Kenny Lau (Mar 31 2018 at 18:52):

(your pdf is still loading, wait)

Kenny Lau (Mar 31 2018 at 18:54):

@Andrew Ashworth Hatcher Chapter 2

Andrew Ashworth (Mar 31 2018 at 18:56):

thanks, i'll check it out

Simon Hudon (Mar 31 2018 at 18:58):

@Andrew Ashworth Are you taking on Machine Learning as a hobby? I've been contemplating getting literate in the domain. There seems to be a lot to be done there. I'm curious about proving security / safety properties in those systems but I still don't know where to start

Andrew Ashworth (Mar 31 2018 at 19:02):

hopefully more than a hobby once i learn more about it

Andrew Ashworth (Mar 31 2018 at 19:02):

i work in imaging and radar

Andrew Ashworth (Mar 31 2018 at 19:03):

are you looking for textbook recommendations? that's where i started off

Simon Hudon (Mar 31 2018 at 19:03):

Interesting. ML must be useful but tricky thing to use there

Simon Hudon (Mar 31 2018 at 19:03):

Yes, thanks!

Kenny Lau (Mar 31 2018 at 19:04):

how would you name the groups that can be generated by a set that injects to S?

Kenny Lau (Mar 31 2018 at 19:04):

as in, name them in Lean

Simon Hudon (Mar 31 2018 at 19:05):

What is S?

Kenny Lau (Mar 31 2018 at 19:05):

a random set

Andrew Ashworth (Mar 31 2018 at 19:06):

i'd start off with the elements of statistical learning

Kenny Lau (Mar 31 2018 at 19:06):

@Simon Hudon I just need a short name

Kenny Lau (Mar 31 2018 at 19:06):

you know

Simon Hudon (Mar 31 2018 at 19:07):

So when you say "injects" I assume you have an injective function from S to S?

Simon Hudon (Mar 31 2018 at 19:07):

Actually, if you show me the construction, that would help me find a name for it

Kenny Lau (Mar 31 2018 at 19:07):

I mean, a group G is inside my structure if it is generated by a set T with an injection from T to S

Simon Hudon (Mar 31 2018 at 19:09):

Ok, that's clearer. Is that group interesting because of your choice of S and then the group basically says that the set T exists and is the set underlying G?

Kenny Lau (Mar 31 2018 at 19:10):

structure to_be_named (G : Type u) [group G] :=
( gen : set G )
( gen_gen : group.generate gen = set.univ )
( func : gen → S )
( inj : function.injective func )

Simon Hudon (Mar 31 2018 at 19:10):

i'd start off with the elements of statistical learning

Thanks! Do you plan on doing some ML in Lean?

Kenny Lau (Mar 31 2018 at 19:16):

@Simon Hudon do you have any suggestions?

Andrew Ashworth (Mar 31 2018 at 19:16):

that would be really hard without a good way of handling algebra and probability

Andrew Ashworth (Mar 31 2018 at 19:16):

er, by algebra i mean matrices

Last updated: Dec 20 2023 at 11:08 UTC