Zulip Chat Archive

Stream: maths

Topic: limits 2.0


view this post on Zulip Reid Barton (Nov 02 2018 at 21:49):

@Scott Morrison, how are the new limits coming along? I took a peek at community mathlib and it looks like things are happening!

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:27):

Yes, I think it's pretty close now.

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:28):

I spent (too long) trying to follow the argument Emily Riehl uses in her book to explain why (C \func D) has limits of shape J whenever D has limits of shape J.

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:28):

It turned out to be really gross to formalise.

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:29):

(She first explains that (discrete C) \func D has those limits, and then shows that the forgetful functor (C \func D) \func ((discete C) \func D) creates limits.)

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:30):

So I've just switched to much more directly constructing limits in (C \func D), and then showing that the evaluation functor ev_X : (C \func D) \func D preserves limits.

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:30):

This seems to be nice and clean, so I think I'm happy with that for now.

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:34):

Still to do:
1. copy-and-pasting for all the dual notions (I think I'm not ready to make tactics for this yet)
2. quite a bit of cleanup...
3. port a few examples from the old development
4. a few @[simp] lemmas describing how colimit.pre and colimit.desc work in the category of types, which I got confused about...

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:34):

If anyone wants to hack on the limits-others-new branch on leanprover-community, feel free. :-)

view this post on Zulip Scott Morrison (Nov 02 2018 at 22:35):

oh, and 5. I need to try porting the construction of limits from equalizers and products to the new setup.

view this post on Zulip Reid Barton (Nov 02 2018 at 23:59):

Sounds good! I fixed the build by making auto_cases work on quotients again and I also made a couple of minor simplifications which you might still be interested in.

view this post on Zulip Reid Barton (Nov 02 2018 at 23:59):

I think I will try to check off a few of the items on my "basic category theory" list, then.

view this post on Zulip Johan Commelin (Nov 03 2018 at 10:08):

@Scott Morrison I'm happy to help out with some of the dualising work. Which parts would I best start to work on?

view this post on Zulip Johan Commelin (Nov 03 2018 at 10:09):

Are certain files pretty stable, and others in flux? Or can I just start anywhere?

view this post on Zulip Reid Barton (Nov 03 2018 at 15:17):

lol, I started looking at the new limits in more detail, and got annoyed by all these const J C X with so many explicit arguments, and tried making at least the C argument implicit (X : C), and immediately got a bunch of errors related to coercions

view this post on Zulip Reid Barton (Nov 03 2018 at 15:18):

No wonder Scott went on that rant recently :)

view this post on Zulip Scott Morrison (Nov 03 2018 at 22:36):

That rant got started after I tried making a coercion all the way from C to J \func C, so you really could just write X instead of const J C X, as we do in the real world.

view this post on Zulip Scott Morrison (Nov 03 2018 at 22:36):

Let's just say it didn't work out. :-)

view this post on Zulip Scott Morrison (Nov 04 2018 at 02:43):

(deleted a dumb question; I really should check the statement when I'm having trouble proving something....)

view this post on Zulip Scott Morrison (Nov 04 2018 at 10:33):

Hi @Reid Barton, any chance you'd like to help me with any of the following sorries, on the HEAD of limits-others-new:

def is_limit.of_extensions_iso (h : is_iso t.extensions) : is_limit t :=
{ lift := λ s, (inv t.extensions) s.X s.π,
  fac' := begin tidy, sorry, end,
  uniq' := begin tidy, sorry, end }

view this post on Zulip Scott Morrison (Nov 04 2018 at 10:33):

def cone.of_representable_cones (F : J ⥤ C) [r : representable F.cones] : cone F :=
{ X := r.X,
  π := r.w.hom r.X (𝟙 r.X) }

def extensions_iso_of_representable_cones (F : J ⥤ C) [r : representable F.cones] :
  is_iso (cone.of_representable_cones F).extensions :=
{ inv :=
  { app := λ X, r.w.inv X,
    naturality' := λ X Y f, begin tidy, sorry end },
  hom_inv_id' := begin tidy, sorry end,
  inv_hom_id' := sorry }

def has_limit_of_cones_representable (F : J ⥤ C) [r : representable F.cones] : has_limit F :=
{ cone := cone.of_representable_cones F,
  is_limit := is_limit.of_extensions_iso (extensions_iso_of_representable_cones F) }

def cones_representable_of_has_limit (F : J ⥤ C) [has_limit F] : representable F.cones :=
{ X := (has_limit.cone F).X,
  w := (has_limit.is_limit F).natural_equiv }

view this post on Zulip Scott Morrison (Nov 04 2018 at 10:36):

For context, here F.cones is the functor C^op \to Type so F.cones X is the type of natural transformations X \natt F, and t.extensions, for t a cone, is the natural transformation yoneda C t.X ⟶ F.cones given by whiskering a cone.

view this post on Zulip Scott Morrison (Nov 04 2018 at 10:36):

I'm finding these sorries very confusing. I'm not sure that this is a sign that the design is bad, just that this is a corner of basic category theory that no one ever writes out the details of. :-)

view this post on Zulip Reid Barton (Nov 04 2018 at 23:12):

I managed to prove them. It took me 2 hours to write about a dozen lines of code.

view this post on Zulip Scott Morrison (Nov 04 2018 at 23:34):

Awesome!

view this post on Zulip Scott Morrison (Nov 04 2018 at 23:42):

1. I'm glad it took you a while, it makes me feel less incompetent. :-)

view this post on Zulip Scott Morrison (Nov 04 2018 at 23:42):

2. Is there something we can learn from this having been hard??

view this post on Zulip Scott Morrison (Nov 04 2018 at 23:43):

It seems like a bad sign that something a textbook contents itself with merely stating, was a struggle in the library.

view this post on Zulip Reid Barton (Nov 04 2018 at 23:45):

I also just proved that equalizers are monomorphisms, since that was the other sorry

view this post on Zulip Reid Barton (Nov 04 2018 at 23:46):

and the lemma I needed to prove it (is_limit.hom_eq; maybe not a very good name? but it's hard to think of different names for all the different aspects of the universal property) is something that I used extensively in my homotopy theory library

view this post on Zulip Scott Morrison (Nov 04 2018 at 23:47):

Ah, thanks!

view this post on Zulip Reid Barton (Nov 04 2018 at 23:48):

I tend to think of it as a general "extensionality" property for limits, since it generalizes funext/prod.ext

view this post on Zulip Scott Morrison (Nov 04 2018 at 23:49):

It's a close relative of

@[extensionality] lemma limit.hom_ext {F : J ⥤ C} [has_limit F] {X : C}
  {f g : X ⟶ limit F}
  (w : ∀ j, f ≫ limit.π F j = g ≫ limit.π F j) : f = g :=

view this post on Zulip Scott Morrison (Nov 04 2018 at 23:50):

I wonder if we should unify them.

view this post on Zulip Reid Barton (Nov 04 2018 at 23:51):

Oh yeah. Isn't it the same thing?

view this post on Zulip Reid Barton (Nov 04 2018 at 23:51):

I think you should never prove anything about limit, always is_limit

view this post on Zulip Reid Barton (Nov 04 2018 at 23:51):

and then provide a wrapper for limit if that seems useful

view this post on Zulip Reid Barton (Nov 04 2018 at 23:52):

because there are lots of ways you could get your hands on a limit cone, only one of which is from the category's chosen limits (if it even has them)

view this post on Zulip Reid Barton (Nov 04 2018 at 23:53):

I also did this for is_equalizer.mono

view this post on Zulip Scott Morrison (Nov 04 2018 at 23:54):

Hmm, I'm on the fence here.

view this post on Zulip Scott Morrison (Nov 04 2018 at 23:55):

One can of course, with some hassle, use theorems stated in terms of limit in situations where you just have an is_limit, by using is_limit.ext to prove that your is_limit is actually equal to the one limit thinks it's using.

view this post on Zulip Reid Barton (Nov 04 2018 at 23:56):

2. Is there something we can learn from this having been hard??

I wondered about this too. My initial feeling was that there were too many definitions built up (cones/representable) with too little supporting theory, but upon reflection this didn't really seem to stand up, considering the eventually successful proof was to think hard about the actual fact which was needed, and then have Lean observe that it was enough.

view this post on Zulip Reid Barton (Nov 04 2018 at 23:57):

In lean-homotopy-theory I have many, many applications of facts like "a pushout of a pushout is a pushout" and I work in a setting where the category is not assumed to have pushouts

view this post on Zulip Reid Barton (Nov 04 2018 at 23:58):

So that's one obstruction to rewriting things in terms of chosen limits

view this post on Zulip Reid Barton (Nov 05 2018 at 00:00):

But it is actually also just more practical in general, because it saves you from transporting the relevant facts across an isomorphism, and dealing with isomorphisms is disproportionately difficult in Lean

view this post on Zulip Scott Morrison (Nov 05 2018 at 00:02):

okay --- so the question is: how much of the stuff I currently have written in terms of limit should we:
1) remove (for now)
2) rewrite in terms of is_limit, possible re-adding wrappers
3) leave as is?

view this post on Zulip Reid Barton (Nov 05 2018 at 00:04):

Well, I suggest 3, with 2 as needed

view this post on Zulip Reid Barton (Nov 05 2018 at 00:05):

Some things, like "limit F is functorial in F", really need limit

view this post on Zulip Reid Barton (Nov 05 2018 at 00:10):

Some other things like limit.pre and limit.pre_pre which involve multiple limit cones are in a sort of middle area. I'm fine with just leaving them how they are until someone wants an is_limit version.

view this post on Zulip Reid Barton (Nov 05 2018 at 00:13):

Oh, I guess I missed that these functions only require limits of the specific diagrams which appear now. That means you can also use them as their is_limit equivalents, at least in principle...

view this post on Zulip Reid Barton (Nov 05 2018 at 00:14):

Still, I don't see any particular advantage to defining, say, instance : mono (equalizer.ι f g) directly over the way that I did it.

view this post on Zulip Scott Morrison (Nov 05 2018 at 00:14):

I agree there. I think this was my mistake, being over-eager to prove things in the limit variation.

view this post on Zulip Reid Barton (Nov 05 2018 at 00:16):

Now I remember that I actually considered a design like this at one point in lean-homotopy-theory, where you have a specific class coproduct a b which provides a chosen coproduct of two specific objects. I never tried it out though

view this post on Zulip Scott Morrison (Nov 05 2018 at 00:16):

I guess my hesitation is that switching to is_limit for, for example:

def limit.pre (F : J ⥤ C) [has_limit F] (E : K ⥤ J) [has_limit (E ⋙ F)] : limit F ⟶ limit (E ⋙ F) :=
limit.lift (E ⋙ F)
{ X := limit F,
  π := { app := λ k, limit.π F (E k) } }

involves more variables.

view this post on Zulip Scott Morrison (Nov 05 2018 at 00:17):

The has_limit typeclasses each have to turn into a cone and an is_limit.

view this post on Zulip Scott Morrison (Nov 05 2018 at 00:17):

A somewhat scary option is to make is_limit a typeclass again, and make has_limit be inferrable from it...

view this post on Zulip Scott Morrison (Nov 05 2018 at 00:18):

It would be nice if the "typeclass inferred wasn't the one expected" class of errors were all solved by appropriate subsingleton instances...

view this post on Zulip Reid Barton (Nov 05 2018 at 00:19):

Right, so there are just two differences really: whether or not cone and is_limit are bundled together, and whether or not the pair is a type class argument

view this post on Zulip Reid Barton (Nov 05 2018 at 00:21):

Well, has_limit is not even a subsingleton, unfortunately :)

