Zulip Chat Archive

Stream: general

Topic: statement of the five lemma

Johan Commelin (Apr 24 2018 at 06:36):

I just wrote a statement of the five lemma: https://gist.github.com/jcommelin/d097eb8f2587d34e5c337450bca543db

Johan Commelin (Apr 24 2018 at 06:37):

It seems extremely verbose to me. (And no, removing line breaks is not the solution :wink: ...)

Johan Commelin (Apr 24 2018 at 06:39):

If we ignore the facts that I am (i) not using lowercase greek for types, (ii) write types and conditions in the wrong order, and (iii) write lots of linebreaks; are there ways to improve this statement?

Reid Barton (Apr 24 2018 at 06:39):

Not nearly as verbose as the proof, I'm sure :simple_smile:

Reid Barton (Apr 24 2018 at 06:40):

One thing you could do is package up the underlying set function and is_group_hom instance of each map into a single type

Johan Commelin (Apr 24 2018 at 06:41):

I would love to just say: "Hey Lean, all these types are groups, and by the way, all my functions are homomorphisms"

Kenny Lau (Apr 24 2018 at 06:46):

sancta mater dei

Kenny Lau (Apr 24 2018 at 06:46):

you formalized five lemma

Kenny Lau (Apr 24 2018 at 06:46):

@Kevin Buzzard this is dank

Johan Commelin (Apr 24 2018 at 06:46):

no I did not

Johan Commelin (Apr 24 2018 at 06:46):

Only the statement

Kenny Lau (Apr 24 2018 at 06:46):

that’s what i mean

Johan Commelin (Apr 24 2018 at 06:46):

Which is not so hard to formalise, right?

Kenny Lau (Apr 24 2018 at 06:46):

formalize [sth] = formalize the statement of sth

Kenny Lau (Apr 24 2018 at 06:46):

well I never got my hands dirty

Johan Commelin (Apr 24 2018 at 06:47):

It's just a lot of repetitive strain injury inducing introductory blabla typing

Johan Commelin (Apr 24 2018 at 06:47):

I'm scared of the proof atm

Johan Commelin (Apr 24 2018 at 06:47):

But I hope that cc will do a lot of diagram chasing for me

Johan Commelin (Apr 24 2018 at 06:48):

Currently my proof starts with split, apply is_group_hom.inj_of_trivial_ker n. And then I'm stuck, because I don't know how to prove that two subsets are equal...

Johan Commelin (Apr 24 2018 at 06:49):

I really need a lot of handholding with Lean :confounded:

Johan Commelin (Apr 24 2018 at 06:56):

How do you split the goal subset_1 = subset_2 into proving x \in subset_1 \to x \in subset_2 and its converse?

Reid Barton (Apr 24 2018 at 06:56):

You can apply set.ext

Reid Barton (Apr 24 2018 at 06:56):

(I was just about to write something longer, but you said just what it does.)

Johan Commelin (Apr 24 2018 at 06:57):

Thanks, that helps. Now I get an \iff. How do I split it into two implications?

Johan Commelin (Apr 24 2018 at 06:57):

(And more meta: what is the best way to discover the answer to these questions without spamming Zulip?)

Johannes Hölzl (Apr 24 2018 at 07:00):

Either you use iff.intro or the anonymous constructor written as \< ... , ... \> where the VS Code plugin replaces the \< and \> .

Johan Commelin (Apr 24 2018 at 07:00):

Ok, cool

Johan Commelin (Apr 24 2018 at 07:00):

thanks!

Johannes Hölzl (Apr 24 2018 at 07:01):

