Zulip Chat Archive

Stream: new members

Topic: cone morphisms


view this post on Zulip Calle Sönne (Oct 24 2019 at 16:59):

Is there some theorem in lean that proves composition of cone morphism is a cone morphism? I cant find it in cone.lean or limit.lean

view this post on Zulip Kenny Lau (Oct 24 2019 at 17:08):

@Calle Sönne

@[simps] instance cone.category : category.{v} (cone F) :=
{ hom  := λ A B, cone_morphism A B,
  comp := λ X Y Z f g,
  { hom := f.hom  g.hom,
    w' := by intro j; rw [assoc, g.w, f.w] },
  id   := λ B, { hom := 𝟙 B.X } }

view this post on Zulip Kenny Lau (Oct 24 2019 at 17:08):

that they form a category

view this post on Zulip Kenny Lau (Oct 24 2019 at 17:09):

that also means you shouldn't use cone_morphism explicitly, but rather A \hom B

view this post on Zulip Calle Sönne (Oct 26 2019 at 10:48):

I have the following code:

lemma comm_of_equalizer : equalizer f g  equalizer g f :=
begin
let H1 : equalizer f g  equalizer g f, exact equalizer.lift g f (equalizer.ι f g) (eq.symm ((equalizer.condition) f g)),
let H2 : equalizer g f  equalizer f g, exact equalizer.lift f g (equalizer.ι g f) (eq.symm ((equalizer.condition) g f)),
have comp12 : H1  H2 = 𝟙 (equalizer f g), apply uniq_cone_morphism limit.is_limit((equalizer f g)) (H1  H2) (𝟙 (equalizer f g))

end

The last have line is a sketch of what I want to say, right now it is giving me an error. I want to apply uniq_cone_morphism to get a goal to show that both H1 >> H2 and the identity are cone morphisms. The statement for uniq_cone_morphism is:

lemma uniq_cone_morphism {s t : cone F} (h : is_limit t) {f f' : s  t} : f = f'

So I need to say that the equalizer is the limit and here is where I get confused. Equalizer is defined as:

abbreviation equalizer := limit (parallel_pair f g)

But limit is defined to be the object of the cone that is the limit:

class has_limit (F : J  C) :=
(cone : cone F)
(is_limit : is_limit cone . tactic.apply_instance)

def limit.cone (F : J  C) [has_limit F] : cone F := has_limit.cone F

def limit (F : J  C) [has_limit F] := (limit.cone F).X

So my question is: from the object (limit) equalizer f g how do I refer back to the cone (whilst preserving the information that it is indeed a limit)

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 10:48):

what imports do you need to get this running?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 10:49):

I should really learn this stuff at some point

view this post on Zulip Calle Sönne (Oct 26 2019 at 10:49):

import category_theory.limits.shapes.equalizers
import category_theory.limits.limits

open category_theory

namespace category_theory.limits
namespace is_limit

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 10:50):

I still have errors

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 10:50):

just make a new scratch file and minimise

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 10:51):

unknown identifier 'equalizer' being the most serious one

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 10:52):

unknown identifier 'f' being the next one

view this post on Zulip Calle Sönne (Oct 26 2019 at 10:54):

Oh I got variables. I will send them

view this post on Zulip Calle Sönne (Oct 26 2019 at 10:54):

variables {C : Type u} [𝒞 : category.{v} C]
include 𝒞
variables {X Y : C}
variables (f g : X ⟶ Y)
variables [has_limit (parallel_pair f g)] [has_limit (parallel_pair g f)]

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 10:54):

Now I have errors on parallel_pair. Just create a new file, get it working at your end, and paste the whole thing

view this post on Zulip Calle Sönne (Oct 26 2019 at 10:55):

Ok

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 10:55):

I don't know anything, I don't know what is defined where, but I'm very interested in this project you're doing

view this post on Zulip Calle Sönne (Oct 26 2019 at 10:59):

import category_theory.limits.shapes.equalizers
import category_theory.limits.limits

open category_theory

namespace category_theory.limits
namespace is_limit

universes v u

variables {C : Type u} [𝒞 : category.{v} C]
include 𝒞
variables {X Y : C}
variables (f g : X  Y)
variables [has_limit (parallel_pair f g)]  [has_limit (parallel_pair g f)]