view this post on Zulip Scott Morrison (Nov 05 2018 at 00:22):

yeah, so at the moment we're in the upside situation: the typeclass is not a singleton, the non-typeclass is...

view this post on Zulip Scott Morrison (Nov 05 2018 at 00:22):

yuck! :-)

view this post on Zulip Reid Barton (Nov 05 2018 at 00:24):

Well anyways, this just makes me even more want to leave all the limit.* functions alone (besides limit.hom_ext I guess) and just wait and see, in practice, how necessary it is to do "cone-based reasoning" vs "limit-based reasoning", for lack of better terms, and how inconvenient it is to feed the limit cones you want into limit.*

view this post on Zulip Scott Morrison (Nov 05 2018 at 00:27):

okay, great :-)

view this post on Zulip Reid Barton (Nov 05 2018 at 00:29):

Hmm, does using limit.hom_ext as an [extensionality] lemma really work?

view this post on Zulip Reid Barton (Nov 05 2018 at 00:32):

I guess it might. I wasn't brave enough to try to make is_limit.hom_ext one too, that seems like it would be bad since it would match basically everything.

view this post on Zulip Scott Morrison (Nov 05 2018 at 02:00):

@[extensionality] lemma limit.hom_ext seems to work great!

view this post on Zulip Johan Commelin (Nov 05 2018 at 07:59):

I really need a lot of coblah at the moment. Which approach are we going to take? I advocate putting every costatement right after statement. So the highest level of interleaving that is possible.
I think every other approach will lead to things going hopelessly out of sync.

view this post on Zulip Scott Morrison (Nov 05 2018 at 09:50):

Hmm, I have been keeping them pretty separate. :-(

view this post on Zulip Scott Morrison (Nov 05 2018 at 09:51):

Mostly so that I can work on limits, and then once it has settled down doing a bunch of copy-paste.

view this post on Zulip Scott Morrison (Nov 05 2018 at 09:52):

Which bits of coblah have you been needing?

view this post on Zulip Scott Morrison (Nov 05 2018 at 09:52):

(Are you guys all at Freiburg?)

view this post on Zulip Johan Commelin (Nov 05 2018 at 09:52):

Mostly coequalizers

view this post on Zulip Johan Commelin (Nov 05 2018 at 09:53):

There is Kenny, Johannes, Rob, Tobias, Cyril, Patrick, Michael, and me

view this post on Zulip Scott Morrison (Nov 05 2018 at 09:54):

Did you do it yet?

view this post on Zulip Scott Morrison (Nov 05 2018 at 09:54):

It looks like I could dualize everything in equalizers.lean on short notice.

view this post on Zulip Johan Commelin (Nov 05 2018 at 09:54):

No, I got stuck somewhere.

view this post on Zulip Scott Morrison (Nov 05 2018 at 09:55):

(I have been synchronizing the two halves of things using a split window editor, and going line by line.)

view this post on Zulip Scott Morrison (Nov 05 2018 at 09:55):

Is it okay if I do that now?

view this post on Zulip Johan Commelin (Nov 05 2018 at 09:55):

Yeah cool. Then I'll try to do some sheaves stuff again.

view this post on Zulip Scott Morrison (Nov 05 2018 at 10:13):

ok, done!

view this post on Zulip Scott Morrison (Nov 05 2018 at 10:13):

(with one sorry, that I'm very confused about. we may have to ask Reid about it)

view this post on Zulip Kenny Lau (Nov 05 2018 at 10:15):

@Scott Morrison do you want to skype with us?

view this post on Zulip Johan Commelin (Nov 05 2018 at 10:29):

@Scott Morrison Thanks for adding coequalizers!

view this post on Zulip Johan Commelin (Nov 05 2018 at 10:32):

Hmmm, I'm also needing coproducts. But I don't want to overload you...

view this post on Zulip Scott Morrison (Nov 05 2018 at 10:38):

Didn't I do those earlier this evening? Maybe you need to fetch. :-)

view this post on Zulip Reid Barton (Nov 05 2018 at 13:22):

(with one sorry, that I'm very confused about. we may have to ask Reid about it)

I fixed it.

view this post on Zulip Reid Barton (Nov 05 2018 at 14:02):

@Scott Morrison do you mind if at some point I merge mathlib master into the limits branch?

view this post on Zulip Scott Morrison (Nov 05 2018 at 18:48):

Thanks for the fix! No problem, merge with master whenever you like.

view this post on Zulip Scott Morrison (Nov 05 2018 at 18:48):

Sorry that my git hygiene has been so poor on this branch. We should also rebase and do some squashing.

view this post on Zulip Johan Commelin (Nov 05 2018 at 18:51):

No, please don't do that on public branches.

view this post on Zulip Johan Commelin (Nov 05 2018 at 18:52):

I think we should only squash when merging into mathlib.

view this post on Zulip Johan Commelin (Nov 05 2018 at 18:52):

Not when multiple people are working on it.

view this post on Zulip Scott Morrison (Nov 06 2018 at 08:03):

@Johan Commelin, two questions/suggestions:
1) don't you think we should do "easy" sheaves _first_, before the ones with sites and coverages?
2) for your definition def sieve : presheaf X (Type v) :=, I think it's much easier if you start off working in tactic mode, and have each of the four maps you're building, so that it's easy to inspect their types. Once everything works you can obfuscate everything into term mode if you prefer. :-)

view this post on Zulip Johan Commelin (Nov 06 2018 at 08:18):

Thanks for the feedback.
1) It might be a good idea. But I really want sheaves on a basis. And a basis is a site... And I think I'm almost there.
2) This sounds like a very good plan!

view this post on Zulip Scott Morrison (Nov 06 2018 at 10:09):

@Reid Barton, @Johan Commelin, I'm close to "sticking a fork in it and saying it's done" on the new limits branch. It's certainly not exhaustively complete, but I want to leave it for a while. Do you think I should re-PR it?

view this post on Zulip Scott Morrison (Nov 06 2018 at 10:09):

It all compiles, and the only sorries are inside comments. :-)

view this post on Zulip Johan Commelin (Nov 06 2018 at 10:10):

Cool! We are making some progress with sheaves. Maybe let's wait for a couple hours and see what happens there?

view this post on Zulip Scott Morrison (Nov 06 2018 at 10:11):

Of course, it's still conspicuously missing examples!

view this post on Zulip Scott Morrison (Nov 06 2018 at 10:11):

Really I'd like to see all the limits and filtered colimits for CommRing in place...

view this post on Zulip Johan Commelin (Nov 06 2018 at 10:25):

@Scott Morrison Would it be an idea to use coproduct instead of limits.sigma? I think that is just as readable, and less confusing with the existing sigma?

view this post on Zulip Scott Morrison (Nov 06 2018 at 10:26):

I'm open. If we change, we should change prod to binary_product, sum to binary_coproduct, pi to product and sigma to coproduct.

view this post on Zulip Scott Morrison (Nov 06 2018 at 10:27):

I actually find calling it sigma helpful, at this point. :-)

view this post on Zulip Scott Morrison (Nov 06 2018 at 10:28):

