empty cone

Stream: new members

[Calle Sönne]

I want to define the empty cone, given an object in a category C. I have tried to do as follows:

def empty_cone (X : C) : cone (functor.empty C) :=
{ X := X,
  π := nat_trans (functor.empty C) ((functor.const pempty).obj X)
}

by (trying to) mimic the way the constant functor is used in const.lean

I get the following error:

invalid field notation, type is not of the form (C ...) where C is a constant
  functor.const pempty
has type
  Type ? → Type ?

If I remove the .obj X I instead get:

type mismatch at application
  nat_trans (functor.empty C) (functor.const pempty)
term
  functor.const pempty
has type
  Type ? → Type ? : Type (max (?+1) (?+1))
but is expected to have type
  pempty ⥤ C : Type (max v u)
Additional information:
/home/calle/lean/sheaves/src/zeroobject.lean:14:7: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    nat_trans ?m_5 ?m_6
  has type
    Type (max ? ?) : Type ((max ? ?)+1)
  but is expected to have type
    (functor.const pempty).obj X ⟶ functor.empty C : Type v

[Reid Barton]

π := nat_trans is already wrong--π needs to be a specific natural transformation, not the type of natural transformation between ... and ...
Is there something like nat_trans.empty already? Otherwise, you can define it easily enough

[Calle Sönne]

I have not found anything like nat_trans.empty, so I will try to define it myself. Thank you.

[Calle Sönne]

Now that I have defined empty_trans I still get the same error:

def empty_cone (X : C) : cone (functor.empty C) :=
{ X := X,
  π := empty_trans ((functor.const pempty).obj X) (functor.empty C)
}

gives the error

invalid field notation, type is not of the form (C ...) where C is a constant
  functor.const pempty
has type
  Type ? → Type ?

Im probably not referring to the constant functor correctly, I tried copying the way it was done in const.lean but apparently I am doing something wrong. Do I need to refer to C explictly somehow?

[Calle Sönne]

This is an example of how its used in const.lean:

@[simp] lemma obj_obj (X : C) (j : J) : ((const J).obj X).obj j = X := rfl

[Reid Barton]

oh

[Reid Barton]

You probably have category.functor.const, not category_theory.functor.const.

[Reid Barton]

It's super annoying.

[Calle Sönne]

Thank you! I think it works because now Im getting a different error, hopefully a somewhat easier one though.

[Calle Sönne]

What does this error mean?

type mismatch at application
  empty_trans ((functor.const pempty).obj X)
term
  (functor.const pempty).obj X
has type
  pempty ⥤ C : Type (max ? v ? u)
but is expected to have type
  Type ? : Type (?+1)
Additional information:
/home/calle/lean/sheaves/src/zeroobject.lean:17:7: context: switched to simple application elaboration procedure because failed to use expected type to elaborate it, error message
  type mismatch, term
    empty_trans ?m_1 ?m_3
  has type
    Π (G : pempty ⥤ ?m_1), nat_trans ?m_3 G : Type (max (max ? ? ? ?) ? ?)
  but is expected to have type
    (functor.const pempty).obj X ⟶ functor.empty C : Type v

This is my code:

def empty_trans (F G : pempty ⥤ C) : nat_trans F G := by tidy

def empty_cone (X : C) : cone (functor.empty C) :=
{ X := X,
  π := empty_trans ((category_theory.functor.const pempty).obj X) (functor.empty C)
}

[Calle Sönne]

Why is it expecting Type ? : Type (?+1)? Is there some implicit argument to empty_trans that I am not providing?

[Calle Sönne]

I solved it, I just had to supply the category C to empty_trans as well

[Kenny Lau]

@Calle Sönne welcome back!

[Kenny Lau]

import category_theory.limits.cones category_theory.pempty

universes v u

namespace category_theory

open limits

variables {C : Type u} [𝒞 : category.{v} C]
include 𝒞

def empty_trans {F G : pempty ⥤ C} : nat_trans F G := by tidy

def empty_cone (X : C) : cone (functor.empty C) :=
{ X := X,
  π := empty_trans }

end category_theory

[Scott Morrison]

Looks like we should add these!

[Calle Sönne]

Thank you @Kenny Lau :)

[Johan Commelin]

Would it be safe to use clean to clean up after tidy in this case? I think it would be a lot of fun if we could use tactics for definitions.

[Johan Commelin]

@Kenny Lau Did you just define data using a tactic :rolling_on_the_floor_laughing: ?

[Kenny Lau]

I just copied his code for that part