lemma comm_of_equalizer : equalizer f g  equalizer g f :=
begin
let H1 : equalizer f g  equalizer g f, exact equalizer.lift g f (equalizer.ι f g) (eq.symm ((equalizer.condition) f g)),
let H2 : equalizer g f  equalizer f g, exact equalizer.lift f g (equalizer.ι g f) (eq.symm ((equalizer.condition) g f)),
have comp12 : H1  H2 = 𝟙 (equalizer f g), apply uniq_cone_morphism limit.is_limit((equalizer f g)) (H1  H2) (𝟙 (equalizer f g))
end


end is_limit
end category_theory.limits

this is enough for me

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 10:59):

Oh!

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:00):

I am using a mathlib from July, that must be the problem. Sorry!

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:02):

Mario would tell you to use refine not apply because apply is in core and has a bug which we can't fix

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:03):

Oh, thats good to know thanks!

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:04):

So the error is this:

type mismatch at application
  limits.is_limit.uniq_cone_morphism limits.limit.is_limit
term
  limits.limit.is_limit
has type
  Π (F : ?m_1 ⥤ ?m_3) [_inst_3 : limits.has_limit F], limits.is_limit (limits.limit.cone F) : Type (max
        (max ? ?)
        ?
        ?)
but is expected to have type
  limits.is_limit ?m_6 : Type (max ? ?)
Additional information:
/home/buzzard/Encfs/Computer_languages/Lean/lean-projects/natural_number_game/scratch/scratch.lean:22:9: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  too many arguments

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:04):

yeah

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:05):

so it says "limits.limit.is_limit wants an F but you didn't give it an F"?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:07):

Is this progress: refine uniq_cone_morphism (limit.is_limit (equalizer f g) (H1 ≫ H2) (𝟙 (equalizer f g)))? Or have I misunderstood something?

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:07):

yeah thats the problem, I gave equalizer but thats the limit object

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:08):

Does \gg do composition in "the wrong order"?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:08):

oh yes I can just check its type and see that it does

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:09):

wait it does?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:09):

Isn't it at this point that you just type tidy or some other fancy tactic and you're done?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:09):

You are using gg correctly

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:10):

I was just thrown for a second

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:10):

neither tidy or simp works

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:12):

Why does

have comp12 : H1  H2 = 𝟙 (equalizer f g),
  refine uniq_cone_morphism _,

not work?

invalid type ascription, term has type
  ?m_8 = ?m_9
but is expected to have type
  H1 ≫ H2 = 𝟙 (limits.equalizer f g)

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:12):

Yeah I got to there now as well

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:12):

I didnt have to give the cone, I had to give the diagram (parallel_pair f g)

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:15):

Now one thing Im not sure of is if lean 'knows' that the identity and composition of H1 and H2 are cone morphisms. As kenny said earlier the fact that they form a category is in mathlib, but maybe we need to provide this explictly

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:15):

  refine @uniq_cone_morphism _ _ _ _ _ _ _ _ _ _ (_ : H1  H2 = 𝟙 (limits.equalizer f g)),

doesn't work either

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:17):

  convert @uniq_cone_morphism _ _ _ _ _ _ _ _ (H1  H2) _,

gives

type mismatch at application
  category_struct.comp H1
term
  H1
has type
  limits.equalizer f g ⟶ limits.equalizer g f : Type v
but is expected to have type
  ?m_6 ⟶ ?m_7 : Type ?

Is this a universe issue??

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:18):

convert @uniq_cone_morphism.{v} _ _ _ _ _ _ _ _ (H1  H2) (𝟙 (equalizer f g)),

shows it isn't.

type mismatch at application
  category_struct.comp H1
term
  H1
has type
  limits.equalizer f g ⟶ limits.equalizer g f
but is expected to have type
  ?m_6 ⟶ ?m_7

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:19):

Now I need to count to see which is the 6th _

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:22):

I think we need to show that H1 and H2 are cone morphisms

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:22):

Because right now they are just maps between some objects

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:22):

equalizer is just the object, not the cone

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:22):

right, this seems to me to be just a case of looking carefully at the type of everything

view this post on Zulip Scott Morrison (Oct 26 2019 at 11:23):

Just saw this thread, and may have to run in a moment.

view this post on Zulip Scott Morrison (Oct 26 2019 at 11:24):

Have a look at def prod.braiding (P Q : C) : P ⨯ Q ≅ Q ⨯ P := ...

view this post on Zulip Scott Morrison (Oct 26 2019 at 11:24):

in category_theory/limits/shapes/binary_products.lean

view this post on Zulip Scott Morrison (Oct 26 2019 at 11:25):

I don't think uniq_cone_morphism is going to be particularly helpful -- why do you want to use that?

