Zulip Chat Archive

Stream: general

Topic: proof of the five lemma


view this post on Zulip Johan Commelin (Apr 24 2018 at 12:30):

Yoohoo, I'm done.
https://gist.github.com/jcommelin/9ea76f7a1356ed8dd9499e765f580ef8
It's pretty long and ugly.

view this post on Zulip Johan Commelin (Apr 24 2018 at 12:31):

Feel free to start golfing on this one (-;

view this post on Zulip Johan Commelin (Apr 24 2018 at 12:31):

I feel that a computer should almost be able to find the proof alone

view this post on Zulip Johan Commelin (Apr 24 2018 at 12:32):

But my tactic-fu is small and my tactic-writing-fu is nonexistent

view this post on Zulip Sean Leather (Apr 24 2018 at 12:32):

But how would the computer know how many times to apply_assumption? :dizzy_face: :laughing:

view this post on Zulip Johan Commelin (Apr 24 2018 at 12:33):

Yeah, agreed... but still... every line I really just follow my nose...

view this post on Zulip Sean Leather (Apr 24 2018 at 12:33):

The nice thing about your proof is that it is clearly step-by-step.

view this post on Zulip Johan Commelin (Apr 24 2018 at 12:33):

And I guess already with the existing tactics I think it can be reasonably shortened

view this post on Zulip Johan Commelin (Apr 24 2018 at 12:34):

Because using commutativity or computations in a group takes pretty long atm

view this post on Zulip Johan Commelin (Apr 24 2018 at 12:35):

I feel like the lines with \ex bla : Group, condition are the only place that Lean should get my help.

view this post on Zulip Johan Commelin (Apr 24 2018 at 12:35):

The rest it should figure out alone...

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:34):

/me updated the proof of the five lemma: https://gist.github.com/jcommelin/9ea76f7a1356ed8dd9499e765f580ef8

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:34):

It is now refactored to first prove two four-lemmas

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:34):

These then combine to prove the five lemma

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:36):

begin
 split,
 apply four_lemma₁ com₁ com₂ com₃ eB₁ eC₁ eB₂ eC₂ hj hk.1 hm.1,
 apply four_lemma₂ com₂ com₃ com₄ eC₁ eD₁ eC₂ eD₂ hk.2 hm.2 hn,
end

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:36):

now I would write this in term mode lol

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:37):

four_lemma₁ com₁ com₂ com₃ eB₁ eC₁ eB₂ eC₂ hj hk.1 hm.1, four_lemma₂ com₂ com₃ com₄ eC₁ eD₁ eC₂ eD₂ hk.2 hm.2 hn

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:37):

Aah, yes. I should have done that

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:38):

Also, can I use some _ business to let it figure out the hypotheses itself?

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:38):

yes

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:38):

I tried... and failed :disappointed:

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:38):

you removed the wrong things :P

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:38):

_ does not find the value from assumptions

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:38):

_ only does unification

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:39):

and only first order (and zeroth order) unification

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:40):

Hmm, ok... But it should be able to figure out everything alone

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:40):

I will need to learn at some point how to do that

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:40):

it does not find the appropriate proofs from the asumptions

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:40):

No, but I mean the com₁ com₂ com₃ eB₁ eC₁ eB₂ eC₂ hj hk.1 hm.1 stuff

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:41):

why would it be able to figure them out?

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:41):

the goal is bijective l

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:41):

it does not contain any of those things you mentioned

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:41):

they have to be found from the assumption list

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:41):

which _ does not do

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:41):

_ only unifies types

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:41):

Yes, and the type of l is C_1 \to C_2

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:42):

and those are mentioned in the statement, and there are requirements (e.g. a group B_1 with a map to C_1

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:42):

but if you replace com₁ with _, the compiler would have to find com₁ from the assumptions

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:42):

...), and those are also in the context, etcc...

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:42):

it is not in the type of the goal

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:42):

it is not in the type of any component of the goal

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:42):

_ does not find things from the local context

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:43):