[Calle Sönne]

In mathlib the empty functor is defined by tidy

[Calle Sönne]

def empty : pempty.{v+1} ⥤ C := by tidy

[Kenny Lau]

Kenny Lau Did you just define data using a tactic :rolling_on_the_floor_laughing: ?

when I tell people not to define data using a tactic, I always append "unless you know what you're doing" :P

[Johan Commelin]

Aah... I see what you're getting at (-;

[Calle Sönne]

Anyway I want to now define a zero object:

structure zero :=
(zero : C)
(initial : is_limit (empty_cone zero)
(terminal : is_colimit (empty_cocone zero)

but the line (initial : is_limit (empty_cone zero) gives the following error:

function expected at
  is_limit (empty_cone zero)
term has type
  Type (max u ?)

I am still not that familiar with classes, structures etc. in lean, should this be a class instead (like has_terminal, has_initial)?

[Kenny Lau]

you're missing closing brackets

[Calle Sönne]

In terminal.lean they define terminal as:

class has_terminal :=
(has_limits_of_shape : has_limits_of_shape.{v} pempty C)
...
abbreviation terminal [has_terminal.{v} C] : C := limit (functor.empty C)

Now using has_terminal makes it easy to say if any given category has a terminal object or not. Should I define a class has_zero similarly or is there a way to rephrase this using structures?

[Johan Commelin]

Isn't there a PR for zero object?

[Johan Commelin]

Maybe it's even merged already

[Calle Sönne]

I have not found anything, but it would be great if it exists. I want to eventually define an abelian category in lean

[Johan Commelin]

Have you talked with Scott?

[Johan Commelin]

https://github.com/leanprover-community/mathlib/pull/1445

[Calle Sönne]

No I have not talked with Scott, but this looks good! Kernels as well :o

[Scott Morrison]

I decided before I proceeded with zero objects and kernels I should go back and patch a few gaps in the API.

[Scott Morrison]

Particularly, for all the special shapes of limits a characterisation of an object being the limit, in the form \forall Y, (Y \hom X) \equiv ... for an appropriate ....

[Scott Morrison]

And then actually proving a bunch of the basic lemmas about the shapes we have already.

[Scott Morrison]

e.g. equalisers are monomorphisms, equalisers are "commutative" and "associative", etc., etc., to test out the existing limits API a bit further. Reid is right to complain that there haven't been enough lemmas relative to definitions so far in category_theory/limits/shapes/.

[Calle Sönne]

@Scott Morrison Is there anything you think I could help with?

[Scott Morrison]

@Calle Sönne, how about proving that equaliser f g \iso equaliser g f, or that mono (equaliser.\iota f g)?

In some sense the real problem is to explain what went wrong when you tried to implement your preferred pencil-and-paper proofs of these facts in Lean. The limits API still (...) needs work, and having people attempt to fill in some basic things like these and report back how it goes would be super useful.

[Scott Morrison]

(I have an idea of what I want to add to the limits API, which I think would make both of these questions easier, but I'm happy not to spoil it for you. :-)

[Calle Sönne]

Sounds good!

[Calle Sönne]

How do you use abbrevations? I have the following abbrevations:

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

@[simp, reassoc] lemma equalizer.condition : equalizer.ι f g ≫ f = equalizer.ι f g ≫ g :=
begin
  erw limit.w (parallel_pair f g) walking_parallel_pair_hom.left,
  erw limit.w (parallel_pair f g) walking_parallel_pair_hom.right
end

abbreviation equalizer.lift {W : C} (k : W ⟶ X) (h : k ≫ f = k ≫ g) : W ⟶ equalizer f g :=
limit.lift (parallel_pair f g) (fork.of_ι k h)
end

I want to combine them as:
lean have H1 : equalizer f g ⟶ equalizer g f, exact ((equalizer g f).lift (equalizer f g).ι (equalizer f g).condition)
But this gives the error

invalid field notation, type is not of the form (C ...) where C is a constant
  limits.equalizer g f
has type
  C

[Johan Commelin]

Unrelated: have is for propositions. Your morphism is data, so you need let H1 : ...

[Calle Sönne]

Thank you

[Johan Commelin]

Next, (equalizer g f).lift will try to see if (equalizer g f) is a term of type equalizer _ _

[Johan Commelin]

But it is not.

[Johan Commelin]

So you should simply write equalizer.lift _ _

[Calle Sönne]

I see, thank you

[Johan Commelin]

Does it work now?

[Calle Sönne]

Yeah