(because it's just the same as the built-in sigma, just for arbitrary categories, not just Type)

view this post on Zulip Johan Commelin (Nov 06 2018 at 10:28):

Well, we were writing sigma.map and it took a while to figure out that we actually wanted limits.sigma.map.

view this post on Zulip Scott Morrison (Nov 06 2018 at 10:28):

Yeah, okay, I've done that too.

view this post on Zulip Johan Commelin (Nov 06 2018 at 10:29):

Another point, this sigma.map could be a bit more general. The domains of f and g could differ. (In our case we have c × c and c, and they are related via the projections.

view this post on Zulip Johan Commelin (Nov 06 2018 at 10:29):

Does it make sense what I'm saying?

view this post on Zulip Johan Commelin (Nov 06 2018 at 10:30):

We would need a map h : beta → beta' such that g \circ h = f or something like that.

view this post on Zulip Reid Barton (Nov 06 2018 at 16:02):

Perhaps it would be worthwhile to make a list of remaining category theory ingredients needed for schemes and perfectoid spaces?

view this post on Zulip Kevin Buzzard (Nov 06 2018 at 16:05):

@Johan Commelin My student @Ramon Fernandez Mir wants sheaves on a basis. Is there a way he can look at your code?

view this post on Zulip Patrick Massot (Nov 06 2018 at 16:08):

Johan and Johannes are currently working hard on this, the situation will probably be rather different in 24 hours.

view this post on Zulip Johan Commelin (Nov 06 2018 at 16:12):

Yes, look at the sheaf branch on community mathlib.

view this post on Zulip Johan Commelin (Nov 06 2018 at 16:12):

We are pretty close to a definition for sheaves of types on a basis.

view this post on Zulip Johan Commelin (Nov 06 2018 at 16:13):

@Scott Morrison We are collecting holes in the api in the sheaf.lean file on the sheaf branch.

view this post on Zulip Johan Commelin (Nov 06 2018 at 16:34):

@Kevin Buzzard So I think we can have sheaves of types on a basis rather soon. Generalising to sheaves of groups/rings shouldn't be hard. (We will need to prove that the respective categories have pullbacks and equalizers and such... but I think that should be doable. If @Ramon Fernandez Mir wants, he could also look into that.)
The bigger problem is extending sheaves on a basis to sheaves on the topology. Defining the functor on presheaves is not hard (I already did that a while ago); but proving that it preserves sheaves (it is even an equivalence!) seems to be harder.

view this post on Zulip Johan Commelin (Nov 06 2018 at 16:35):

At least it will be hard if I want to use the general machinery of morphisms of sites.

view this post on Zulip Johan Commelin (Nov 06 2018 at 16:36):

Maybe this special case is easier... it might help that it is an equivalence.

view this post on Zulip Kevin Buzzard (Nov 06 2018 at 16:36):

So what does this currently look like in Lean? I've not been following developments in category theory since term started.

view this post on Zulip Johan Commelin (Nov 06 2018 at 16:37):

Look at the sheaf branch on community-mathlib.

view this post on Zulip Johan Commelin (Nov 06 2018 at 16:38):

Most of the proofs stay really close to the level that we as mathematicians would use. Sometimes you have to go into gory details, which means we didn't set up enough rules for obviously. But that should be easy to improve.

view this post on Zulip Kevin Buzzard (Nov 06 2018 at 16:38):

no, I mean what does the definition of a sheaf look like?

view this post on Zulip Kevin Buzzard (Nov 06 2018 at 16:38):

Oh I see, sorry, I missed the first message

view this post on Zulip Johan Commelin (Nov 06 2018 at 16:39):

On the sheaf branch, you want to look at category_theory/sheaf.lean

view this post on Zulip Johan Commelin (Nov 06 2018 at 16:39):

I still need to prove a fundamental lemma, which reduces the sheaf condition to the usual thing in the case of topological spaces.

view this post on Zulip Kevin Buzzard (Nov 06 2018 at 16:40):

great thanks, this is all we needed to know right now. Thanks a lot!

view this post on Zulip Johan Commelin (Nov 06 2018 at 18:49):

This is throwing up type class issues again:

namespace lattice.complete_lattice

open lattice

variables {X : Type u} [complete_lattice X]

instance : has_limits.{u u} X :=
{ cone := λ J _ F, -- now I have two instances of small_category J -- HELP
  { X := infi F.obj,
    π := _ },
  is_limit := _ }

end lattice.complete_lattice

view this post on Zulip Reid Barton (Nov 06 2018 at 19:00):

I think the problem is actually that you have 0 instances

view this post on Zulip Reid Barton (Nov 06 2018 at 19:01):

I put by exactI before infi, and now at least that line is accepted.

view this post on Zulip Reid Barton (Nov 06 2018 at 19:01):

(Or, possibly you have some different imports/mathlib commit than I do.)

view this post on Zulip Reid Barton (Nov 06 2018 at 19:03):

If you want to avoid by exactI tricks then you could probably define the limits of X in a separate top-level definition, taking care to put the arguments in the correct order for has_limits, and also to put the [small_category J] bit to the left of the colon

view this post on Zulip Reid Barton (Nov 06 2018 at 19:05):

By the way, @Scott Morrison, is there a particular reason for the duplication between has_limits_of, has_limits_of_shapes, has_limits? Why isn't for example has_limits C = Π {J : Type v} [small_category J], has_limits_of_shape J C?

view this post on Zulip Johan Commelin (Nov 06 2018 at 19:09):

@Reid Barton Let me see if I understand what you are suggesting...

view this post on Zulip Reid Barton (Nov 06 2018 at 19:09):

(Obviously it can't make that big a difference, I just intuitively feel that this duplication will lead to unpacking/repacking down the line. But maybe it's actually more convenient to use for some other reason.)

view this post on Zulip Reid Barton (Nov 06 2018 at 19:11):

@Johan Commelin Actually limits/types.lean is already written in the style I was suggesting, so you can use that as an example.

view this post on Zulip Johan Commelin (Nov 06 2018 at 19:36):

@Reid Barton It's working quite well! Thanks! Now I'm left fighting plift:

namespace lattice.complete_lattice

open lattice

variables {X : Type u} [complete_lattice X]
variables {J : Type u} [small_category J]

def limit (F : J  X) : cone F :=
{ X := infi F.obj,
  π := { app := λ j, plift.up (infi_le _ j) } }

def limit_is_limit (F : J  X) : is_limit (limit F) :=
{ lift := λ s, plift.up $ le_infi (λ i, plift.down $ s.π i) }

instance : has_limits.{u u} X :=
{ cone := λ J hJ F, @limit _ _ J hJ F,
  is_limit := λ J hJ F, @limit_is_limit _ _ J hJ F }

instance : has_pullbacks.{u u} X := has_pullbacks_of_has_limits _

end lattice.complete_lattice

view this post on Zulip Johan Commelin (Nov 06 2018 at 19:37):

limit_is_limit is still broken. The plift.down is illegal.

view this post on Zulip Reid Barton (Nov 06 2018 at 19:39):

Probably because there is ulift involved too? I wonder why your limit was accepted?

view this post on Zulip Reid Barton (Nov 06 2018 at 19:39):

oh, I didn't notice the angle brackets!

view this post on Zulip Johan Commelin (Nov 06 2018 at 19:40):

I think the other problem has to do with the constant functor etc... I have to look into it...

view this post on Zulip Reid Barton (Nov 06 2018 at 19:40):

I need to do something about my terminal font. or maybe set up emacs to display them in different colors

view this post on Zulip Reid Barton (Nov 06 2018 at 19:41):

For has_pullbacks? Deleting _ worked for me

view this post on Zulip Reid Barton (Nov 06 2018 at 19:42):

(If using angle brackets for ulift.up, why not also for plift.up?)

view this post on Zulip Johan Commelin (Nov 06 2018 at 19:43):

Yes, maybe I should do that...

view this post on Zulip Johan Commelin (Nov 06 2018 at 19:55):

Done:

namespace lattice.complete_lattice

open lattice

variables {X : Type u} [complete_lattice X]
variables {J : Type u} [small_category J]

def limit (F : J  X) : cone F :=
{ X := infi F.obj,
  π := { app := λ j, ⟨⟨infi_le _ j⟩⟩ } }

def limit_is_limit (F : J  X) : is_limit (limit F) :=
{ lift := λ s, ⟨⟨le_infi (λ i, plift.down $ ulift.down $ s.π i)⟩⟩ }

instance : has_limits.{u u} X :=
{ cone := λ J hJ F, @limit _ _ J hJ F,
  is_limit := λ J hJ F, @limit_is_limit _ _ J hJ F }

instance : has_pullbacks.{u u} X := has_pullbacks_of_has_limits _

end lattice.complete_lattice

view this post on Zulip Scott Morrison (Nov 06 2018 at 21:29):

By the way, @Scott Morrison, is there a particular reason for the duplication between has_limits_of, has_limits_of_shapes, has_limits? Why isn't for example has_limits C = Π {J : Type v} [small_category J], has_limits_of_shape J C?

Oh, it didn't occur to me that this could be possible. I've only recently realised that you can put Pi types in typeclass arguments sometimes.
It sounds like a good idea.

view this post on Zulip Scott Morrison (Nov 07 2018 at 11:29):

@Johan Commelin please don't rely on 'theorems' like your

lemma cone.ext' {F : J ⥤ C} :
  ∀{x y : cone F} (eq : x.X = y.X), x.π == y.π → x = y ...

view this post on Zulip Scott Morrison (Nov 07 2018 at 11:29):

it will lead to tears.

view this post on Zulip Scott Morrison (Nov 07 2018 at 11:29):

If you replace the equalities with isos, it's fine.

view this post on Zulip Scott Morrison (Nov 07 2018 at 11:30):

(and the == with an appropriate composition)

view this post on Zulip Scott Morrison (Nov 07 2018 at 11:32):

It looks like you've made lots of progress on sheaves!!

view this post on Zulip Scott Morrison (Nov 07 2018 at 11:33):

ah, it seems you don't actually use cone.ext' anywhere, so I shouldn't get too upset about it. :-)

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 12:27):

yes, I removed to prove which used it afterwards, I couldn't apply it. so in the end I unfolded the proof in pullback.lift_id.

view this post on Zulip Scott Morrison (Nov 07 2018 at 12:37):

I've just pushed some work on sheaf.lean.

view this post on Zulip Scott Morrison (Nov 07 2018 at 12:38):

I moved a bunch of the API stuff you guys added to the limits branch, and then fixed the errors in comap.

view this post on Zulip Johan Commelin (Nov 07 2018 at 12:56):

@Scott Morrison Thanks a lot!

view this post on Zulip Johan Commelin (Nov 07 2018 at 14:58):

Is preorder (over U) going to create diamond issues? Here U : opens X and X is a type with a topology.

view this post on Zulip Johan Commelin (Nov 07 2018 at 19:24):

@Scott Morrison I saw that in the stuff on over categories you added right := punit.star a couple of times. Why is this necessary? I thought obviously was handling it. As a user I was very happy that I could ignore right when it was so trivial that you would like to think it didn't even exist.

view this post on Zulip Johan Commelin (Nov 07 2018 at 19:54):

Does mathlib have the indiscrete (codiscrete?) topology, and if so, what is its name?

view this post on Zulip Johan Commelin (Nov 07 2018 at 19:55):

git grep didn't find either of those...

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 20:01):

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 20:02):

