# Zulip Chat Archive

## Stream: new members

### Topic: cone morphisms

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

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

#### Kenny Lau (Oct 24 2019 at 17:08):

that they form a category

#### Kenny Lau (Oct 24 2019 at 17:09):

that also means you shouldn't use `cone_morphism`

explicitly, but rather `A \hom B`

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

#### Kevin Buzzard (Oct 26 2019 at 10:48):

what imports do you need to get this running?

#### Kevin Buzzard (Oct 26 2019 at 10:49):

I should really learn this stuff at some point

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

#### Kevin Buzzard (Oct 26 2019 at 10:50):

I still have errors

#### Kevin Buzzard (Oct 26 2019 at 10:50):

just make a new scratch file and minimise

#### Kevin Buzzard (Oct 26 2019 at 10:51):

`unknown identifier 'equalizer'`

being the most serious one

#### Kevin Buzzard (Oct 26 2019 at 10:52):

`unknown identifier 'f'`

being the next one

#### Calle Sönne (Oct 26 2019 at 10:54):

Oh I got variables. I will send them

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

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

#### Calle Sönne (Oct 26 2019 at 10:55):

Ok

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

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

#### Kevin Buzzard (Oct 26 2019 at 10:59):

Oh!

#### Kevin Buzzard (Oct 26 2019 at 11:00):

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

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

#### Calle Sönne (Oct 26 2019 at 11:03):

Oh, thats good to know thanks!

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

#### Calle Sönne (Oct 26 2019 at 11:04):

yeah

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

"?

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

#### Calle Sönne (Oct 26 2019 at 11:07):

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

#### Kevin Buzzard (Oct 26 2019 at 11:08):

Does `\gg`

do composition in "the wrong order"?

#### Kevin Buzzard (Oct 26 2019 at 11:08):

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

#### Calle Sönne (Oct 26 2019 at 11:09):

wait it does?

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

#### Kevin Buzzard (Oct 26 2019 at 11:09):

You are using gg correctly

#### Kevin Buzzard (Oct 26 2019 at 11:10):

I was just thrown for a second

#### Calle Sönne (Oct 26 2019 at 11:10):

neither tidy or simp works

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

#### Calle Sönne (Oct 26 2019 at 11:12):

Yeah I got to there now as well

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

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

#### Kevin Buzzard (Oct 26 2019 at 11:15):

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

doesn't work either

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

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

#### Kevin Buzzard (Oct 26 2019 at 11:19):

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

#### Calle Sönne (Oct 26 2019 at 11:22):

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

#### Calle Sönne (Oct 26 2019 at 11:22):

Because right now they are just maps between some objects

#### Calle Sönne (Oct 26 2019 at 11:22):

equalizer is just the object, not the cone

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

#### Scott Morrison (Oct 26 2019 at 11:23):

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

#### Scott Morrison (Oct 26 2019 at 11:24):

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

#### Scott Morrison (Oct 26 2019 at 11:24):

in `category_theory/limits/shapes/binary_products.lean`

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

#### Scott Morrison (Oct 26 2019 at 11:26):

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

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

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

#### Scott Morrison (Oct 26 2019 at 11:31):

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

#### Kevin Buzzard (Oct 26 2019 at 11:31):

Which London?

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

#### Calle Sönne (Oct 26 2019 at 11:42):

Is the := just like let?

#### Kevin Buzzard (Oct 26 2019 at 11:42):

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

#### Calle Sönne (Oct 26 2019 at 11:42):

Oh right the isomorphism

#### Calle Sönne (Oct 26 2019 at 11:43):

But then how do I continue the proof?

#### Kevin Buzzard (Oct 26 2019 at 11:43):

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

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

#### Kevin Buzzard (Oct 26 2019 at 11:44):

got it

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

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

#### Calle Sönne (Oct 26 2019 at 11:47):

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

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

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

#### Calle Sönne (Oct 26 2019 at 11:50):

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

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

#### Calle Sönne (Oct 26 2019 at 11:51):

Seems like a reasonable plan

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

#### Calle Sönne (Oct 26 2019 at 11:54):

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

#### Kevin Buzzard (Oct 26 2019 at 11:54):

I cannot steer this stuff at all.

