cone morphisms

Stream: new members

[Calle Sönne]

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]

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

that they form a category

[Kenny Lau]

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

[Calle Sönne]

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]

what imports do you need to get this running?

[Kevin Buzzard]

I should really learn this stuff at some point

[Calle Sönne]

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

open category_theory

namespace category_theory.limits
namespace is_limit

[Kevin Buzzard]

I still have errors

[Kevin Buzzard]

just make a new scratch file and minimise

[Kevin Buzzard]

unknown identifier 'equalizer' being the most serious one

[Kevin Buzzard]

unknown identifier 'f' being the next one

[Calle Sönne]

Oh I got variables. I will send them

[Calle Sönne]

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]

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]

Ok

[Kevin Buzzard]

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]

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]

Oh!

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

Oh, thats good to know thanks!

[Kevin Buzzard]

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]

yeah

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Calle Sönne]

wait it does?

[Kevin Buzzard]

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

[Kevin Buzzard]

You are using gg correctly

[Kevin Buzzard]

I was just thrown for a second

[Calle Sönne]

neither tidy or simp works

[Kevin Buzzard]

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]

Yeah I got to there now as well

[Calle Sönne]

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

[Calle Sönne]

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]

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

doesn't work either

[Kevin Buzzard]

  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]

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]

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

[Calle Sönne]

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

[Calle Sönne]

Because right now they are just maps between some objects

[Calle Sönne]

equalizer is just the object, not the cone

[Kevin Buzzard]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

in category_theory/limits/shapes/binary_products.lean

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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

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

[Kevin Buzzard]

Which London?

[Calle Sönne]

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

[Calle Sönne]

Is the := just like let?

[Kevin Buzzard]

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

[Calle Sönne]

Oh right the isomorphism

[Calle Sönne]

But then how do I continue the proof?

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

got it

[Kevin Buzzard]

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]

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

[Calle Sönne]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

[Calle Sönne]

Seems like a reasonable plan

[Calle Sönne]

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]

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

[Kevin Buzzard]

I cannot steer this stuff at all.

[Calle Sönne]

steer?

[Kevin Buzzard]

I don't even know the basics.

[Kevin Buzzard]

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

[Kevin Buzzard]

That's the only documentation I have ever seen.

[Calle Sönne]

ah

[Kevin Buzzard]

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]

But I can't work Scott's library

[Kevin Buzzard]

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]

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]

I made some progress!

[Calle Sönne]

but minor...

[Calle Sönne]

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]

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

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

[Calle Sönne]

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]

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

[Kevin Buzzard]

Now write some docs! ;-)

[Kevin Buzzard]

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]

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

[Calle Sönne]

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

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

[Kevin Buzzard]

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]

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]

Like how do I unfold

[Calle Sönne]

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]

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]

indeed, mono is a structure

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

[or rather why you were stuck 2 hours ago]

[Calle Sönne]

yeah exactly

[Calle Sönne]

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

[Calle Sönne]

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

[Calle Sönne]

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]

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]

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]

So can I somehow rewrite the abbrevation first?

[Kevin Buzzard]

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

[Calle Sönne]

ah :/

[Kevin Buzzard]

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

[Kevin Buzzard]

there are too many >>'s, right?

[Calle Sönne]

but the last >> is the same on both sides

[Kevin Buzzard]

Is >> left associative or right associative?

[Kevin Buzzard]

aah! It's right associative!

[Calle Sönne]

Wait now Im confused, isnt it both?

[Kevin Buzzard]

nonono

[Calle Sönne]

oh okay now I see

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Calle Sönne]

So I have to rewrite associativity first

[Kevin Buzzard]

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

[Kevin Buzzard]

what's this lemma called?

[Kevin Buzzard]

actually, what's this axiom called?

[Kevin Buzzard]

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]

category.assoc_symm

[Kevin Buzzard]

Not assoc??

[Kevin Buzzard]

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

[Calle Sönne]

I dont know but category.assoc_symm worked

[Calle Sönne]

Thank you. The proof is now completed

[Kevin Buzzard]

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

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

[Kevin Buzzard]

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]

they're not lemmas they're defs

[Scott Morrison]

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