this is the indiscrete topology

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:07):

Ok, but it doesn't have a name, I guess?

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:07):

I have now pushed site.trivial and site.discrete.

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:07):

They are the only sorry-free examples of sites we have so far.

view this post on Zulip Scott Morrison (Nov 07 2018 at 20:17):

@Johan Commelin, regarding right := punit.star. I did remove this, but I think only temporarily. The problem is that every field with an autoparam should be restated, otherwise the auto_param garbage clutters up the goal view, and sometimes gets in the way of elaboration. I want to restore obviously to left and right, but it will involve restating hom by hand, and I didn't want to do that on the spot.

view this post on Zulip Scott Morrison (Nov 07 2018 at 20:17):

btw, comap is awesome, I'm really glad it's achievable with the current setup, and hopefully the proofs can even be trimmed down further.

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:21):

@Scott Morrison If you have a couple of minutes. Would you mind taking a look at the bottom of the current version of the sheaf file? There is a very ugly mixing of category theory, lattices and topological stuff.

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:21):

Probably I need to layer things better. But I currently don't see exactly how.

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:22):

Especially the case for a basis.

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:22):

That one is pretty important, it is math-trivial, and it is getting very ugly.

view this post on Zulip Johannes Hölzl (Nov 07 2018 at 20:26):

the name of is bot. I guess the concrete structure is something like topological_space.has_bot? But you can just use whenever you need the indiscrete topology

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:26):

Ok, I was just looking for a name to give to site.trivial. But maybe site.trivial is fine as it is...

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:26):

Or is this going to be site.has_bot at some point :lol:?

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:28):

Anyway...

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:28):

I'm feeling like basis.site needs choice somewhere...

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:43):

Aah, progress has been made and pushed. It's not done yet, but I need sleep. And now it looks a lot better.

view this post on Zulip Johan Commelin (Nov 07 2018 at 20:43):

Anyone who wants to step in: please go ahead!

view this post on Zulip Scott Morrison (Nov 07 2018 at 20:44):

okay, I've just been having a look, but it's going to take me a while to get up to speed here. :-(

view this post on Zulip Scott Morrison (Nov 07 2018 at 20:48):

@Johan Commelin, I'm starting to doubt using def over (X : C) := comma (functor.id C) (functor.of_obj X)

view this post on Zulip Scott Morrison (Nov 07 2018 at 20:48):

It means the comma_morphism.w field is a bit unusable, because it has lurking functor.ids in it that we have to dsimp and then rw category.id_comp to get out of the way.

view this post on Zulip Scott Morrison (Nov 07 2018 at 20:49):

At very least we should not use g.w for g a morphisms of overs, but write a cleaner lemma.

view this post on Zulip Scott Morrison (Nov 07 2018 at 21:08):

Okay, I've fixed that issue, and cleaned up proofs a little. I don't yet have any help for your sorries, however .:-)

view this post on Zulip Johan Commelin (Nov 08 2018 at 04:19):

@Scott Morrison Thanks for your help! I didn't think over was creating too many problems yet. And I would hope that they would be fixable by API otherwise...

view this post on Zulip Scott Morrison (Nov 08 2018 at 04:27):

I think I solved the over issue; the simp lemma cone_morphism.over_w is all we needed.

view this post on Zulip Scott Morrison (Nov 08 2018 at 04:46):

Ugh.. I just sat down to clean some things up in the limits branch, and within minutes I was dealing with something that wouldn't be a problem if we didn't use coercions... :pile_of_poo:

view this post on Zulip Johan Commelin (Nov 08 2018 at 05:27):

@Mario Carneiro @Johannes Hölzl :up:

view this post on Zulip Johannes Hölzl (Nov 08 2018 at 08:52):

@Scott Morrison when you cleanup the limits branch, take care that no line is longer than 100 chars, also don't indent like

{ long_field_name := { g := ...,
                         ... } }

but

{ long_field_name :=
  { ...
  } }

view this post on Zulip Scott Morrison (Nov 08 2018 at 08:53):

Yep, I've been doing this. I'm now in cleanup mode, and will check everything before the PR. :-)

view this post on Zulip Scott Morrison (Nov 08 2018 at 09:26):

Oof, I just realised you said 100 characters, I thought I'd got away with 120 before. I'll trim some more. :-)

view this post on Zulip Johannes Hölzl (Nov 08 2018 at 09:30):

I'm personally fine with 120 but most people say they cannot read my laptop screen as my resolution is too high... So I think 100 is the better solution. And I get the feeling Mario would prefer 60 :-)

view this post on Zulip Scott Morrison (Nov 08 2018 at 09:33):

No worries, I'm going for 100 for now. :-)

view this post on Zulip Reid Barton (Nov 13 2018 at 18:54):

@Scott Morrison is it intentional that category_theory.limits.types and category_theory.limits.functor_category aren't imported from category_theory.limits.default?

view this post on Zulip Scott Morrison (Nov 13 2018 at 20:51):

I wasn't sure. My inclination is always to import less by default, but I don't really mind.

view this post on Zulip Johan Commelin (Nov 13 2018 at 21:07):

Would it make sense to add filtered limits to this PR?

view this post on Zulip Reid Barton (Nov 13 2018 at 21:21):

I have a bunch of stuff related to κ\kappa-filtered colimits somewhere

view this post on Zulip Johan Commelin (Nov 14 2018 at 11:27):

The file preserves.lean is not fully dualised. For example, there is no preserved_colimit.

view this post on Zulip Johan Commelin (Nov 14 2018 at 19:15):

Comma categories come with two natural forgetful functors: on this page https://ncatlab.org/nlab/show/comma+category#InComponents they are called HCH_C and HDH_D.
See https://github.com/leanprover-community/mathlib/blob/limits/category_theory/commas.lean for what we have in the current limits PR. What would be good names for these forgetful functors in Lean?

view this post on Zulip Johan Commelin (Nov 14 2018 at 19:15):

This is not just hypothetical, I want to use them in my sheaves project now...

view this post on Zulip Johan Commelin (Nov 14 2018 at 19:16):

forget_left could mean that we forget towards the left... or that we forget the left component, and keep the right...

view this post on Zulip Johan Commelin (Nov 14 2018 at 19:16):

So, should we go with to_left or forget_to_left?

view this post on Zulip Scott Morrison (Nov 14 2018 at 19:18):

How about just fst and snd?

view this post on Zulip Scott Morrison (Nov 14 2018 at 19:19):

These are the usual names for the projections on a pair-like object.

view this post on Zulip Johan Commelin (Nov 14 2018 at 19:19):

Ok, fine with me.

view this post on Zulip Johan Commelin (Nov 14 2018 at 19:24):

namespace comma

variables (L) (R)

def fst : comma L R  A :=
{ obj := λ X, X.left,
  map := λ _ _ f, f.left }

def snd : comma L R  B :=
{ obj := λ X, X.right,
  map := λ _ _ f, f.right }

end comma

view this post on Zulip Johan Commelin (Nov 14 2018 at 19:24):

@Scott Morrison Should I push this to limits?

view this post on Zulip Scott Morrison (Nov 14 2018 at 19:25):

yes, thanks

view this post on Zulip Scott Morrison (Nov 14 2018 at 19:25):

While you're at it, how about we even rename the fields of commas and comma morphisms to fst and snd?

view this post on Zulip Johan Commelin (Nov 14 2018 at 19:28):

Aah, hmm. I pushed already.

view this post on Zulip Johan Commelin (Nov 14 2018 at 19:28):

But yes, that might be a good idea.

view this post on Zulip Johan Commelin (Nov 14 2018 at 19:29):

But doesn't that lead to conflicts?

view this post on Zulip Johan Commelin (Nov 14 2018 at 19:29):

As in, we are defining a structure comma with fields fst and snd, and then in the comma namespace we also want to define fst and snd...

view this post on Zulip Johan Commelin (Nov 14 2018 at 19:32):

@Scott Morrison Is this one of the reasons you sometimes add ' to names?

view this post on Zulip Scott Morrison (Nov 14 2018 at 22:32):

No, that's not why I sometimes add '. That's purely so we can give restated, dsimped (or coercioned, back in the bad old days)) versions of the structure fields.

view this post on Zulip Scott Morrison (Nov 14 2018 at 22:33):

Not sure how to deal with that name conflict....

view this post on Zulip Johan Commelin (Nov 15 2018 at 05:30):

@Mario Carneiro So, what is the common way to resolve naming conflicts like this? The general question is this: what do we do with structures that have a field foo and the projection on foo happens to be a functor... Would this have been easier if functors were a class?

view this post on Zulip Mario Carneiro (Nov 15 2018 at 05:30):

I've been using one letter prefixes in a few places

view this post on Zulip Mario Carneiro (Nov 15 2018 at 05:31):

like linear_map.comp is composition of linear maps, and linear_map.lcomp is a linear composition function

view this post on Zulip Mario Carneiro (Nov 15 2018 at 05:31):

and llcomp is linear in a really high order type

view this post on Zulip Johan Commelin (Nov 15 2018 at 05:32):

So in this case you would propose ffst and fsnd?

view this post on Zulip Mario Carneiro (Nov 15 2018 at 05:33):

yeah... you might also want to ask @Scott Morrison in case he has already found a naming convention for this

view this post on Zulip Johan Commelin (Nov 15 2018 at 05:33):

@Scott Morrison Have you documented somewhere why functors are not a class?

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:33):

You mean a typeclass on the underlying function of objects?

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:34):

It's a good question, which I've been meaning to try to remember the answer to. :-)

view this post on Zulip Johan Commelin (Nov 15 2018 at 05:34):

Because if we could just write instance : functor (fst) then someone could write X.fst and get functorial behaviour out of that...

view this post on Zulip Johan Commelin (Nov 15 2018 at 05:34):

Or am I dreaming?

view this post on Zulip Johan Commelin (Nov 15 2018 at 05:35):