#### Calle Sönne (Oct 26 2019 at 11:54):

steer?

#### Kevin Buzzard (Oct 26 2019 at 11:58):

I don't even know the basics.

#### Kevin Buzzard (Oct 26 2019 at 11:58):

#### Kevin Buzzard (Oct 26 2019 at 11:58):

That's the only documentation I have ever seen.

#### Calle Sönne (Oct 26 2019 at 11:58):

ah

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

#### Kevin Buzzard (Oct 26 2019 at 11:59):

But I can't work Scott's library

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

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

#### Calle Sönne (Oct 26 2019 at 12:03):

I made some progress!

#### Calle Sönne (Oct 26 2019 at 12:04):

but minor...

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

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

#### Calle Sönne (Oct 26 2019 at 12:05):

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

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

#### Calle Sönne (Oct 26 2019 at 12:18):

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

#### Kevin Buzzard (Oct 26 2019 at 12:18):

Now write some docs! ;-)

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

#### Kevin Buzzard (Oct 26 2019 at 12:19):

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

#### 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) :=

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

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

#### Calle Sönne (Oct 26 2019 at 12:26):

Like how do I unfold

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

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

#### Kevin Buzzard (Oct 26 2019 at 12:28):

indeed, `mono`

is a structure

#### Kevin Buzzard (Oct 26 2019 at 12:28):

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

#### Kevin Buzzard (Oct 26 2019 at 12:30):

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

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

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

#### Kevin Buzzard (Oct 26 2019 at 12:46):

[or rather why you were stuck 2 hours ago]

#### Calle Sönne (Oct 26 2019 at 12:47):

yeah exactly

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

#### Calle Sönne (Oct 26 2019 at 12:48):

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

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

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

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

#### Calle Sönne (Oct 26 2019 at 13:05):

So can I somehow rewrite the abbrevation first?

#### Kevin Buzzard (Oct 26 2019 at 13:06):

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

#### Calle Sönne (Oct 26 2019 at 13:06):

ah :/

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

#### Kevin Buzzard (Oct 26 2019 at 13:07):

there are too many >>'s, right?

#### Calle Sönne (Oct 26 2019 at 13:07):

but the last >> is the same on both sides

#### Kevin Buzzard (Oct 26 2019 at 13:08):

Is >> left associative or right associative?

#### Kevin Buzzard (Oct 26 2019 at 13:08):

aah! It's right associative!

#### Calle Sönne (Oct 26 2019 at 13:08):

Wait now Im confused, isnt it both?

#### Kevin Buzzard (Oct 26 2019 at 13:09):

nonono

#### Calle Sönne (Oct 26 2019 at 13:09):

oh okay now I see

#### Kevin Buzzard (Oct 26 2019 at 13:09):

#print notation ≫ #print notation + #print notation ^

#### Kevin Buzzard (Oct 26 2019 at 13:09):

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

#### Kevin Buzzard (Oct 26 2019 at 13:09):

For `+`

the two numbers are the same, so `+`

is left associative

#### Kevin Buzzard (Oct 26 2019 at 13:09):

by which I mean "when Lean says `a+b+c`

, it means `(a+b)+c`

"

#### Calle Sönne (Oct 26 2019 at 13:10):

So I have to rewrite associativity first

#### Kevin Buzzard (Oct 26 2019 at 13:10):

For `^`

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

#### Kevin Buzzard (Oct 26 2019 at 13:11):

what's this lemma called?

#### Kevin Buzzard (Oct 26 2019 at 13:11):

actually, what's this axiom called?

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

#### Calle Sönne (Oct 26 2019 at 13:11):

category.assoc_symm

#### Kevin Buzzard (Oct 26 2019 at 13:12):

Not `assoc`

??

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

#### Calle Sönne (Oct 26 2019 at 13:13):

I dont know but category.assoc_symm worked

#### Calle Sönne (Oct 26 2019 at 13:13):

Thank you. The proof is now completed

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

#### Kevin Buzzard (Oct 26 2019 at 13:14):

and then you apply `eq.symm`

and you get Scott's axiom.

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

#### Kenny Lau (Oct 26 2019 at 15:00):

they're not `lemma`

s they're `def`

s

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