limits 2.0

Stream: maths

[Reid Barton]

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

[Scott Morrison]

Yes, I think it's pretty close now.

[Scott Morrison]

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.

[Scott Morrison]

It turned out to be really gross to formalise.

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Reid Barton]

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.

[Reid Barton]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

No wonder Scott went on that rant recently :)

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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 }

[Scott Morrison]

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 }

[Scott Morrison]

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.

[Scott Morrison]

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

[Reid Barton]

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

[Scott Morrison]

Awesome!

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

Ah, thanks!

[Reid Barton]

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

[Scott Morrison]

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

[Scott Morrison]

I wonder if we should unify them.

[Reid Barton]

Oh yeah. Isn't it the same thing?

[Reid Barton]

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

[Reid Barton]

and then provide a wrapper for limit if that seems useful

[Reid Barton]

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)

[Reid Barton]

I also did this for is_equalizer.mono

[Scott Morrison]

Hmm, I'm on the fence here.

[Scott Morrison]

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.

[Reid Barton]

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.

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

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?

[Reid Barton]

Well, I suggest 3, with 2 as needed

[Reid Barton]

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

[Reid Barton]

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.

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

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

[Reid Barton]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

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

[Scott Morrison]

yuck! :-)

[Reid Barton]

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

[Scott Morrison]

okay, great :-)

[Reid Barton]

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

[Reid Barton]

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.

[Scott Morrison]

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

[Johan Commelin]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

Which bits of coblah have you been needing?

[Scott Morrison]

(Are you guys all at Freiburg?)

[Johan Commelin]

Mostly coequalizers

[Johan Commelin]

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

[Scott Morrison]

Did you do it yet?

[Scott Morrison]

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

[Johan Commelin]

No, I got stuck somewhere.

[Scott Morrison]

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

[Scott Morrison]

Is it okay if I do that now?

[Johan Commelin]

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

[Scott Morrison]

ok, done!

[Scott Morrison]

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

[Kenny Lau]

@Scott Morrison do you want to skype with us?

[Johan Commelin]

@Scott Morrison Thanks for adding coequalizers!

[Johan Commelin]

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

[Scott Morrison]

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

[Reid Barton]

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

I fixed it.

[Reid Barton]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

I think we should only squash when merging into mathlib.

[Johan Commelin]

Not when multiple people are working on it.

[Scott Morrison]

@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. :-)

[Johan Commelin]

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!

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

Of course, it's still conspicuously missing examples!

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

Yeah, okay, I've done that too.

[Johan Commelin]

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.

[Johan Commelin]

Does it make sense what I'm saying?

[Johan Commelin]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Johan Commelin]

Yes, look at the sheaf branch on community mathlib.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

Look at the sheaf branch on community-mathlib.

[Johan Commelin]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

Oh I see, sorry, I missed the first message

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Reid Barton]

I think the problem is actually that you have 0 instances

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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?

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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

[Johan Commelin]

@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

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

oh, I didn't notice the angle brackets!

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

For has_pullbacks? Deleting _ worked for me

[Reid Barton]

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

[Johan Commelin]

Yes, maybe I should do that...

[Johan Commelin]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

it will lead to tears.

[Scott Morrison]

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

[Scott Morrison]

(and the == with an appropriate composition)

[Scott Morrison]

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

[Scott Morrison]

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

[Johannes Hölzl]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

@Scott Morrison Thanks a lot!

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johannes Hölzl]

⊥

[Johannes Hölzl]

this is the indiscrete topology

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Especially the case for a basis.

[Johan Commelin]

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

[Johannes Hölzl]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Anyway...

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Anyone who wants to step in: please go ahead!

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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:

[Johan Commelin]

@Mario Carneiro @Johannes Hölzl :up:

[Johannes Hölzl]

@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 :=
  { ...
  } }

[Scott Morrison]

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

[Scott Morrison]

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

[Johannes Hölzl]

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

[Scott Morrison]

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

[Reid Barton]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Reid Barton]

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

[Johan Commelin]

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

[Johan Commelin]

Comma categories come with two natural forgetful functors: on this page https://ncatlab.org/nlab/show/comma+category#InComponents they are called $H_C$ and $H_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?

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

So, should we go with to_left or forget_to_left?

[Scott Morrison]

How about just fst and snd?

[Scott Morrison]

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

[Johan Commelin]

Ok, fine with me.

[Johan Commelin]

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

[Johan Commelin]

@Scott Morrison Should I push this to limits?

[Scott Morrison]

yes, thanks

[Scott Morrison]

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

[Johan Commelin]

Aah, hmm. I pushed already.

[Johan Commelin]

But yes, that might be a good idea.

[Johan Commelin]

But doesn't that lead to conflicts?

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

and llcomp is linear in a really high order type

[Johan Commelin]

So in this case you would propose ffst and fsnd?

[Mario Carneiro]

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

[Johan Commelin]

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

[Scott Morrison]

You mean a typeclass on the underlying function of objects?

[Scott Morrison]

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

[Johan Commelin]

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

[Johan Commelin]

Or am I dreaming?

[Johan Commelin]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

ah,

[Scott Morrison]

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

[Scott Morrison]

But that's not an obstacle in itself.

[Scott Morrison]

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)

[Scott Morrison]

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

[Scott Morrison]

the problem is you can't write functorial yoneda

[Scott Morrison]

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

[Scott Morrison]

and where would that come from?

[Scott Morrison]

the category structure is only on the bundled functors

[Scott Morrison]

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?

[Scott Morrison]

Seems a bit gross.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Mario Carneiro]

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

[Mario Carneiro]

with bundling linear maps

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

but I stand by that last one

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

It is a functor from Top to Type

[Mario Carneiro]