view this post on Zulip Scott Morrison (Oct 26 2019 at 11:26):

Oh, to prove that the two compositions are the identity, I see.

view this post on Zulip Scott Morrison (Oct 26 2019 at 11:28):

local attribute [tidy] tactic.case_bash

lemma comm_of_equalizer : equalizer f g  equalizer g f :=
{ hom := equalizer.lift g f (equalizer.ι f g) (eq.symm ((equalizer.condition) f g)),
  inv := equalizer.lift f g (equalizer.ι g f) (eq.symm ((equalizer.condition) g f)), }

doesn't quite get there, but it gives two very manageable goals that possibly ought to be simp lemmas.

view this post on Zulip Scott Morrison (Oct 26 2019 at 11:29):

(The first incantation local attribute [tidy] tactic.case_bash tells the tidy tactic that it's allowed to case bash on hypotheses which are inductive types. In particular, that means that to prove two natural transformations out of a "finite" category are equal, it can check object by object.)

view this post on Zulip Scott Morrison (Oct 26 2019 at 11:31):

(Boarding a flight Perth-London, so I'll be offline for a while. :-) Good luck!)

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:31):

Which London?

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:41):

I dont really understand the above syntax, how to I continue of what Scott was doing?

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:42):

Is the := just like let?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:42):

he's making a structure, isn't he?

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:42):

Oh right the isomorphism

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:43):

But then how do I continue the proof?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:43):

good question! I was trying to figure out what was going on in your proof still.

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:44):

I think he decided to come to London to help you out personally. It's a bit of an extreme reaction but he has to be applauded.

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:44):

got it

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:45):

lemma comm_of_equalizer : equalizer f g  equalizer g f :=
begin
  refine_struct { hom := equalizer.lift g f (equalizer.ι f g) (eq.symm ((equalizer.condition) f g)),
  inv := equalizer.lift f g (equalizer.ι g f) (eq.symm ((equalizer.condition) g f)), },
  sorry, sorry
end

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:46):

does this help? Now it looks like you have to prove something which looks like a standard diagram chase.

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:47):

Yes exactly, but it feels like that could be done by some tactic?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:48):

I'm afraid I do't know how the category theory library works at all. For those watching with amusement, we're now on

⊢ limits.equalizer.ι f g ≫ g = limits.limit.π (limits.parallel_pair f g) limits.walking_parallel_pair.one

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:50):

Yeah right now im just reading up, hopefully there is some theorem about the fact that the projection commutes with the diagram

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:50):

I mean its in the definition but Im not sure how to access that

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:50):

you could just wait for about 20 hours and then go and meet him at the airport

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:51):

Seems like a reasonable plan

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:52):

but I think this will help

@[simp] lemma cone.w {F : J  C} (c : cone F) {j j' : J} (f : j  j') :
  c.π.app j  F.map f = c.π.app j' :=
by convert (c.π.naturality f).symm; apply id_comp

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:54):

But then the question again becomes how to we access the cone of the equalizer

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:54):

I cannot steer this stuff at all.

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:54):

steer?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:58):

I don't even know the basics.

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:58):

https://github.com/leanprover-community/mathlib/blob/master/docs/tutorial/category_theory/calculating_colimits_in_Top.lean

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:58):

That's the only documentation I have ever seen.

view this post on Zulip Calle Sönne (Oct 26 2019 at 11:58):

ah

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:58):

What I'm saying is that I don't have a clue how to access the cone of the equalizer. In maths I'd just draw a picture and say we were done.

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:59):

But I can't work Scott's library

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 11:59):

If it were a car, I'm not saying that I can't drive it, I'm saying I can't even use the steering wheel.

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 12:02):

I should stress that this is entirely my problem, not Scott's. Furthermore I think that trying to prove math-trivial things such as the equaliser of f and g is isomorphic the equaliser of g and f is exactly the way one should learn these things. Maybe when you meet Scott at the airport you can tell him that I've booked a room at Imperial for the talk he's giving in London which explains all this stuff.

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:03):

I made some progress!

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:04):

but minor...

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:04):

lemma comm_of_equalizer : equalizer f g  equalizer g f :=
begin
  refine_struct { hom := equalizer.lift g f (equalizer.ι f g) (eq.symm ((equalizer.condition) f g)),
  inv := equalizer.lift f g (equalizer.ι g f) (eq.symm ((equalizer.condition) g f)), },
  rw [limit.w],
end

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:04):

 limits.equalizer.ι f g  g =
    limits.limit.π (limits.parallel_pair f g) ?m_1  (limits.parallel_pair f g).map ?m_2

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:05):

