proof of the five lemma

Stream: general

[Johan Commelin]

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

[Johan Commelin]

Feel free to start golfing on this one (-;

[Johan Commelin]

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

[Johan Commelin]

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

[Sean Leather]

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

[Johan Commelin]

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

[Sean Leather]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

The rest it should figure out alone...

[Johan Commelin]

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

[Johan Commelin]

It is now refactored to first prove two four-lemmas

[Johan Commelin]

These then combine to prove the five lemma

[Kenny Lau]

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]

now I would write this in term mode lol

[Kenny Lau]

⟨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]

Aah, yes. I should have done that

[Johan Commelin]

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

[Kenny Lau]

yes

[Johan Commelin]

I tried... and failed :disappointed:

[Kenny Lau]

you removed the wrong things :P

[Kenny Lau]

_ does not find the value from assumptions

[Kenny Lau]

_ only does unification

[Kenny Lau]

and only first order (and zeroth order) unification

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

it does not find the appropriate proofs from the asumptions

[Johan Commelin]

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

[Kenny Lau]

why would it be able to figure them out?

[Kenny Lau]

the goal is bijective l

[Kenny Lau]

it does not contain any of those things you mentioned

[Kenny Lau]

they have to be found from the assumption list

[Kenny Lau]

which _ does not do

[Kenny Lau]

_ only unifies types

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Kenny Lau]

it is not in the type of the goal

[Kenny Lau]

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

[Kenny Lau]

_ does not find things from the local context

[Kenny Lau]

(that is what I meant by assumption)

[Kenny Lau]

H1 : something
H2 : something
|- goal

[Kenny Lau]

_ does not match against H1 and H2

[Kenny Lau]

unless the goal contains them

[Johan Commelin]

I see

[Johan Commelin]

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

[Johan Commelin]

or something like that?

[Kenny Lau]

does that work?

[Kenny Lau]

I doubt that works

[Kenny Lau]

try apply four_lemma₁, repeat { assumption }

[Kenny Lau]

alternatively apply four_lemma₁; try { assumption }

[Johan Commelin]

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

[Kenny Lau]

right

[Johan Commelin]

never mind, I learned something (-;

[Kenny Lau]

:)

[Johan Commelin]

Next up: the snake lemma ???

[Kenny Lau]

I heard one of them follows from the other

[Johan Commelin]

I guess the snake lemma is stronger

[Kenny Lau]

maybe we should have proved the snake lemma first :P

[Johan Commelin]

lol

[Johan Commelin]

There is also the salamander lemma

[Johan Commelin]

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

[Kenny Lau]

then perhaps we should prove that first

[Johan Commelin]

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

[Johan Commelin]

My eyes always glaze over when I read that page

[Kenny Lau]

:P

[Kenny Lau]

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

[Kevin Buzzard]

I need the three lemma

[Kevin Buzzard]

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

[Kevin Buzzard]

and A -> B -> C is exact

[Kevin Buzzard]

and A is isomorphic to A'

[Kevin Buzzard]

and B to B'

[Kevin Buzzard]

and C to C'

[Kevin Buzzard]

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

[Kevin Buzzard]

with both squares commuting

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

"then the computation changes in the same way"

[Kevin Buzzard]

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

[Kevin Buzzard]

one for replacing A

[Kevin Buzzard]

one for B

[Kevin Buzzard]

and one for C

[Kevin Buzzard]

or just prove it by brute force in one go

[Kevin Buzzard]

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

[Kevin Buzzard]

I want more of this abstract nonsense in Lean

[Kevin Buzzard]

either for abelian groups

[Kevin Buzzard]

or for abelian categories

[Johan Commelin]

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

[Kevin Buzzard]

yes, it's too strong :-)

[Kevin Buzzard]

it proves something non-trivial

[Johan Commelin]

Haha

[Johan Commelin]

We need a very good way of substituting isomorphic things

[Kevin Buzzard]

rw :-)

[Johan Commelin]

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

[Kevin Buzzard]

yes

[Kevin Buzzard]

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

[Kevin Buzzard]

after reading some of his work

[Kevin Buzzard]

but he redefined =

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

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

[Kenny Lau]

@Kevin Buzzard

[Kenny Lau]

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

[Kenny Lau]

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

[Kenny Lau]

this is much better

[Reid Barton]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

You live and learn in this game

[Kevin Buzzard]

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

[Kevin Buzzard]

You understood what Scott was saying