Because now I have a bunch of code containing X.fst which will probably have to be written as the defeq ffst.obj X just to make sure that it plays nice with later constructions.

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:38):

At some point in the past I had a strong opinion about this (against the typeclass version), but it's worth revisiting.

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:38):

My opinion may have been based on trying to refactor everything to this form and it being miserable. :-)

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:39):

ah,

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:39):

So you do quickly want the bundled version as well, to talk about the category of functors and natural transformations

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:40):

But that's not an obstacle in itself.

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:41):

When you want to write yoneda : C \func (C^op \func Type), what would we do? Just write yoneda : C \to (C^op \to Type)

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:41):

and then separate instances functorial (yoneda X), and ...?

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:42):

the problem is you can't write functorial yoneda

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:42):

because we would need a category structure on C^op \to Type

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:42):

and where would that come from?

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:43):

the category structure is only on the bundled functors

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:44):

so.... you define yoneda_2 : C \to (C^op \func Type), and prove that its underlying functions are the same as yoneda, and then construct functorial yoneda_2?

view this post on Zulip Scott Morrison (Nov 15 2018 at 05:44):

Seems a bit gross.

view this post on Zulip Johan Commelin (Nov 15 2018 at 05:57):

I see, those are good points. Thanks for pointing them out! Otoh it might be consistent with what we have been doing so far? (Having both an unbundled and a bundled version.)

view this post on Zulip Johan Commelin (Nov 15 2018 at 05:58):

I hope that with the unbundled version a lot of other code might become cleaner...

view this post on Zulip Johan Commelin (Nov 15 2018 at 05:59):

Another reason against unbundling is if we can cook up a plethora of examples where functors have the same underlying function on objects... But can only cook up pathological examples at the moment.

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:39):

it is worth mentioning that this is basically the opposite direction to the one I took in the module refactor

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:39):

with bundling linear maps

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:40):

I'm not saying it's a bad idea per se, but the reasons that apply to one equally apply to the other

view this post on Zulip Johan Commelin (Nov 15 2018 at 06:40):

I was also very surprised that you did that :grinning:
I remember that about half a year ago you told me that bundling comes with quite some drawbacks, and that a lot of stuff should be dealt with in an unbundled setting first...

view this post on Zulip Johan Commelin (Nov 15 2018 at 06:41):

As a recent example, the bundled version open_set (X : Top) was changed into the unbundled opens (X : Type) [topological_space X]

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:42):

not only there are drawbacks in every direction, some are innate and some are artifacts of lean 3 implementation

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:42):

but I stand by that last one

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:43):

The point is that opens is not a functor, it is a function on a fixed topological space

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:43):

er, actually I think it is a functor from the preorder category, but you get the idea

view this post on Zulip Johan Commelin (Nov 15 2018 at 06:44):

It is a functor from Top to Type

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:44):

it's not, though

view this post on Zulip Johan Commelin (Nov 15 2018 at 06:44):

contravariant

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:44):

like not literally

view this post on Zulip Johan Commelin (Nov 15 2018 at 06:44):

???

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:44):

this is what fopens would be for

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:44):

you take the function and bundle it up into a functor

view this post on Zulip Johan Commelin (Nov 15 2018 at 06:45):

Ok, so I want instance : functorial opens

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:45):

this is also what scott is talking about with yoneda_2

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:45):

that's not going to help if you need a functor though

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:45):

it's still unbundled

view this post on Zulip Johan Commelin (Nov 15 2018 at 06:45):

Or maybe we rename the current functor to Functor, and then have functor for the unbundled version.

view this post on Zulip Mario Carneiro (Nov 15 2018 at 06:46):

like if you need to inhabit a functor category like scott said

view this post on Zulip Johan Commelin (Nov 15 2018 at 06:46):

Anyway, my train is calling me. See you in 45min.

view this post on Zulip Johan Commelin (Nov 15 2018 at 07:34):

Ok, so what is the verdict? Would it make sense to introduce an unbundled version of functor or should I go for the prefix naming scheme? Or is this something that isn't clear, and deserves more experimentation?

view this post on Zulip Johan Commelin (Nov 15 2018 at 07:34):

@Mario Carneiro Also, which parts exactly do you think a br0xen because of Lean 3? And which parts are inherent drawbacks?

view this post on Zulip Mario Carneiro (Nov 15 2018 at 07:37):

the stuff about coercions is broken because of lean 3

view this post on Zulip Mario Carneiro (Nov 15 2018 at 07:39):

some of the stuff about using bundled classes for Group, Top etc could be solved but only with significant changes to how elaboration works (i.e. unification hints)

view this post on Zulip Mario Carneiro (Nov 15 2018 at 07:40):

I think you shouldn't bother making an unbundled version of functor. This already exists, and it's called functor

view this post on Zulip Johan Commelin (Nov 15 2018 at 07:44):

I don't follow

view this post on Zulip Johan Commelin (Nov 15 2018 at 07:45):

If functor is unbundled, what would be a bundled functor?

view this post on Zulip Mario Carneiro (Nov 15 2018 at 08:02):

_root_.functor

view this post on Zulip Johan Commelin (Nov 15 2018 at 08:05):

What? That is not even in the category theory library...

view this post on Zulip Johan Commelin (Nov 15 2018 at 08:05):

Also, it isn't bundling the function on objects. So I would call this an unbundled endofunctor of Type

view this post on Zulip Johan Commelin (Nov 15 2018 at 08:06):

Maybe I'm just very confused about terminology.

view this post on Zulip Johan Commelin (Nov 15 2018 at 08:11):

What we have now is

structure functor (C : Type u₁) [category.{u₁ v₁} C] (D : Type u₂) [category.{u₂ v₂} D] :
  Type (max u₁ v₁ u₂ v₂) :=
(obj       : C  D)
(map       : Π {X Y : C}, (X  Y)  ((obj X)  (obj Y)))
(map_id'   :  (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(map_comp' :  {X Y Z : C} (f : X  Y) (g : Y  Z), map (f  g) = (map f)  (map g) . obviously)

And I'm asking whether it makes sense to also have

structure functor {C : Type u₁} [category.{u₁ v₁} C] {D : Type u₂} [category.{u₂ v₂} D] (obj : C  D) :
  Type (max u₁ v₁ u₂ v₂) :=