it's not, though

[Johan Commelin]

contravariant

[Mario Carneiro]

like not literally

[Johan Commelin]

???

[Mario Carneiro]

this is what fopens would be for

[Mario Carneiro]

you take the function and bundle it up into a functor

[Johan Commelin]

Ok, so I want instance : functorial opens

[Mario Carneiro]

this is also what scott is talking about with yoneda_2

[Mario Carneiro]

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

[Mario Carneiro]

it's still unbundled

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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?

[Johan Commelin]

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

[Mario Carneiro]

the stuff about coercions is broken because of lean 3

[Mario Carneiro]

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)

[Mario Carneiro]

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

[Johan Commelin]

I don't follow

[Johan Commelin]

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

[Mario Carneiro]

_root_.functor

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Maybe I'm just very confused about terminology.

[Johan Commelin]

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)

[Mario Carneiro]

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

[Mario Carneiro]

which is not necessarily an endofunctor btw

[Mario Carneiro]

I was saying that _root_.functor is unbundled

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johannes Hölzl]

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

[Johannes Hölzl]

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

[Johan Commelin]

Aah sure, that was an "edito"

[Johannes Hölzl]

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.

[Johan Commelin]

I see, that makes sense.

[Johannes Hölzl]

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

[Johan Commelin]

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

[Johan Commelin]

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?

[Johan Commelin]

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

[Johannes Hölzl]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Reid Barton]

@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

[Scott Morrison]

Looks fine.

[Kevin Buzzard]

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?

[Patrick Massot]

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

[Kevin Buzzard]

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

[Patrick Massot]

not for poly_vars and R

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

I see, I didn't know about mk_ob

[Reid Barton]

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

[Reid Barton]

using \<_, _\>

[Kevin Buzzard]

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

[Reid Barton]

Yes, looks like a good start

[Kevin Buzzard]

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

[Kevin Buzzard]

Maybe I'm writing it :-)

[Reid Barton]

I think possibly nobody has used it before

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

And I guess we should state these simultaneously somehow

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

No

[Reid Barton]

No adding things!

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

Nothing is defeq to anything...

[Reid Barton]

Maybe we should just not do anything here?

[Johan Commelin]

What does "not do anything" mean?

[Johan Commelin]

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?

[Reid Barton]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Reid Barton]

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.

[Reid Barton]

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

[Johan Commelin]

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

[Reid Barton]

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

[Reid Barton]

it's a right adjoint

[Reid Barton]

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)

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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.

[Johan Commelin]

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

[Reid Barton]

functor.of_function and similar things

[Reid Barton]

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.

[Reid Barton]

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)

[Johan Commelin]

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

[Johan Commelin]

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.

[Scott Morrison]

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.

[Scott Morrison]

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.

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Reid Barton]

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.

[Reid Barton]

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.

[Reid Barton]

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.

[Reid Barton]

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"

[Johan Commelin]

I think I agree with both of you.

[Johan Commelin]

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.

[Reid Barton]

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

[Johan Commelin]

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

[Johan Commelin]

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?

[Reid Barton]

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

[Scott Morrison]

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?

[Reid Barton]

No, don't do that

[Reid Barton]

Better: provide specialized ways to construct is_limit cones

[Scott Morrison]

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?

[Scott Morrison]

(supposing we're in an algebraic category)

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

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

[Reid Barton]

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

[Reid Barton]

What two functors?

[Reid Barton]

Do you mean Type x Type -> Type?

[Reid Barton]

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.

[Reid Barton]

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

[Johan Commelin]

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.

[Reid Barton]

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

[Scott Morrison]

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.

[Scott Morrison]

And learn what we need from that development.

[Scott Morrison]

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

[Scott Morrison]

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.

[Scott Morrison]

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.

[Johan Commelin]

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

[Reid Barton]

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.

[Reid Barton]

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

[Reid Barton]

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?

[Kevin Buzzard]

What does whisker mean?

[Kevin Buzzard]

I know what a cocone is.

[Scott Morrison]

No, sorry, haven't done this.

[Scott Morrison]

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.

[Reid Barton]

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

[Reid Barton]

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

[Scott Morrison]

I agree, these would be good changes.

[Johan Commelin]

Only seeing this now, but sounds good to me.

[Johan Commelin]

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?

[Johan Commelin]

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

[Reid Barton]

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.

[Johan Commelin]

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

[Mario Carneiro]

Any advice on where to focus?

[Johan Commelin]

(eg #503, #505)

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

Indeed

[Johan Commelin]

@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

[Mario Carneiro]

I'm not sure about the op thing though

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Reid Barton]

Oh yeah, that could be annoying...

[Mario Carneiro]

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

[Mario Carneiro]

I tend to shy away from it for that reason

[Reid Barton]

I notice that PR doesn't build currently anyways

[Reid Barton]

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

[Johan Commelin]

@Mario Carneiro Thanks for the merges!

[Reid Barton]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Patrick Massot]

it's a variation on dunfold

[Patrick Massot]

I've never used it

[Mario Carneiro]

it's a very low level definition unfolding tactic

[Mario Carneiro]

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

[Mario Carneiro]

although I guess in this case dunfold suffices

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

I knew I saw it not a long time ago!

[Kevin Buzzard]

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

[Scott Morrison]

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.

[Scott Morrison]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Mario Carneiro]

okay, then progress it

[Johan Commelin]

At least https://github.com/leanprover/mathlib/pull/512/files#diff-c997371393c06bacaf4074ef43915f3e

[Johan Commelin]

I think the rest is fine.

[Mario Carneiro]

I will leave it to you and scott to figure out what needs fixing

[Johan Commelin]

Done (finally): #550

[Scott Morrison]

Thanks @Johan Commelin.