(that is what I meant by assumption)

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:43):

H1 : something
H2 : something
|- goal

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:43):

_ does not match against H1 and H2

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:43):

unless the goal contains them

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:43):

I see

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:43):

So, maybe I should not have done apply ..., but simp [four_lemma_1]

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:44):

or something like that?

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:44):

does that work?

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:44):

I doubt that works

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:44):

try apply four_lemma₁, repeat { assumption }

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:45):

alternatively apply four_lemma₁; try { assumption }

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:46):

hmm, doesn't make it shorter... because it can't figure out hk.1 on it's own...

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:46):

right

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:46):

never mind, I learned something (-;

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:47):

:)

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:47):

Next up: the snake lemma ???

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:48):

I heard one of them follows from the other

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:48):

I guess the snake lemma is stronger

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:48):

maybe we should have proved the snake lemma first :P

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:48):

lol

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:48):

There is also the salamander lemma

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:49):

And you can apply it 4 times to get the snake lemma

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:49):

then perhaps we should prove that first

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:49):

https://ncatlab.org/nlab/show/salamander+lemma

view this post on Zulip Johan Commelin (Apr 24 2018 at 14:49):

My eyes always glaze over when I read that page

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:50):

:P

view this post on Zulip Kenny Lau (Apr 24 2018 at 14:51):

really, prove the strongest theorem, and your work will be minimized

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:37):

I need the three lemma

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:37):

I need that if A,B,C,A',B',C' are abelian groups

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:37):

and A -> B -> C is exact

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:37):

and A is isomorphic to A'

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:37):

and B to B'

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:37):

and C to C'

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:37):

and we have maps A' -> B' -> C'

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:38):

with both squares commuting

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:38):

then A' -> B' -> C' is exact

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:38):

As a mathematician my instinct is to do surgery on the first sequence

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:38):

i.e. simply replace A with A', B with B' and C with C' and then say we're done

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:39):

I am trying to work out if there is a general principle here

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:40):

but if there is, I don't think I can formulate it well in Lean yet.

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:40):

It says something like "if there is a commutative diagram, and you do some computation like image of this over kernel of this"

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:40):

"and then you take a term in the commutative diagram and replace it with an isomorphic term such that all the diagrams commute"

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:41):

"then the computation changes in the same way"

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:41):

but I fear that I am going to have to use three lemmas to prove the three lemma

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:41):

one for replacing A

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:41):

one for B

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:41):

and one for C

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:43):

or just prove it by brute force in one go

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:43):

and then deal with the fact that I'll need another trivial lemma of this form tomorrow, tomorrow

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:43):

I want more of this abstract nonsense in Lean

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:44):

either for abelian groups

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:44):

or for abelian categories

view this post on Zulip Johan Commelin (Apr 27 2018 at 07:45):

Hmm, I'm sorry that my five lemma doesn't help :slightly_frowning_face:

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:45):

yes, it's too strong :-)

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:45):

it proves something non-trivial

view this post on Zulip Johan Commelin (Apr 27 2018 at 07:45):

Haha

view this post on Zulip Johan Commelin (Apr 27 2018 at 07:46):

We need a very good way of substituting isomorphic things

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:46):

rw :-)

view this post on Zulip Johan Commelin (Apr 27 2018 at 07:46):

I don't know much about HoTT, but I think this is what Voevodsky was after as well

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:46):

yes

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:46):

I wrote some vague mumblings about that in some other thread a week or so ago

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:46):

after reading some of his work

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 07:47):

but he redefined =

view this post on Zulip Johan Commelin (Apr 27 2018 at 07:47):

Well, if you're changing from ZFC to type theory, might as well change '='

view this post on Zulip Johan Commelin (Apr 27 2018 at 07:48):

Anyway, I guess that you are not saved by 5 rws

view this post on Zulip Johan Commelin (Apr 27 2018 at 07:48):

So we need @Scott Morrison 's category theory, and then some strong tactics that know about commutative diagrams

