## Stream: general

### Topic: proof of the five lemma

#### Johan Commelin (Apr 24 2018 at 12:30):

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

#### Johan Commelin (Apr 24 2018 at 12:31):

Feel free to start golfing on this one (-;

#### Johan Commelin (Apr 24 2018 at 12:31):

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

#### Johan Commelin (Apr 24 2018 at 12:32):

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

#### Sean Leather (Apr 24 2018 at 12:32):

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

#### Johan Commelin (Apr 24 2018 at 12:33):

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

#### Sean Leather (Apr 24 2018 at 12:33):

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

#### Johan Commelin (Apr 24 2018 at 12:33):

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

#### Johan Commelin (Apr 24 2018 at 12:34):

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

#### 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.

#### Johan Commelin (Apr 24 2018 at 12:35):

The rest it should figure out alone...

#### Johan Commelin (Apr 24 2018 at 14:34):

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

#### Johan Commelin (Apr 24 2018 at 14:34):

It is now refactored to first prove two four-lemmas

#### Johan Commelin (Apr 24 2018 at 14:34):

These then combine to prove the five lemma

#### 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


#### Kenny Lau (Apr 24 2018 at 14:36):

now I would write this in term mode lol

#### 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⟩


#### Johan Commelin (Apr 24 2018 at 14:37):

Aah, yes. I should have done that

#### Johan Commelin (Apr 24 2018 at 14:38):

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

yes

#### Johan Commelin (Apr 24 2018 at 14:38):

I tried... and failed :disappointed:

#### Kenny Lau (Apr 24 2018 at 14:38):

you removed the wrong things :P

#### Kenny Lau (Apr 24 2018 at 14:38):

_ does not find the value from assumptions

#### Kenny Lau (Apr 24 2018 at 14:38):

_ only does unification

#### Kenny Lau (Apr 24 2018 at 14:39):

and only first order (and zeroth order) unification

#### Johan Commelin (Apr 24 2018 at 14:40):

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

#### Johan Commelin (Apr 24 2018 at 14:40):

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

#### Kenny Lau (Apr 24 2018 at 14:40):

it does not find the appropriate proofs from the asumptions

#### 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

#### Kenny Lau (Apr 24 2018 at 14:41):

why would it be able to figure them out?

#### Kenny Lau (Apr 24 2018 at 14:41):

the goal is bijective l

#### Kenny Lau (Apr 24 2018 at 14:41):

it does not contain any of those things you mentioned

#### Kenny Lau (Apr 24 2018 at 14:41):

they have to be found from the assumption list

#### Kenny Lau (Apr 24 2018 at 14:41):

which _ does not do

#### Kenny Lau (Apr 24 2018 at 14:41):

_ only unifies types

#### Johan Commelin (Apr 24 2018 at 14:41):

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

#### 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

#### Kenny Lau (Apr 24 2018 at 14:42):

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

#### Johan Commelin (Apr 24 2018 at 14:42):

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

#### Kenny Lau (Apr 24 2018 at 14:42):

it is not in the type of the goal

#### Kenny Lau (Apr 24 2018 at 14:42):

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

#### Kenny Lau (Apr 24 2018 at 14:42):

_ does not find things from the local context

#### Kenny Lau (Apr 24 2018 at 14:43):

(that is what I meant by assumption)

#### Kenny Lau (Apr 24 2018 at 14:43):

H1 : something
H2 : something
|- goal


#### Kenny Lau (Apr 24 2018 at 14:43):

_ does not match against H1 and H2

#### Kenny Lau (Apr 24 2018 at 14:43):

unless the goal contains them

I see

#### Johan Commelin (Apr 24 2018 at 14:43):

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

#### Johan Commelin (Apr 24 2018 at 14:44):

or something like that?

does that work?

#### Kenny Lau (Apr 24 2018 at 14:44):

I doubt that works

#### Kenny Lau (Apr 24 2018 at 14:44):

try apply four_lemma₁, repeat { assumption }

#### Kenny Lau (Apr 24 2018 at 14:45):

alternatively apply four_lemma₁; try { assumption }

#### 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...

right

#### Johan Commelin (Apr 24 2018 at 14:46):

never mind, I learned something (-;

:)

#### Johan Commelin (Apr 24 2018 at 14:47):

Next up: the snake lemma ???

#### Kenny Lau (Apr 24 2018 at 14:48):

I heard one of them follows from the other

#### Johan Commelin (Apr 24 2018 at 14:48):

I guess the snake lemma is stronger

#### Kenny Lau (Apr 24 2018 at 14:48):

maybe we should have proved the snake lemma first :P

lol

#### Johan Commelin (Apr 24 2018 at 14:48):

There is also the salamander lemma

#### Johan Commelin (Apr 24 2018 at 14:49):

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

#### Kenny Lau (Apr 24 2018 at 14:49):

then perhaps we should prove that first

#### Johan Commelin (Apr 24 2018 at 14:49):

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

#### Johan Commelin (Apr 24 2018 at 14:49):

My eyes always glaze over when I read that page

:P

#### Kenny Lau (Apr 24 2018 at 14:51):

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

#### Kevin Buzzard (Apr 27 2018 at 07:37):

I need the three lemma

#### Kevin Buzzard (Apr 27 2018 at 07:37):

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

#### Kevin Buzzard (Apr 27 2018 at 07:37):

and A -> B -> C is exact

#### Kevin Buzzard (Apr 27 2018 at 07:37):

and A is isomorphic to A'

and B to B'

and C to C'

#### Kevin Buzzard (Apr 27 2018 at 07:37):

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

#### Kevin Buzzard (Apr 27 2018 at 07:38):

with both squares commuting

#### Kevin Buzzard (Apr 27 2018 at 07:38):

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

#### Kevin Buzzard (Apr 27 2018 at 07:38):

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

#### 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

#### Kevin Buzzard (Apr 27 2018 at 07:39):

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

#### Kevin Buzzard (Apr 27 2018 at 07:40):

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

#### 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"

#### 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"

#### Kevin Buzzard (Apr 27 2018 at 07:41):

"then the computation changes in the same way"

#### 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

#### Kevin Buzzard (Apr 27 2018 at 07:41):

one for replacing A

one for B

and one for C

#### Kevin Buzzard (Apr 27 2018 at 07:43):

or just prove it by brute force in one go

#### 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

#### Kevin Buzzard (Apr 27 2018 at 07:43):

I want more of this abstract nonsense in Lean

#### Kevin Buzzard (Apr 27 2018 at 07:44):

either for abelian groups

#### Kevin Buzzard (Apr 27 2018 at 07:44):

or for abelian categories

#### Johan Commelin (Apr 27 2018 at 07:45):

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

#### Kevin Buzzard (Apr 27 2018 at 07:45):

yes, it's too strong :-)

#### Kevin Buzzard (Apr 27 2018 at 07:45):

it proves something non-trivial

Haha

#### Johan Commelin (Apr 27 2018 at 07:46):

We need a very good way of substituting isomorphic things

#### Kevin Buzzard (Apr 27 2018 at 07:46):

rw :-)