Alternatively: use subset.antisymm then you have it in the right form (the subset relation is defintional equal to forall x subset_1 implies subset2

Johan Commelin (Apr 24 2018 at 07:05):

What are the advantages of subset.antisymm over the other method?

Kenny Lau (Apr 24 2018 at 07:05):

@Johan Commelin use split

Kenny Lau (Apr 24 2018 at 07:06):

to break down an iff

Reid Barton (Apr 24 2018 at 07:06):

In this specific case, I imagine there's probably a lemma that says that it suffices to show that f x = 0 \to x = 0

Johan Commelin (Apr 24 2018 at 07:11):

Yeah, I've got the trivial part now. If x \in trivial subgroup \to x \in ker

Johan Commelin (Apr 24 2018 at 07:12):

that's paraphrasing

Johan Commelin (Apr 24 2018 at 07:19):

Can I easily rewrite the hypothesis (com₁ : m ∘ f = r ∘ l) into com₁' : \fo x, (m (f x) = r (l x)) ?

Sean Leather (Apr 24 2018 at 07:19):

Here's my attempt to syntactically follow the lemma.

Sean Leather (Apr 24 2018 at 07:20):

It probably won't help you prove anything, of course. :simple_smile:

Kenny Lau (Apr 24 2018 at 07:21):

I mean, shouldn’t one prove the weak four lemmas first?

Johan Commelin (Apr 24 2018 at 07:22):

One could, of course... but they are basically the two subgoals after the first split

Johan Commelin (Apr 24 2018 at 07:22):

There is a good reason to do that though... because then you only have to prove one of them

Johan Commelin (Apr 24 2018 at 07:22):

the other follows by duality

Johan Commelin (Apr 24 2018 at 07:23):

Still, the proof is a very straightforward diagram chase... so I hope I can convince Lean that it is easy as well

Johan Commelin (Apr 24 2018 at 07:24):

I want to tell lean "For every group_hom \phi that you can see, do this... have := is_group_hom.one \phi"

Johan Commelin (Apr 24 2018 at 07:24):

And things like that

Johan Commelin (Apr 24 2018 at 07:25):

And one it has figured out all these basic things, then cc might actually deduce the result

Johan Commelin (Apr 24 2018 at 07:26):

But then cc needs to know how to deal with \circ, hence my previous question about rewriting com\1

Johan Commelin (Apr 24 2018 at 07:27):

@Sean Leather Thanks for the refactoring. It is more readable now (except that I most I would give the arrows names like f_1, g_1 and f_2, g_2 etc...)

Johan Commelin (Apr 24 2018 at 07:27):

But it is still a bit verbose, right?

Reid Barton (Apr 24 2018 at 07:27):

I added a comment with an "artistic" layout

Reid Barton (Apr 24 2018 at 07:27):

(warning: long lines)

Johan Commelin (Apr 24 2018 at 07:28):

Ha! I like that one

Johan Commelin (Apr 24 2018 at 07:28):

It really explains the diagram. Cool!

Johan Commelin (Apr 24 2018 at 07:29):

It would be great of you could tell lean [is_group_hom f g h i j k l]

Johan Commelin (Apr 24 2018 at 07:30):

something like that, and it just understands that all of them are group homs

Sean Leather (Apr 24 2018 at 07:31):

It would be great of you could tell lean [is_group_hom f g h i j k l]

Something like that would be useful in your case, but you wouldn't want to remove the ability to use multiple-parameter type classes, which it looks like is_group_hom is there.

Johan Commelin (Apr 24 2018 at 07:31):

Hmmz, I see

Johan Commelin (Apr 24 2018 at 07:32):

Also: ↪ and ↠ for injective respectively surjective functions

Johan Commelin (Apr 24 2018 at 07:33):

But I guess that might be a bit hard

Johan Commelin (Apr 24 2018 at 07:33):

So {f: A ↪ B} means {f: A → B} [function.injective f]

Sean Leather (Apr 24 2018 at 07:36):

At the very least, you can open function to avoid having to prepend function.. :simple_smile:

Johan Commelin (Apr 24 2018 at 07:36):

Aaah, ok. TIL :)

Johan Commelin (Apr 24 2018 at 07:36):

Hmmz TIL is confusing in this context. I meant "Today I Learned"

Kevin Buzzard (Apr 24 2018 at 07:54):

(And more meta: what is the best way to discover the answer to these questions without spamming Zulip?)

Spam Zulip. I was in just this situation last September and spamming Zulip was by far the most efficient method. Mario often answered very quickly, and several others too. Now there are more people who can help, and the sooner you're up to speed the sooner you can help others. It's really important that mathematicians learn how to use this software as quickly as possible.

Kevin Buzzard (Apr 24 2018 at 07:54):

PS I hope you're going to implement the abstract abelian category proof rather than all the diagram-chasing ;-)

Kevin Buzzard (Apr 24 2018 at 07:55):

[not serious]

Kevin Buzzard (Apr 24 2018 at 07:56):