Just have to figure out how to supply ?m_1 and ?m_2

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:17):

lemma comm_of_equalizer : equalizer f g  equalizer g f :=
begin
  refine_struct { hom := equalizer.lift g f (equalizer.ι f g) (eq.symm ((equalizer.condition) f g)),
  inv := equalizer.lift f g (equalizer.ι g f) (eq.symm ((equalizer.condition) g f)), },
  rw [limit.w (parallel_pair f g) walking_parallel_pair_hom.right, parallel_pair_map_right],
  rw [limit.w (parallel_pair g f) walking_parallel_pair_hom.right, parallel_pair_map_right],
end

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:18):

now it is done. Thank you very much for the help @Kevin Buzzard @Scott Morrison

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 12:18):

Now write some docs! ;-)

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 12:19):

Make a new file in the https://github.com/leanprover-community/mathlib/tree/master/docs/tutorial/category_theory directory and just write down the basic things you need to know to work with equalisers and give this as an example.

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 12:19):

And then Patrick will accept the PR and...oh :-/

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:22):

I think I need some more practice first. Now I will try to prove

lemma mono_of_equalizer : mono (equalizer.ι f g) :=

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 12:24):

I am absolutely serious when I say that if you just figure out how to prove three trivial things about equalizers and then just write a little piece saying what the problems are and how to solve them in Lean and dump it as a .md file in that category theory directory then you will be doing a great service to the community, and not least to people like me who see this stuff now, understand it, forget it, and then can't find this thread in 1 month's time -- people like me (old people) and newcomers (beginners) really need documentation.

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:26):

Another trivial lean question:

class mono (f : X  Y) : Prop :=
(right_cancellation : Π {Z : C} (g h : Z  X) (w : g  f = h  f), g = h)

I have the above class and I want to prove

lemma mono_of_equalizer : mono (equalizer.ι f g)

I tried using intro but it says "Pi\let expression expected" What does this mean?

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:26):

Like how do I unfold

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:26):

I am absolutely serious when I say that if you just figure out how to prove three trivial things about equalizers and then just write a little piece saying what the problems are and how to solve them in Lean and dump it as a .md file in that category theory directory then you will be doing a great service to the community, and not least to people like me who see this stuff now, understand it, forget it, and then can't find this thread in 1 month's time -- people like me (old people) and newcomers (beginners) really need documentation.

Im thinning I could write it after proving both of these things

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 12:27):

I tried using intro but it says "Pi\let expression expected" What does this mean?

That means "the goal is not a pi type, it's something else"

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 12:28):

indeed, mono is a structure

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 12:28):

lemma mono_of_equalizer : mono (equalizer.ι f g) :=
begin
  refine ⟨_⟩,
  intro,

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 12:30):

lemma mono_of_equalizer : mono (equalizer.ι f g) :=
{ right_cancellation := begin
  intro,
  sorry,
end}

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 12:42):

So I've been trying to answer your original question ("how do I get my way to work") and I am slowly beginning to get to the point where you were when you asked the question.

term
  limits.equalizer f g
has type
  C : Type u
but is expected to have type
  limits.cone ?m_3 : Type (max u v)

This is the problem, right?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 12:45):

uniq_cone_morphism, the thing you were initially trying to use, does not prove that two morphisms in C are equal, it proves that two morphisms in some category called limits.cone F are equal. This is why you're stuck.

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 12:46):

[or rather why you were stuck 2 hours ago]

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:47):

yeah exactly

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:48):

So what I was wondering was how to lift the information to the category of cones

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:48):

limit (diagram) is not the cone, but just the element

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:57):

I have a problem for the last step of the proof, a rewrite in the middle of a function composition:

lemma mono_of_equalizer : mono (equalizer.ι f g) :=
begin
refine ⟨_⟩,
intros Z h i comp,
apply limit.hom_ext,
intro j, cases j,
refine comp,
rw [limit.w (parallel_pair f g) walking_parallel_pair_hom.right, comp],
end

This is my goal:

1 goal
case category_theory.limits.walking_parallel_pair.one
C : Type u,
𝒞 : category C,
X Y : C,
f g : X  Y,
_inst_1 : limits.has_limit (limits.parallel_pair f g),
_inst_2 : limits.has_limit (limits.parallel_pair g f),
Z : C,
h i : Z  limits.equalizer f g,
comp : h  limits.equalizer.ι f g = i  limits.equalizer.ι f g
 h 
      limits.limit.π (limits.parallel_pair f g) limits.walking_parallel_pair.zero 
        (limits.parallel_pair f g).map limits.walking_parallel_pair_hom.right =
    i 
      limits.limit.π (limits.parallel_pair f g) limits.walking_parallel_pair.zero 
        (limits.parallel_pair f g).map limits.walking_parallel_pair_hom.right