view this post on Zulip Johan Commelin (Apr 27 2018 at 07:57):

Or are you just going for a temporary brute force approach?

view this post on Zulip Kenny Lau (Apr 27 2018 at 10:13):

import algebra.group data.set data.equiv

def is_add_group_hom {α : Type*} {β : Type*} [add_group α] [add_group β] (f : α  β) : Prop :=
@is_group_hom (multiplicative α) (multiplicative β) _ _ f

attribute [class] is_add_group_hom

namespace is_add_group_hom

variables {α : Type*} {β : Type*} [add_group α] [add_group β] (f : α  β) [hf : is_add_group_hom f]

theorem mk (H :  x y, f (x + y) = f x + f y) : is_add_group_hom f :=
H

theorem add (x y) : f (x + y) = f x + f y :=
@is_group_hom.mul (multiplicative α) (multiplicative β) _ _ f hf x y

theorem zero : f 0 = 0 :=
@is_group_hom.one (multiplicative α) (multiplicative β) _ _ f hf

theorem neg (x) : f (-x) = -f x :=
@is_group_hom.inv (multiplicative α) (multiplicative β) _ _ f hf x

def ker : set α :=
{ x | f x = 0 }

end is_add_group_hom

theorem three (A B C A' B' C' : Type*)
  [add_comm_group A] [add_comm_group A']
  [add_comm_group B] [add_comm_group B']
  [add_comm_group C] [add_comm_group C']
  (ab : A  B) [is_add_group_hom ab]
  (bc : B  C) [is_add_group_hom bc]
  (Habc : set.range ab = is_add_group_hom.ker bc)
  (fa : A  A') [is_add_group_hom fa]
  (fb : B  B') [is_add_group_hom fb]
  (fc : C  C') [is_add_group_hom fc]

  (ab' : A'  B') [is_add_group_hom ab']
  (bc' : B'  C') [is_add_group_hom bc']
  (H1 : fb  ab = ab'  fa)
  (H2 : fc  bc = bc'  fb) :

  set.range ab' = is_add_group_hom.ker bc' :=
begin
  apply set.ext,
  intro b',
  split,
  { intro hb',
    cases hb' with a' ha',
    simp [is_add_group_hom.ker],
    let a := fa.symm a',
    have ha : fa a = a',
    { simp [a] },
    rw [ ha',  ha],
    change bc' ((ab'  fa) a) = 0,
    rw  H1,
    change (bc'  fb) (ab a) = 0,
    rw  H2,
    have H3 : ab a  is_add_group_hom.ker bc,
    { rw  Habc, existsi a, simp },
    simp [is_add_group_hom.ker] at H3 ,
    rw H3,
    apply is_add_group_hom.zero },
  { intro hb',
    let b := fb.symm b',
    have hb : fb b = b',
    { simp [b] },
    simp [is_add_group_hom.ker] at hb',
    rw  hb at hb',
    change (bc'  fb) b = 0 at hb',
    rw  H2 at hb',
    rw  is_add_group_hom.zero fc at hb',
    replace hb' := congr_arg fc.symm hb',
    simp at hb',
    have H3 : b  set.range ab,
    { rwa Habc },
    cases H3 with a ha,
    existsi fa a,
    change (ab'  fa) a = b',
    rw  H1,
    simp [ha] }
end

view this post on Zulip Kenny Lau (Apr 27 2018 at 10:14):

@Kevin Buzzard

view this post on Zulip Kenny Lau (Apr 27 2018 at 10:25):

that's why I don't like stating equality with function composition

view this post on Zulip Kenny Lau (Apr 27 2018 at 10:29):

import algebra.group data.set data.equiv

def is_add_group_hom {α : Type*} {β : Type*} [add_group α] [add_group β] (f : α  β) : Prop :=
@is_group_hom (multiplicative α) (multiplicative β) _ _ f

attribute [class] is_add_group_hom

namespace is_add_group_hom

variables {α : Type*} {β : Type*} [add_group α] [add_group β] (f : α  β) [hf : is_add_group_hom f]

theorem mk (H :  x y, f (x + y) = f x + f y) : is_add_group_hom f :=
H

theorem add (x y) : f (x + y) = f x + f y :=
@is_group_hom.mul (multiplicative α) (multiplicative β) _ _ f hf x y

theorem zero : f 0 = 0 :=
@is_group_hom.one (multiplicative α) (multiplicative β) _ _ f hf

theorem neg (x) : f (-x) = -f x :=
@is_group_hom.inv (multiplicative α) (multiplicative β) _ _ f hf x

def ker : set α :=
{ x | f x = 0 }

end is_add_group_hom

theorem three (A B C A' B' C' : Type*)
  [add_comm_group A] [add_comm_group A']
  [add_comm_group B] [add_comm_group B']
  [add_comm_group C] [add_comm_group C']
  (ab : A  B) [is_add_group_hom ab]
  (bc : B  C) [is_add_group_hom bc]
  (Habc : set.range ab = is_add_group_hom.ker bc)
  (fa : A  A') [is_add_group_hom fa]
  (fb : B  B') [is_add_group_hom fb]
  (fc : C  C') [is_add_group_hom fc]

  (ab' : A'  B') [is_add_group_hom ab']
  (bc' : B'  C') [is_add_group_hom bc']
  (H1 :  a, fb (ab a) = ab' (fa a))
  (H2 :  b, fc (bc b) = bc' (fb b)) :

  set.range ab' = is_add_group_hom.ker bc' :=
begin
  apply set.ext,
  intro b',
  split,
  { intro hb',
    cases hb' with a' ha',
    simp [is_add_group_hom.ker],
    let a := fa.symm a',
    have ha : fa a = a',
    { simp [a] },
    rw [ ha',  ha,  H1,  H2],
    have H3 : ab a  is_add_group_hom.ker bc,
    { rw  Habc, existsi a, simp },
    simp [is_add_group_hom.ker] at H3 ,
    rw H3,
    apply is_add_group_hom.zero },
  { intro hb',
    let b := fb.symm b',
    have hb : fb b = b',
    { simp [b] },
    simp [is_add_group_hom.ker] at hb',
    rw [ hb,  H2,  is_add_group_hom.zero fc] at hb',
    replace hb' := congr_arg fc.symm hb',
    simp at hb',
    have H3 : b  set.range ab,
    { rwa Habc },
    cases H3 with a ha,
    existsi fa a,
    rw  H1,
    simp [ha] }
end

view this post on Zulip Kenny Lau (Apr 27 2018 at 10:30):

this is much better

view this post on Zulip Reid Barton (Apr 27 2018 at 17:56):

How about proving some lemmas like this one, and combining them into what you want.

import data.equiv

open set

lemma equiv_range {α β : Type*} (f : α  β) {α' β' : Type*} (f' : α'  β')
  ( : α  α') ( : β  β') (h : f'   =   f) :
  range f' =  '' range f :=
calc range f' = f' '' univ         : by rw image_univ
     ...      = f' '' (range )   : by rw range_iff_surjective.mpr .bijective.2
     ...      = f' '' ( '' univ) : by rw image_univ
     ...      = (f'  ) '' univ  : by rw image_comp
     ...      = (  f) '' univ   : by rw h
     ...      =  '' (f '' univ)  : by rw image_comp
     ...      =  '' range f      : by rw image_univ

view this post on Zulip Reid Barton (Apr 27 2018 at 18:23):

(Now I see that Patrick said much the same thing about a half hour earlier.)

view this post on Zulip Johan Commelin (Apr 27 2018 at 19:20):

I should have used calc in my proof of the five lemma...

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 20:22):

You live and learn in this game

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 20:23):

Your levels were really helpful for me today. Do you know some abstract type theory?

view this post on Zulip Kevin Buzzard (Apr 27 2018 at 20:23):

You understood what Scott was saying


Last updated: May 15 2021 at 00:39 UTC