although, in this crazy, world, who's to say that the abstract universal property proof won't be easier!

Kevin Buzzard (Apr 24 2018 at 07:56):

I find myself in a similar situation right now, as it happens.

Kevin Buzzard (Apr 24 2018 at 07:56):

I would like to prove R[1/f][1/g] = R[1/fg] (unique isomorphism of R-algebras)

Kevin Buzzard (Apr 24 2018 at 07:57):

and I have set up all these universal properties and I know I can deduce it from those, and it will be really nice to do

Kevin Buzzard (Apr 24 2018 at 07:57):

but I suspect that if I were to ask Kenny he would just write down a proof with lots of quotient.mk's in which just did everything directly.

Kevin Buzzard (Apr 24 2018 at 07:58):

i.e. we have an interface (i.e. a bunch of universal properties) which will enable me to prove my result, but now I realise that someone who knows the underlying implementation can just prove the result directly anyway.

Kevin Buzzard (Apr 24 2018 at 07:58):

It might be the same here; you can deduce the 5 lemma from the axioms of an ab cat

Kevin Buzzard (Apr 24 2018 at 07:58):

or from the diagram chase

Kevin Buzzard (Apr 24 2018 at 07:58):

and the proofs will be very different

Johan Commelin (Apr 24 2018 at 08:02):

Yes, I see. I think it should be possible to have a diagram_chase tactic

Johan Commelin (Apr 24 2018 at 08:03):

And my gut feeling is that cc is almost it. But you need to spam the context with a lot of information about group homomorphisms and kernels etc...

Kevin Buzzard (Apr 24 2018 at 08:05):

diagram_chase tactic: I wonder if that's possible!

Kevin Buzzard (Apr 24 2018 at 08:05):

As far as I know these CS people don't really do this kind of maths

Kevin Buzzard (Apr 24 2018 at 08:06):

so you might find that this is actually a possibility once you formalise what you want

Patrick Massot (Apr 24 2018 at 08:07):

That would be sooo nice

Kevin Buzzard (Apr 24 2018 at 08:07):

When drawing that snake map from ker(map3) to coker(map1) I always feel I'm making the unique move each time

Patrick Massot (Apr 24 2018 at 08:07):

Is the new parser going to accept tikz-cd input?

Sean Leather (Apr 24 2018 at 08:07):

As far as I know these CS people don't really do this kind of maths

:astonished: Diagrams are pretty core to PLT.

Patrick Massot (Apr 24 2018 at 08:07):

PLT?

Kevin Buzzard (Apr 24 2018 at 08:07):

diagram-chasing in abelian groups is perhaps a bit different

Sean Leather (Apr 24 2018 at 08:07):

Programming language theory.

Patrick Massot (Apr 24 2018 at 08:07):

thks

Sean Leather (Apr 24 2018 at 08:08):

diagram-chasing in abelian groups is perhaps a bit different

Okay. I'm not familiar with it, so that may be.

Kevin Buzzard (Apr 24 2018 at 08:08):

Is the theory of abelian categories "complete" in some way?

Johan Commelin (Apr 24 2018 at 08:08):