Now limits.equalizer.ι f g (see the comp hypothesis) is just an abbrevation:

abbreviation equalizer.ι : equalizer f g  X :=
limit.π (parallel_pair f g) zero

So I should be done with just a simple rewrite using comp, but I get the following error:

rewrite tactic failed, did not find instance of the pattern in the target expression
  h  limits.equalizer.ι f g

view this post on Zulip Calle Sönne (Oct 26 2019 at 12:58):

FYI on the line refine comp I had the exact same goal, only without the 2nd function composition. Then refine comp worked perfectly to eliminate one of the goals

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:04):

Before rw comp your local context is this:

comp : h ≫ limits.equalizer.ι f g = i ≫ limits.equalizer.ι f g
⊢ h ≫
      limits.limit.π (limits.parallel_pair f g) limits.walking_parallel_pair.zero ≫
        (limits.parallel_pair f g).map limits.walking_parallel_pair_hom.right =
    i ≫
      limits.limit.π (limits.parallel_pair f g) limits.walking_parallel_pair.zero ≫
        (limits.parallel_pair f g).map limits.walking_parallel_pair_hom.right

So rw comp will fail because rw works with syntactic equality, and the left hand side of h is not exactly mentioned in the goal.

view this post on Zulip Calle Sönne (Oct 26 2019 at 13:05):

So can I somehow rewrite the abbrevation first?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:06):

I have no idea how to steer abbreviations. I don't even know what they are.

view this post on Zulip Calle Sönne (Oct 26 2019 at 13:06):

ah :/

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:07):

Is the left hand side of the goal I posted definitionally equal to the left hand side of comp in your opinion?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:07):

there are too many >>'s, right?

view this post on Zulip Calle Sönne (Oct 26 2019 at 13:07):

but the last >> is the same on both sides

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:08):

Is >> left associative or right associative?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:08):

aah! It's right associative!

view this post on Zulip Calle Sönne (Oct 26 2019 at 13:08):

Wait now Im confused, isnt it both?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:09):

nonono

view this post on Zulip Calle Sönne (Oct 26 2019 at 13:09):

oh okay now I see

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:09):

#print notation 
#print notation +
#print notation ^

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:09):

I can never remember whether the difference in numbers means left or right

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:09):

For + the two numbers are the same, so + is left associative

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:09):

by which I mean "when Lean says a+b+c, it means (a+b)+c"

view this post on Zulip Calle Sönne (Oct 26 2019 at 13:10):

So I have to rewrite associativity first

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:10):

For ^ the numbers differ by 1, because it's right associative. So, yes.

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:11):

what's this lemma called?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:11):

actually, what's this axiom called?

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:11):

ha ha if I don't even know the names of the axioms this is a pretty good indication of how good I am at categories in Lean :D

view this post on Zulip Calle Sönne (Oct 26 2019 at 13:11):

category.assoc_symm

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:12):

Not assoc??

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:13):

wow you're right. Maybe it's because it's the other way around to usual because of the different conventions.

view this post on Zulip Calle Sönne (Oct 26 2019 at 13:13):

I dont know but category.assoc_symm worked

view this post on Zulip Calle Sönne (Oct 26 2019 at 13:13):

Thank you. The proof is now completed

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:14):

#print notation 

Usual function composition is left associative, so the convention I guess is that assoc means (a*b)*c=a*(b*c) [for a general infix binary operator]

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:14):

and then you apply eq.symm and you get Scott's axiom.

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 13:18):

so the rewrite does work. I guess abbreviation really does not change even syntactic equality. Maybe the parser just unfolds it before even passing it to the kernel?

view this post on Zulip Kenny Lau (Oct 26 2019 at 15:00):

they're not lemmas they're defs

view this post on Zulip Scott Morrison (Oct 27 2019 at 06:22):

It sounds like you've been making good progress. :-) I am actually in London right now, but only for two hours, before heading off to Frankfurt. I wish I could have stopped by Imperial to chat about categories in Lean, but my travel schedule is pretty constrained, so I'm just jumping back and forth for a week at Oberwolfach (for my "day job").


Last updated: May 12 2021 at 23:13 UTC