(map       : Π {X Y : C}, (X  Y)  ((obj X)  (obj Y)))
(map_id'   :  (X : C), map (𝟙 X) = 𝟙 (obj X) . obviously)
(map_comp' :  {X Y Z : C} (f : X  Y) (g : Y  Z), map (f  g) = (map f)  (map g) . obviously)

view this post on Zulip Mario Carneiro (Nov 15 2018 at 08:22):

possibly... in particular it may work better with notations, just like the <$> notation in _root_.functor

view this post on Zulip Mario Carneiro (Nov 15 2018 at 08:23):

which is not necessarily an endofunctor btw

view this post on Zulip Mario Carneiro (Nov 15 2018 at 08:23):

I was saying that _root_.functor is unbundled

view this post on Zulip Mario Carneiro (Nov 15 2018 at 08:26):

but I think it doesn't work well with identity and composition of functors

view this post on Zulip Mario Carneiro (Nov 15 2018 at 08:26):

I recall Simon had to do some workaround stuff to define the composition of _root_.functors

view this post on Zulip Mario Carneiro (Nov 15 2018 at 08:27):

It is best when all the functors are "atomic", i.e. F A : D if A : C, and F is a variable or constant here

view this post on Zulip Mario Carneiro (Nov 15 2018 at 08:28):

when you have things like (F o G) A = F (G A) it gets hard for lean

view this post on Zulip Johan Commelin (Nov 15 2018 at 08:35):

Ok, I don't understand all the issues, but I'll believe you (-;

view this post on Zulip Johan Commelin (Nov 15 2018 at 08:36):

@Mario Carneiro The f in _root_.functor f goes from Type u to Type v, so up to universes it is an endofunctor, right?

view this post on Zulip Johannes Hölzl (Nov 15 2018 at 09:02):

Yes, _root_.functor is an endofunctor in the Type category (as you said, up to universes)

view this post on Zulip Johannes Hölzl (Nov 15 2018 at 09:02):

I guess you meant also class functor {C : Type u₁} [category.{u₁ v₁} C] {D : Type u₂} [category.{u₂ v₂} D] (obj : C → D) : ... (class instead of structure)?

view this post on Zulip Johan Commelin (Nov 15 2018 at 09:03):

Aah sure, that was an "edito"

view this post on Zulip Johannes Hölzl (Nov 15 2018 at 09:06):

The problem with classes is that the .func_in_namespace syntax doesn't work. So while you can add a specific function (like fst) map needs to be named fmap or we need to introduce a infix operator. Similar with the theorem names.

view this post on Zulip Johan Commelin (Nov 15 2018 at 09:07):

I see, that makes sense.

view this post on Zulip Johannes Hölzl (Nov 15 2018 at 09:10):

This is a hard decision. I think there is no clear answer (at least not in Lean 3)

view this post on Zulip Johan Commelin (Nov 15 2018 at 09:10):

The correct solution in this case is probably that we should define comma as a 2-categorical pullback. That would instantly make fst and snd into functors (à la Scott).

view this post on Zulip Johan Commelin (Nov 15 2018 at 11:08):

Next naming question: given a natural transformation R₁ \nattrans R₂ you get a functor comma L R₁ → comma L R₂. How should we call this gadget? Would this be map_right, and the corresponding thing for L₁ and L₂ would be map_left?

view this post on Zulip Johan Commelin (Nov 15 2018 at 11:24):

@Johannes Hölzl Is it safe to add @[simp] in the following way?

@[simp] def fst : comma L R  A :=
{ obj := λ X, X.left,
  map := λ _ _ f, f.left }

view this post on Zulip Johannes Hölzl (Nov 15 2018 at 11:26):

It is safe, but would be annoying. I think you only want to unfold fst under a projection (i.e. obj (fst _) = _ and map (fst _) = _) or some other operation

view this post on Zulip Johan Commelin (Nov 15 2018 at 11:29):

Ok, so I should write my own explicit simp-lemmas

view this post on Zulip Johan Commelin (Nov 15 2018 at 11:49):

@Scott Morrison I just pushed map_left and map_right to limits. I don't know if you like that, but I think they are pretty useful. Maybe I shouldn't be touching this branch too much. I can keep further stuff in the sheaf branch.

view this post on Zulip Johan Commelin (Nov 15 2018 at 11:50):

Also, I didn't have the -- obviously says comments. Maybe that is bad, because then you won't find this code for future clean-ups??

view this post on Zulip Scott Morrison (Nov 15 2018 at 19:59):

No, it's fine. I think my point that rewrite_search is awesome but for now slow has been made, and we can drop those comments. :-)

view this post on Zulip Johan Commelin (Nov 15 2018 at 20:08):

Well, maybe you put the comments there so that you could easily clean up those blocks once mathlib has a fast rewrite_search...

view this post on Zulip Reid Barton (Nov 16 2018 at 16:47):

@Scott Morrison do you have an opinion about this change?

diff --git a/category_theory/limits/cones.lean b/category_theory/limits/cones.lean
index 6d68844..7fce15c 100644
--- a/category_theory/limits/cones.lean
+++ b/category_theory/limits/cones.lean
@@ -228,16 +228,17 @@ include 𝒟

 @[simp] def functoriality (F : J ⥤ C) (G : C ⥤ D) : (cocone F) ⥤ (cocone (F ⋙ G)) :=
 { obj := λ A,
-  { X  := G.obj A.X,
-    ι  :=  whisker_right A.ι G ⊟ (functor.const_compose _ _ _).inv },
+  { X := G.obj A.X,
+    ι :=
+    { app := λ j, G.map (A.ι.app j), naturality' := by intros; erw ←G.map_comp; tidy } },
   map := λ _ _ f,
   { hom := G.map f.hom,
     w'  :=
     begin
       intros, dsimp,
-      erw [category.comp_id, ←functor.map_comp, cocone_morphism.w, category.comp_id],
+      erw [←functor.map_comp, cocone_morphism.w],
     end } }
 end
 end cocones

 end category_theory.limits
@@ -257,6 +261,6 @@ def map_cocone_morphism (H : C ⥤ D) {c c' : cocone F} (f : cocone_morphism c c
 @[simp] lemma map_cone_π (H : C ⥤ D) (c : cone F) (j : J) :
   (map_cone H c).π.app j = ((functor.const_compose _ _ _).hom ⊟ whisker_right c.π H).app j := rfl
 @[simp] lemma map_cocone_ι (H : C ⥤ D) (c : cocone F) (j : J) :
-  (map_cocone H c).ι.app j = (whisker_right c.ι H ⊟ (functor.const_compose _ _ _).inv).app j := rfl
+  (map_cocone H c).ι.app j = H.map (c.ι.app j) := rfl

 end category_theory.functor

view this post on Zulip Scott Morrison (Nov 16 2018 at 21:45):

Looks fine.

view this post on Zulip Kevin Buzzard (Nov 20 2018 at 17:03):

local attribute [instance, priority 0] classical.prop_decidable
noncomputable instance : has_colimits.{v+1 v} CommRing :=
{ cocone := λ J HJ F, {
    X := by letI := HJ; exact
         let poly_vars := Σ (j : J), F.obj j in
         let R := mv_polynomial poly_vars  in
         by letI : comm_ring R := finsupp.to_comm_ring; exact
         let I : ideal R := ideal.span ( : set R) in
         {α := I.quotient},...

Why do I have to put all these letI's in? Is this expected? I'm trying to construct the colimit of a diagram of commutative rings. The ideal is currently wrong.

Oh -- I also made this change to mathlib:

structure bundled (c : Type u  Type v) :=
(α : Type u)
(str : c α . tactic.interactive.apply_instance)

Is that crazy?

view this post on Zulip Patrick Massot (Nov 20 2018 at 17:04):

A much more trivial remark is that, as far as I understand, nested let can be flattened

view this post on Zulip Kevin Buzzard (Nov 20 2018 at 17:05):

the letI's can't though and they are interspersed with the lets :-/

view this post on Zulip Patrick Massot (Nov 20 2018 at 17:05):

not for poly_vars and R

view this post on Zulip Reid Barton (Nov 20 2018 at 17:32):

The first letI is expected; or you can use by exactI ...

view this post on Zulip Reid Barton (Nov 20 2018 at 17:34):

I don't know why you would need the second one though

view this post on Zulip Kevin Buzzard (Nov 20 2018 at 17:35):

We don't need it! Thanks! We needed it at some point -- maybe I was confused by another error.

view this post on Zulip Reid Barton (Nov 20 2018 at 17:35):

For making objects of bundled, the intent was to use mk_ob in the situation where the instance is one that will be provided by type class inference

view this post on Zulip Reid Barton (Nov 20 2018 at 17:36):

though I'm not sure whether it really works... it worked great in lean-homotopy-theory, where the category Top was fixed, but I'm not sure it works as well with c variable

view this post on Zulip Kevin Buzzard (Nov 20 2018 at 17:36):

local attribute [instance, priority 0] classical.prop_decidable
noncomputable instance : has_colimits.{v+1 v} CommRing :=
{ cocone := λ J HJ F, {
    X := by exactI
         let poly_vars := Σ (j : J), F.obj j,
         R := mv_polynomial poly_vars  in
         let I : ideal R := ideal.span ( : set R) in
         {α := I.quotient, str := by apply_instance},
    ι := { app := λ j, ⟨λ r,begin sorry end, begin sorry end, naturality' := sorry}
    },
  is_colimit := sorry
}

I have a student making colimits -- this is how far we are.

view this post on Zulip Kevin Buzzard (Nov 20 2018 at 17:37):

I see, I didn't know about mk_ob

view this post on Zulip Reid Barton (Nov 20 2018 at 17:37):

however, I also found making the str field into a () field more convenient, for the case where you want to provide it explicitly

view this post on Zulip Reid Barton (Nov 20 2018 at 17:38):

using \<_, _\>

view this post on Zulip Kevin Buzzard (Nov 20 2018 at 17:38):

local attribute [instance, priority 0] classical.prop_decidable
noncomputable instance : has_colimits.{v+1 v} CommRing :=
{ cocone := λ J HJ F, {
    X := by exactI
         let poly_vars := Σ (j : J), F.obj j,
         R := mv_polynomial poly_vars  in
         let I : ideal R := ideal.span ( : set R) in
         category_theory.mk_ob (I.quotient),
    ι := { app := λ j, ⟨λ r,begin sorry end, begin sorry end, naturality' := sorry}
    },
  is_colimit := sorry
}

mk_ob added

view this post on Zulip Reid Barton (Nov 20 2018 at 17:38):

Yes, looks like a good start

view this post on Zulip Kevin Buzzard (Nov 20 2018 at 17:38):

I have never used this library before, I didn't know about mk_ob. Are there any docs or basic worked examples?

view this post on Zulip Kevin Buzzard (Nov 20 2018 at 17:38):

Maybe I'm writing it :-)

view this post on Zulip Reid Barton (Nov 20 2018 at 17:39):

I think possibly nobody has used it before

view this post on Zulip Johan Commelin (Nov 27 2018 at 14:04):

I think something like this might be useful, and I couldn't find it elsewhere:

namespace category_theory.limits
open category_theory

variables {K : Type v} {C : Type u} {J : Type v} [𝒞 : category.{u v} C] [𝒦 : small_category K] [small_category J]
include C 𝒞 K 𝒦

lemma colimit.pre_map
  [has_colimits_of_shape.{u v} J C] [has_colimits_of_shape.{u v} K C]
  {F : J  C} {E₁ E₂ : K  J} (α : E₁  E₂) :
  colimit.pre F E₁ = colim.map (whisker_right α F)  colimit.pre F E₂ :=
begin
  ext1, dsimp,
  conv {to_rhs, rw category.assoc},
  simp,
end

end category_theory.limits

view this post on Zulip Johan Commelin (Nov 29 2018 at 16:00):

I don't have time to finish this atm, but I think we want lemmas like

def colimit.coyoneda {F : J  C} [has_colimit F] : coyoneda.obj (colimit F)  F.cocones :=
{ hom :=
  { app := λ P f, cocones_of_cocone ((colimit.cocone F).extend f),
    naturality' :=
    begin
      tidy {trace_result := tt},
      sorry
    end },
  inv :=
  { app := λ P c, colimit.desc F (cocone_of_cocones c),
    naturality' :=
    begin
      tidy {trace_result := tt},
      sorry
    end } }

view this post on Zulip Johan Commelin (Nov 29 2018 at 16:01):

This generalises

def colimit.hom_equiv {F : J  C} [has_colimit F] (P : C) : (colimit F  P)  (F.cocones.obj P) :=
{ hom := λ f, cocones_of_cocone ((colimit.cocone F).extend f),
  inv := λ c, colimit.desc F (cocone_of_cocones c) }

view this post on Zulip Reid Barton (Nov 29 2018 at 16:13):

Yes, probably. But this one is kind of automatic, I think. You might have an easier time constructing it with nat_iso.of_components.

view this post on Zulip Reid Barton (Nov 29 2018 at 16:14):

The more crucial one is that the isomorphism is also natural in F

view this post on Zulip Reid Barton (Nov 29 2018 at 16:20):

And I guess we should state these simultaneously somehow

view this post on Zulip Johan Commelin (Nov 29 2018 at 17:13):

Yes, I realised that while I was on the train. I'm not general enough...

view this post on Zulip Johan Commelin (Nov 29 2018 at 17:14):

So cocones has to be turned into a functor, and then colim >>> coyoneda should be naturally isomorphic to it, I guess.

view this post on Zulip Johan Commelin (Nov 29 2018 at 17:21):

@Reid Barton Do you think it makes sense to do this before the limits-2 branch is merged?

view this post on Zulip Reid Barton (Nov 29 2018 at 17:23):

No

view this post on Zulip Reid Barton (Nov 29 2018 at 17:23):

No adding things!

view this post on Zulip Johan Commelin (Nov 29 2018 at 17:26):

Sure... I'll create a limits-2.epsilon after this one is merged :wink:

view this post on Zulip Reid Barton (Dec 03 2018 at 04:21):

This business with special shapes of limits is more subtle than I expected

view this post on Zulip Reid Barton (Dec 03 2018 at 04:22):

Nothing is defeq to anything...

view this post on Zulip Reid Barton (Dec 03 2018 at 04:43):

Maybe we should just not do anything here?

view this post on Zulip Johan Commelin (Dec 03 2018 at 05:22):

What does "not do anything" mean?

view this post on Zulip Johan Commelin (Dec 03 2018 at 05:22):

Do you mean to not have these special cases at all? Or do you mean that you don't want to change anything of what Scott did?

view this post on Zulip Reid Barton (Dec 03 2018 at 16:35):

I mean not to have these special cases, or more precisely, still provide the functions for building functors and cones out of discrete categories, for example, but don't use the word "product" anywhere

view this post on Zulip Johan Commelin (Dec 03 2018 at 16:53):

Ok, I would have to see that in action. I guess it would be useful if it increases the defeqness (defeqtitude?) of the library.

view this post on Zulip Johan Commelin (Dec 03 2018 at 18:13):

@Reid Barton Are you currently testing this out? Could you show what it would look like for (binary) products?

view this post on Zulip Reid Barton (Dec 03 2018 at 18:28):

I haven't tried to put this into practice yet (hopefully I will be able to do so over the next few days) but you can approximate it by just ignoring the existence of files like limits/products.lean.

view this post on Zulip Reid Barton (Dec 03 2018 at 18:29):

The definition of pi there for example is essentially just pi f := limit (functor.of_function f)--I'm suggesting you work with the right-hand side directly

view this post on Zulip Johan Commelin (Dec 03 2018 at 18:33):

Hmm, but it is surprising that that would increase defeqness, right?

view this post on Zulip Reid Barton (Dec 03 2018 at 18:33):

I'm "increasing defeqness" by removing all the parts of the library which have defeq issues

view this post on Zulip Reid Barton (Dec 03 2018 at 18:33):

it's a right adjoint

view this post on Zulip Reid Barton (Dec 03 2018 at 18:35):

Here is an example: limit.post : G.obj (limit F) ⟶ limit (F ⋙ G)
The products version should look like pi.post : G.obj (limits.pi f) ⟶ (limits.pi (G.obj ∘ f)) where limits.pi f = limit (functor.of_function f)

view this post on Zulip Reid Barton (Dec 03 2018 at 18:36):

Unfortunately functor.of_function (G.obj ∘ f) is not definitionally equal to functor.of_function f ⋙ G

view this post on Zulip Reid Barton (Dec 03 2018 at 18:36):

so pi.post is not a special case of limit.post

view this post on Zulip Reid Barton (Dec 03 2018 at 18:37):

So. my current feeling is that I have no idea how to solve this kind of issue clearly in the library, and so I would rather not even try, and let the user deal with it instead.

view this post on Zulip Johan Commelin (Dec 03 2018 at 18:38):

Hmm... I see. So what kind of functions would you still provide?

view this post on Zulip Reid Barton (Dec 03 2018 at 18:38):

functor.of_function and similar things

view this post on Zulip Reid Barton (Dec 03 2018 at 18:41):

Anything which lets you build a functor, natural transformation, cone, etc. out of one of these special indexing categories from simpler data. That amount clearly seems to be required, since building those manually is a big pain.

view this post on Zulip Reid Barton (Dec 03 2018 at 18:42):

I want to make the overall API of size O(N+M) where N is the number of facts I know about limits and M is the number of special cases of limits I care about, not O(N*M)

view this post on Zulip Johan Commelin (Dec 03 2018 at 18:58):

I wouldn't mind having nice binder notation for limit (functor.of_function f), but I guess we need to use a weird \Pi, because the other one is stolen...

view this post on Zulip Johan Commelin (Dec 03 2018 at 18:59):

And writing limit (functor.of_pair X Y) seems pretty verbose. But we'll see. For now I think it is a good idea to at least make a PR with all the special shapes.

view this post on Zulip Scott Morrison (Dec 04 2018 at 07:27):

limit (functor.of_pair X Y) feels pretty lame to me. I agree the interface size is an issue, but we should set aside the pain of producing it, and decide whether the N+M or N*M interface is actually more usable.

view this post on Zulip Scott Morrison (Dec 04 2018 at 07:28):

I worry that all the things you're proposing to leave out because they suffer from defeq issues are exactly putting the pain of dealing with those defeq issues on the user of the library.

view this post on Zulip Scott Morrison (Dec 04 2018 at 07:29):

I mean, this is why I wrote everything out again in each special shape --- precisely because you can't just use the general one (or rather, if you do, you get a clumsier statement).

view this post on Zulip Scott Morrison (Dec 04 2018 at 07:31):

That said, I absolutely appreciate the horror of an N*M size library.

view this post on Zulip Johan Commelin (Dec 04 2018 at 07:39):

I would really have to see how this works out in practice.

view this post on Zulip Reid Barton (Dec 04 2018 at 14:01):

I worry that all the things you're proposing to leave out because they suffer from defeq issues are exactly putting the pain of dealing with those defeq issues on the user of the library.

Yes, this is exactly the plan.

view this post on Zulip Reid Barton (Dec 04 2018 at 14:10):

Note that the example pi.post where things start to go wrong is again a definition. That means it will appear in the statement of theorems about limits. It will not be possible to specialize these theorems to facts about pi.post if the latter is defined in a way unrelated to limit.post.

view this post on Zulip Reid Barton (Dec 04 2018 at 14:20):

Basically my claim is that we don't actually how to address these issues (yet?) and I would rather not make O(N*M) guesses about the best way to proceed.

view this post on Zulip Reid Barton (Dec 04 2018 at 14:20):

In my mind M and especially N are not fixed, but variable. So it's not just a matter of "write out all the N*M things, and then you're done"

view this post on Zulip Johan Commelin (Dec 04 2018 at 14:22):

I think I agree with both of you.

view this post on Zulip Johan Commelin (Dec 04 2018 at 14:22):

For the short-term future, I would follow Reid, but in the long-term I wouldn't mind having a really slick and polished library the way that Scott envisions it.

view this post on Zulip Reid Barton (Dec 04 2018 at 14:23):

I do think we could define product X Y := limit (functor.of_pair X Y) and maybe 2-3 minor conveniences per limit type.

view this post on Zulip Johan Commelin (Dec 04 2018 at 14:23):

Anyway, we've had an O(N) chunk merged. Next up seems to be an O(M) chunk. (-;

view this post on Zulip Johan Commelin (Dec 04 2018 at 16:25):

So, how about the classes has_products, has_pullbacks, has_equalizers, etc... will they remain? Or do we just write has_limits_of_shape walking_pair?

view this post on Zulip Reid Barton (Dec 04 2018 at 17:32):

I was planning on getting rid of those as well, though for a different reason, namely that the class system doesn't seem to deal with them well

view this post on Zulip Scott Morrison (Dec 04 2018 at 19:09):

I'm really pretty dubious. We know that in many categories, there should be separate implementations of, say, binary_products and general limits. How will this be achieved in the minimal API?

view this post on Zulip Reid Barton (Dec 04 2018 at 19:12):

No, don't do that

view this post on Zulip Reid Barton (Dec 04 2018 at 19:13):

Better: provide specialized ways to construct is_limit cones

view this post on Zulip Scott Morrison (Dec 04 2018 at 19:14):

I'm confused. What will it look like when someone needs to compare the carrier type of limit (functor.of_pair X Y) with the Lean built-in product of the carrier types of X and Y?

view this post on Zulip Scott Morrison (Dec 04 2018 at 19:15):

(supposing we're in an algebraic category)

view this post on Zulip Reid Barton (Dec 04 2018 at 19:15):

I think you should not do that either, if by "compare" you mean expect them to be defeq

view this post on Zulip Reid Barton (Dec 04 2018 at 19:17):

But you can use the is_limit for the cone for the product type to get an isomorphism to the limit

view this post on Zulip Scott Morrison (Dec 04 2018 at 19:17):

So, will we provide the natural isomorphism between the two functors C x C -> Type at some point?

view this post on Zulip Reid Barton (Dec 04 2018 at 19:18):

Or if you're feeling lucky, you can locally set the product type one as an instance

view this post on Zulip Reid Barton (Dec 04 2018 at 19:18):

What two functors?

view this post on Zulip Reid Barton (Dec 04 2018 at 19:20):

Do you mean Type x Type -> Type?

view this post on Zulip Reid Barton (Dec 04 2018 at 19:24):

There's going to be a difference between the underlying type of a limit over a discrete diagram that comes from limit and the Pi type in any case.

view this post on Zulip Reid Barton (Dec 04 2018 at 19:25):

I'd rather have this difference out in the open where I can deal with it explicitly, than buried inside some implicit parameter to a class instance

view this post on Zulip Johan Commelin (Dec 04 2018 at 19:30):

I'm afraid I'm too much of an ITP-newbie to contribute meaningfully to this discussion. But for what it's worth, I'dd love to use sheaves as a testing ground of what @Reid Barton is suggesting.

view this post on Zulip Reid Barton (Dec 04 2018 at 19:31):

Recall Johan's issue https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/sheaves.20and.20sites/near/148024839. It took me a long time to even understand how the two sides could be different

view this post on Zulip Scott Morrison (Dec 04 2018 at 20:54):

Okay, I'm definitely happy with the plan to just provide the bare minimum (e.g. functor.of_function and its friends), and then see if we can rebase the sheaf branch onto that.

view this post on Zulip Scott Morrison (Dec 04 2018 at 20:54):

And learn what we need from that development.

view this post on Zulip Scott Morrison (Dec 04 2018 at 20:54):

I agree it's hard to know how bad leaving things out is going to be, in the abstract.

view this post on Zulip Scott Morrison (Dec 05 2018 at 05:46):

As mentioned elsewhere, I've rebased what remains of my limits PR into two pieces: some assorted stuff that can be merged, and the remaining remaining stuff, about special shapes, that shouldn't (yet) be.

view this post on Zulip Scott Morrison (Dec 05 2018 at 05:47):

I did, in the special shapes part, remove a few very naughty [instance] attributes that really shouldn't have been there. I will, sometime, investigate whether their removal has helped.

view this post on Zulip Johan Commelin (Dec 09 2018 at 17:47):

@Reid Barton Any news about the next stage? Can you use any help?

view this post on Zulip Reid Barton (Dec 09 2018 at 20:36):

I've been focusing on other Lean projects recently but actually the next thing I was going to do was PR a version of discrete categories, which Scott has already done in the meantime.

view this post on Zulip Reid Barton (Dec 09 2018 at 20:39):

I'm going to be needing some of the other shapes before too long as well

view this post on Zulip Reid Barton (Dec 12 2018 at 21:51):

I need to prove that cocone.whiskering with an equivalence preserves is_colimit. @Scott Morrison @Johan Commelin I don't suppose either of you has already done this?

view this post on Zulip Kevin Buzzard (Dec 12 2018 at 22:05):

What does whisker mean?

view this post on Zulip Kevin Buzzard (Dec 12 2018 at 22:05):

I know what a cocone is.

view this post on Zulip Scott Morrison (Dec 12 2018 at 22:09):

No, sorry, haven't done this.

view this post on Zulip Scott Morrison (Dec 12 2018 at 22:14):

A cocone on F is a natural transformation from F : J \func C to a constant functor X. Whiskering means whiskering this natural transformation by a functor (i.e. horizontal composition with the identity natural transformation on a functor) (but we still need to work out if we mean by a functor J' \func J or by a functor C \func C'). Looking up category_theory/limits/cones.lean, it seems we have def whisker {K : Type v} [small_category K] (E : K ⥤ J) (c : cocone F) : cocone (E ⋙ F), so it's whiskering on the left.

view this post on Zulip Reid Barton (Dec 12 2018 at 22:17):

I kind of want to rename whisker to whisker_left and make it a functor and rename functoriality to whisker_right

view this post on Zulip Reid Barton (Dec 12 2018 at 22:18):

I think the definition you originally wrote made the relationship to whisker_right more obvious

view this post on Zulip Scott Morrison (Dec 12 2018 at 22:31):

I agree, these would be good changes.

view this post on Zulip Johan Commelin (Dec 13 2018 at 05:52):

Only seeing this now, but sounds good to me.

view this post on Zulip Johan Commelin (Dec 15 2018 at 10:21):

I would like to get more access to specialised shapes. But I don't have a good feeling which for which direction we want to go now. If we can get one example into a PR-ready form, then I could work on the others myself. @Reid Barton @Scott Morrison Do you think you have time to work on (say) products, this week?

view this post on Zulip Johan Commelin (Dec 15 2018 at 10:21):

For example, I want to connect binary (co)products to sup and inf for lattices.

view this post on Zulip Reid Barton (Dec 15 2018 at 16:12):

I'm going to take a look at special shapes again today. However, I'm not entirely sure how to proceed, both in terms of what we want the API to look like, and also in view of the fact that there is already an outstanding PR which adds discrete categories.

view this post on Zulip Johan Commelin (Dec 15 2018 at 17:07):

Ok, cool. @Mario Carneiro Would you have some time to take care of the outstanding PR's? Then we could start moving forward again. It seems to be blocking some work... (But I understand completely if you have other deadlines that are more important.)

view this post on Zulip Mario Carneiro (Dec 15 2018 at 17:08):

Any advice on where to focus?

view this post on Zulip Johan Commelin (Dec 15 2018 at 17:16):

(eg #503, #505)

view this post on Zulip Reid Barton (Dec 15 2018 at 17:18):

#512 has discrete categories which I think are the least problematic of the "special shapes"

view this post on Zulip Mario Carneiro (Dec 15 2018 at 17:26):

I commented on that PR, but it looks like there are still some outstanding comments of yours as well

view this post on Zulip Reid Barton (Dec 15 2018 at 17:27):

Indeed

view this post on Zulip Johan Commelin (Dec 15 2018 at 17:30):

@Mario Carneiro While you are at it, would you mind taking a look at my other PR's? I think they are all pretty straight-forward. Just adding little tidbits to the category lib

view this post on Zulip Mario Carneiro (Dec 15 2018 at 17:34):

I'm not sure about the op thing though

view this post on Zulip Mario Carneiro (Dec 15 2018 at 17:35):

I thought there was a reason it was a type synonym rather than a wrapper

view this post on Zulip Mario Carneiro (Dec 15 2018 at 17:35):

I agree that if it is irreducible it may as well just be a separate inductive type

view this post on Zulip Mario Carneiro (Dec 15 2018 at 17:36):

although with up and down functions you won't get up (down x) = x and down (up x) = x both being rfl

view this post on Zulip Mario Carneiro (Dec 15 2018 at 17:37):

maybe this doesn't matter because these are object equalities...?

view this post on Zulip Reid Barton (Dec 15 2018 at 17:37):

Oh yeah, that could be annoying...

view this post on Zulip Mario Carneiro (Dec 15 2018 at 17:38):

with irreducible you will get strange things not being refl, like with real

view this post on Zulip Mario Carneiro (Dec 15 2018 at 17:38):

I tend to shy away from it for that reason

view this post on Zulip Reid Barton (Dec 15 2018 at 17:40):

I notice that PR doesn't build currently anyways

view this post on Zulip Reid Barton (Dec 15 2018 at 17:49):

With the irreducible definition, would the elaborator treat both unop (op x) = x and op (unop x) = x as definitional equalities?

view this post on Zulip Johan Commelin (Dec 15 2018 at 17:49):

@Mario Carneiro Thanks for the merges!

view this post on Zulip Reid Barton (Dec 15 2018 at 17:50):

I guess I should just experiment... but this particular PR hasn't been a high priority for me

view this post on Zulip Reid Barton (Dec 15 2018 at 18:08):

I think these being questions about equalities between objects makes it more important whether the equalities are definitional, not less

view this post on Zulip Mario Carneiro (Dec 15 2018 at 18:28):

with the irreducible definition I think they would both not be defeq

view this post on Zulip Mario Carneiro (Dec 15 2018 at 18:31):

I stand corrected:

@[irreducible] def A := nat

def to_nat : A  nat := by delta A; exact id
def of_nat : nat  A := by delta A; exact id

theorem to_of (x) : to_nat (of_nat x) = x := rfl --ok
theorem of_to (x) : of_nat (to_nat x) = x := rfl --ok

view this post on Zulip Johan Commelin (Dec 15 2018 at 18:37):

What the heck is delta? I've never seen it before...

view this post on Zulip Patrick Massot (Dec 15 2018 at 18:38):

it's a variation on dunfold

view this post on Zulip Patrick Massot (Dec 15 2018 at 18:40):

I've never used it

view this post on Zulip Mario Carneiro (Dec 15 2018 at 18:56):

it's a very low level definition unfolding tactic

view this post on Zulip Mario Carneiro (Dec 15 2018 at 18:57):

it's good for cases when the elaborator doesn't want it to unfold

view this post on Zulip Mario Carneiro (Dec 15 2018 at 18:57):

although I guess in this case dunfold suffices

view this post on Zulip Mario Carneiro (Dec 15 2018 at 19:00):

I used delta also in the hidden thread, to unfold nat.add into its underlying recursor

view this post on Zulip Mario Carneiro (Dec 15 2018 at 19:00):

dunfold and its friends refuse to use the definition, they only use equation lemmas

view this post on Zulip Patrick Massot (Dec 15 2018 at 19:01):

I knew I saw it not a long time ago!

view this post on Zulip Kevin Buzzard (Dec 15 2018 at 19:18):

It was when I was writing a blog post about equality (a post which is still in the queue of jobs).

view this post on Zulip Scott Morrison (Dec 20 2018 at 12:30):

Hi @Reid Barton, @Johan Commelin, I just separated out what remains of my limits PR into two branches. limits-shapes just provides convenience methods for dealing with cones of special shapes, but doesn't attempt to introduce has_products or any similar gadgets.

view this post on Zulip Scott Morrison (Dec 20 2018 at 12:30):

There's also limits-other which still has everything (the O(M*N) approach...) rebased onto this.

view this post on Zulip Johan Commelin (Dec 21 2018 at 03:02):

@Scott Morrison Does this also mean that you are planning to split #512 into two pieces?

view this post on Zulip Scott Morrison (Dec 21 2018 at 03:22):

I guess I was hoping to just get #512 merged.

view this post on Zulip Scott Morrison (Dec 21 2018 at 03:23):

It's such a grab bag it's not obvious to me where a split would go.

view this post on Zulip Johan Commelin (Dec 21 2018 at 08:17):

@Scott Morrison @Mario Carneiro The merge of #512 introduced some regressions.

view this post on Zulip Mario Carneiro (Dec 21 2018 at 08:18):

okay, then progress it

view this post on Zulip Johan Commelin (Dec 21 2018 at 08:18):

At least https://github.com/leanprover/mathlib/pull/512/files#diff-c997371393c06bacaf4074ef43915f3e

view this post on Zulip Johan Commelin (Dec 21 2018 at 08:18):

I think the rest is fine.

view this post on Zulip Mario Carneiro (Dec 21 2018 at 08:18):

I will leave it to you and scott to figure out what needs fixing

view this post on Zulip Johan Commelin (Dec 21 2018 at 09:04):

Done (finally): #550

view this post on Zulip Scott Morrison (Dec 21 2018 at 10:15):

Thanks @Johan Commelin.


Last updated: May 06 2021 at 18:20 UTC