Yes, I was thinking about tikz-cd as well (-;

Kevin Buzzard (Apr 24 2018 at 08:08):

i.e. "the five lemma is true, so there should be a proof which an algorithm can construct"?

Kevin Buzzard (Apr 24 2018 at 08:09):

Just think, we could pester Mario to spend weeks developing such an algorithm, and then use it to prove the five lemma and then say "actually, the five lemma is pretty much the only thing we ever use"

Johan Commelin (Apr 24 2018 at 08:09):

@Patrick Massot Did you see how @Reid Barton rewrote the statement? https://gist.github.com/jcommelin/d097eb8f2587d34e5c337450bca543db

Kevin Buzzard (Apr 24 2018 at 08:09):

"but thanks anyway"

Johan Commelin (Apr 24 2018 at 08:09):

Ouch

Johan Commelin (Apr 24 2018 at 08:10):

And the snake lemma, and the rest of homological algebra

Kevin Buzzard (Apr 24 2018 at 08:10):

That PR will be rejected because the groups aren't all called alpha

Johan Commelin (Apr 24 2018 at 08:10):

Yeah, I will relabel everything to be alpha_1 alpha_2 etc...

Johan Commelin (Apr 24 2018 at 08:10):

who needs betas

Kevin Buzzard (Apr 24 2018 at 08:12):

I concur with Kenny's "dank" comment

Kevin Buzzard (Apr 24 2018 at 08:12):

This is absolutely great

Patrick Massot (Apr 24 2018 at 08:12):

No, you should keep groups G. Mario and Johannes will end up understanding.

Patrick Massot (Apr 24 2018 at 08:12):

Don't release pressure on this important issue

Johan Commelin (Apr 24 2018 at 08:12):

Sure

Johan Commelin (Apr 24 2018 at 08:12):

Was just kidding

Johan Commelin (Apr 24 2018 at 08:13):

@Kevin Buzzard Well, thanks. I thought it was a good test case

Reid Barton (Apr 24 2018 at 08:35):

Is the theory of abelian categories "complete" in some way?

No, https://mathoverflow.net/a/12799

Reid Barton (Apr 24 2018 at 08:37):

Most similar theories will admit embeddings of the word problem like this, I think. But in diagrams where there are only finitely many ways to compose morphisms (basically, "without loops"), maybe there is hope.

Kevin Buzzard (Apr 24 2018 at 08:56):

Thanks @Reid Barton . I wondered if the abelian-ness of the situation saved our bacon but somehow this automorphism trick gets you back into a non-abelian situation

Johan Commelin (Apr 24 2018 at 09:26):

I put an update in the comments of the gist: https://gist.github.com/jcommelin/d097eb8f2587d34e5c337450bca543db

Johan Commelin (Apr 24 2018 at 09:27):

The first half of the proof is almost done

Johan Commelin (Apr 24 2018 at 09:27):

There is one stupid admit

Johan Commelin (Apr 24 2018 at 09:27):

And I don't get why apply_assumption fails, because 2 lines above, there is f_1 w = y

Kevin Buzzard (Apr 24 2018 at 09:28):

Your definition of im is not great

Kevin Buzzard (Apr 24 2018 at 09:29):

You defined definition im (f : A → B) [is_group_hom f] := f '' (@set.univ A)

Johan Commelin (Apr 24 2018 at 09:29):

No, no longer

Johan Commelin (Apr 24 2018 at 09:29):

See the update

Kevin Buzzard (Apr 24 2018 at 09:29):

Oh OK

Johan Commelin (Apr 24 2018 at 09:29):

It is now set.range f

Johan Commelin (Apr 24 2018 at 09:29):

I dunno if that is better (-;

Kevin Buzzard (Apr 24 2018 at 09:30):

That's definitely better

Kevin Buzzard (Apr 24 2018 at 09:30):

The problem with the old one

Kevin Buzzard (Apr 24 2018 at 09:30):

definition im (f : A → B) [is_group_hom f] := f '' (@set.univ A)

Kevin Buzzard (Apr 24 2018 at 09:31):

was that you can write #print notation '' to find out what '' expands to

Kevin Buzzard (Apr 24 2018 at 09:31):

and see it expands to set.image

Kevin Buzzard (Apr 24 2018 at 09:31):

and then #print set.image to find what that unfolds to

Johan Commelin (Apr 24 2018 at 09:31):

I see...

Kevin Buzzard (Apr 24 2018 at 09:31):

and you see it becomes \ex a, a \in set.univ and f a = b

Kevin Buzzard (Apr 24 2018 at 09:32):

in particular we have some clause which is always true

Kevin Buzzard (Apr 24 2018 at 09:32):

and in the way

Kevin Buzzard (Apr 24 2018 at 09:32):

With your new definition we can do stuff like this:

Kevin Buzzard (Apr 24 2018 at 09:32):

import group_theory.subgroup

open function is_group_hom

universes u

variables {A B : Type u} [group A] [group B]
definition im (f : A → B) := set.range f

example (G H K : Type u) [group G] [group H] [group K] (α : G → H) [is_group_hom α]
(β : H → K) [is_group_hom β] (Hexact : im α = ker β) (h : H) (Hker : β h = 1) :
∃ g, α g = h :=
begin
have Hker2 : h ∈ ker β := (mem_ker β).2 Hker,
rw ←Hexact at Hker2,
exact Hker2
end