#### 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

yes

#### Kevin Buzzard (Apr 27 2018 at 07:46):

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

#### Kevin Buzzard (Apr 27 2018 at 07:46):

after reading some of his work

#### Kevin Buzzard (Apr 27 2018 at 07:47):

but he redefined =

#### Johan Commelin (Apr 27 2018 at 07:47):

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

#### Johan Commelin (Apr 27 2018 at 07:48):

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

#### 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

#### Johan Commelin (Apr 27 2018 at 07:57):

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

#### 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

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 }

theorem three (A B C A' B' C' : Type*)
(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',
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 },
rw H3,
{ intro hb',
let b := fb.symm b',
have hb : fb b = b',
{ simp [b] },
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


@Kevin Buzzard

#### Kenny Lau (Apr 27 2018 at 10:25):

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

#### 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

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 }

theorem three (A B C A' B' C' : Type*)
(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',
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 },
rw H3,
{ intro hb',
let b := fb.symm b',
have hb : fb b = b',
{ simp [b] },
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


#### Kenny Lau (Apr 27 2018 at 10:30):

this is much better

#### 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' : α' → β')
(eα : α ≃ α') (eβ : β ≃ β') (h : f' ∘ eα = eβ ∘ f) :
range f' = eβ '' range f :=
calc range f' = f' '' univ         : by rw image_univ
...      = f' '' (range eα)   : by rw range_iff_surjective.mpr eα.bijective.2
...      = f' '' (eα '' univ) : by rw image_univ
...      = (f' ∘ eα) '' univ  : by rw ←image_comp
...      = (eβ ∘ f) '' univ   : by rw h
...      = eβ '' (f '' univ)  : by rw image_comp
...      = eβ '' range f      : by rw image_univ


#### Reid Barton (Apr 27 2018 at 18:23):

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

#### Johan Commelin (Apr 27 2018 at 19:20):

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

#### Kevin Buzzard (Apr 27 2018 at 20:22):

You live and learn in this game

#### Kevin Buzzard (Apr 27 2018 at 20:23):

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

#### Kevin Buzzard (Apr 27 2018 at 20:23):

You understood what Scott was saying

Last updated: May 15 2021 at 00:39 UTC