## Stream: maths

### Topic: limits 2.0

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

#### Scott Morrison (Nov 02 2018 at 22:27):

Yes, I think it's pretty close now.

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

#### Scott Morrison (Nov 02 2018 at 22:28):

It turned out to be really gross to formalise.

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

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

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

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

#### Scott Morrison (Nov 02 2018 at 22:34):

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

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

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

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

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

#### Johan Commelin (Nov 03 2018 at 10:09):

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

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

#### Reid Barton (Nov 03 2018 at 15:18):

No wonder Scott went on that rant recently :)

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

#### Scott Morrison (Nov 03 2018 at 22:36):

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

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

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


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


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

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

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

Awesome!

#### Scott Morrison (Nov 04 2018 at 23:42):

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

#### Scott Morrison (Nov 04 2018 at 23:42):

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

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

#### Reid Barton (Nov 04 2018 at 23:45):

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

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

Ah, thanks!

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

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


#### Scott Morrison (Nov 04 2018 at 23:50):

I wonder if we should unify them.

#### Reid Barton (Nov 04 2018 at 23:51):

Oh yeah. Isn't it the same thing?

#### Reid Barton (Nov 04 2018 at 23:51):

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

#### Reid Barton (Nov 04 2018 at 23:51):

and then provide a wrapper for limit if that seems useful

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

#### Reid Barton (Nov 04 2018 at 23:53):

I also did this for is_equalizer.mono

#### Scott Morrison (Nov 04 2018 at 23:54):

Hmm, I'm on the fence here.

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

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

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

#### Reid Barton (Nov 04 2018 at 23:58):

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

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

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

#### Reid Barton (Nov 05 2018 at 00:04):

Well, I suggest 3, with 2 as needed

#### Reid Barton (Nov 05 2018 at 00:05):

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

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

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

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

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

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

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

#### Scott Morrison (Nov 05 2018 at 00:17):

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

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

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

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

#### Reid Barton (Nov 05 2018 at 00:21):

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

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

yuck! :-)

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

okay, great :-)

#### Reid Barton (Nov 05 2018 at 00:29):

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

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

#### Scott Morrison (Nov 05 2018 at 02:00):

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

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

#### Scott Morrison (Nov 05 2018 at 09:50):

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

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

#### Scott Morrison (Nov 05 2018 at 09:52):

Which bits of coblah have you been needing?

#### Scott Morrison (Nov 05 2018 at 09:52):

(Are you guys all at Freiburg?)

#### Johan Commelin (Nov 05 2018 at 09:52):

Mostly coequalizers

#### Johan Commelin (Nov 05 2018 at 09:53):

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

#### Scott Morrison (Nov 05 2018 at 09:54):

Did you do it yet?

#### Scott Morrison (Nov 05 2018 at 09:54):

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

#### Johan Commelin (Nov 05 2018 at 09:54):

No, I got stuck somewhere.

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

#### Scott Morrison (Nov 05 2018 at 09:55):

Is it okay if I do that now?

#### Johan Commelin (Nov 05 2018 at 09:55):

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

ok, done!

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

#### Kenny Lau (Nov 05 2018 at 10:15):

@Scott Morrison do you want to skype with us?

#### Johan Commelin (Nov 05 2018 at 10:29):

@Scott Morrison Thanks for adding coequalizers!

#### Johan Commelin (Nov 05 2018 at 10:32):

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

#### Scott Morrison (Nov 05 2018 at 10:38):

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

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

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

#### Scott Morrison (Nov 05 2018 at 18:48):

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

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

#### Johan Commelin (Nov 05 2018 at 18:51):

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

#### Johan Commelin (Nov 05 2018 at 18:52):

I think we should only squash when merging into mathlib.

#### Johan Commelin (Nov 05 2018 at 18:52):

Not when multiple people are working on it.

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

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

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

#### Scott Morrison (Nov 06 2018 at 10:09):

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

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

#### Scott Morrison (Nov 06 2018 at 10:11):

Of course, it's still conspicuously missing examples!

#### Scott Morrison (Nov 06 2018 at 10:11):

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

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

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

#### Scott Morrison (Nov 06 2018 at 10:27):

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

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

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

#### Scott Morrison (Nov 06 2018 at 10:28):

Yeah, okay, I've done that too.

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

#### Johan Commelin (Nov 06 2018 at 10:29):

Does it make sense what I'm saying?

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

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

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

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

#### Johan Commelin (Nov 06 2018 at 16:12):

Yes, look at the sheaf branch on community mathlib.

#### Johan Commelin (Nov 06 2018 at 16:12):

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

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

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

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

#### Johan Commelin (Nov 06 2018 at 16:36):

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

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

#### Johan Commelin (Nov 06 2018 at 16:37):

Look at the sheaf branch on community-mathlib.

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

#### Kevin Buzzard (Nov 06 2018 at 16:38):

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

#### Kevin Buzzard (Nov 06 2018 at 16:38):

Oh I see, sorry, I missed the first message

#### Johan Commelin (Nov 06 2018 at 16:39):

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

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

#### Kevin Buzzard (Nov 06 2018 at 16:40):

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

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


#### Reid Barton (Nov 06 2018 at 19:00):

I think the problem is actually that you have 0 instances

#### Reid Barton (Nov 06 2018 at 19:01):

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

#### Reid Barton (Nov 06 2018 at 19:01):

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

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

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

#### Johan Commelin (Nov 06 2018 at 19:09):

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

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

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

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


#### Johan Commelin (Nov 06 2018 at 19:37):

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

#### Reid Barton (Nov 06 2018 at 19:39):

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

#### Reid Barton (Nov 06 2018 at 19:39):

oh, I didn't notice the angle brackets!

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

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

#### Reid Barton (Nov 06 2018 at 19:41):

For has_pullbacks? Deleting _ worked for me

#### Reid Barton (Nov 06 2018 at 19:42):

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

#### Johan Commelin (Nov 06 2018 at 19:43):

Yes, maybe I should do that...

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


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

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


#### Scott Morrison (Nov 07 2018 at 11:29):

it will lead to tears.

#### Scott Morrison (Nov 07 2018 at 11:29):

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

#### Scott Morrison (Nov 07 2018 at 11:30):

(and the == with an appropriate composition)

#### Scott Morrison (Nov 07 2018 at 11:32):

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

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

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

#### Scott Morrison (Nov 07 2018 at 12:37):

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

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

#### Johan Commelin (Nov 07 2018 at 12:56):

@Scott Morrison Thanks a lot!

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

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

#### Johan Commelin (Nov 07 2018 at 19:54):

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

#### Johan Commelin (Nov 07 2018 at 19:55):

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

#### Johannes Hölzl (Nov 07 2018 at 20:01):

⊥

#### Johannes Hölzl (Nov 07 2018 at 20:02):

this is the indiscrete topology

#### Johan Commelin (Nov 07 2018 at 20:07):

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

#### Johan Commelin (Nov 07 2018 at 20:07):

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

#### Johan Commelin (Nov 07 2018 at 20:07):

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

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

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

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

#### Johan Commelin (Nov 07 2018 at 20:21):

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

#### Johan Commelin (Nov 07 2018 at 20:22):

Especially the case for a basis.

#### Johan Commelin (Nov 07 2018 at 20:22):

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

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

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

#### Johan Commelin (Nov 07 2018 at 20:26):

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

Anyway...

#### Johan Commelin (Nov 07 2018 at 20:28):

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

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

#### Johan Commelin (Nov 07 2018 at 20:43):

Anyone who wants to step in: please go ahead!

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

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

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

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

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

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

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

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

#### Johan Commelin (Nov 08 2018 at 05:27):

@Mario Carneiro @Johannes Hölzl :up:

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


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

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

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

#### Scott Morrison (Nov 08 2018 at 09:33):

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

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

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

#### Johan Commelin (Nov 13 2018 at 21:07):

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

#### Reid Barton (Nov 13 2018 at 21:21):

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

#### Johan Commelin (Nov 14 2018 at 11:27):

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

#### 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 $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 (Nov 14 2018 at 19:15):

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

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

#### Johan Commelin (Nov 14 2018 at 19:16):

So, should we go with to_left or forget_to_left?

#### Scott Morrison (Nov 14 2018 at 19:18):

How about just fst and snd?

#### Scott Morrison (Nov 14 2018 at 19:19):

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

#### Johan Commelin (Nov 14 2018 at 19:19):

Ok, fine with me.

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


#### Johan Commelin (Nov 14 2018 at 19:24):

@Scott Morrison Should I push this to limits?

yes, thanks

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

#### Johan Commelin (Nov 14 2018 at 19:28):

Aah, hmm. I pushed already.

#### Johan Commelin (Nov 14 2018 at 19:28):

But yes, that might be a good idea.

#### Johan Commelin (Nov 14 2018 at 19:29):

But doesn't that lead to conflicts?

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

#### Johan Commelin (Nov 14 2018 at 19:32):

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

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

#### Scott Morrison (Nov 14 2018 at 22:33):

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

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

#### Mario Carneiro (Nov 15 2018 at 05:30):

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

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

#### Mario Carneiro (Nov 15 2018 at 05:31):

and llcomp is linear in a really high order type

#### Johan Commelin (Nov 15 2018 at 05:32):

So in this case you would propose ffst and fsnd?

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

#### Johan Commelin (Nov 15 2018 at 05:33):

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

#### Scott Morrison (Nov 15 2018 at 05:33):

You mean a typeclass on the underlying function of objects?

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

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

#### Johan Commelin (Nov 15 2018 at 05:34):

Or am I dreaming?

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

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

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

ah,

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

#### Scott Morrison (Nov 15 2018 at 05:40):

But that's not an obstacle in itself.

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

#### Scott Morrison (Nov 15 2018 at 05:41):

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

#### Scott Morrison (Nov 15 2018 at 05:42):

the problem is you can't write functorial yoneda

#### Scott Morrison (Nov 15 2018 at 05:42):

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

#### Scott Morrison (Nov 15 2018 at 05:42):

and where would that come from?

#### Scott Morrison (Nov 15 2018 at 05:43):

the category structure is only on the bundled functors

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

#### Scott Morrison (Nov 15 2018 at 05:44):

Seems a bit gross.

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

#### Johan Commelin (Nov 15 2018 at 05:58):

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

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

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

#### Mario Carneiro (Nov 15 2018 at 06:39):

with bundling linear maps

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

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

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

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

#### Mario Carneiro (Nov 15 2018 at 06:42):

but I stand by that last one

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

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

#### Johan Commelin (Nov 15 2018 at 06:44):

It is a functor from Top to Type

it's not, though

contravariant

#### Mario Carneiro (Nov 15 2018 at 06:44):

like not literally

???

#### Mario Carneiro (Nov 15 2018 at 06:44):

this is what fopens would be for

#### Mario Carneiro (Nov 15 2018 at 06:44):

you take the function and bundle it up into a functor

#### Johan Commelin (Nov 15 2018 at 06:45):

Ok, so I want instance : functorial opens

#### Mario Carneiro (Nov 15 2018 at 06:45):

this is also what scott is talking about with yoneda_2

#### Mario Carneiro (Nov 15 2018 at 06:45):

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

#### Mario Carneiro (Nov 15 2018 at 06:45):

it's still unbundled

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

#### Mario Carneiro (Nov 15 2018 at 06:46):

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

#### Johan Commelin (Nov 15 2018 at 06:46):

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

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

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

#### Mario Carneiro (Nov 15 2018 at 07:37):

the stuff about coercions is broken because of lean 3

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

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

I don't follow

#### Johan Commelin (Nov 15 2018 at 07:45):

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

#### Mario Carneiro (Nov 15 2018 at 08:02):

_root_.functor

#### Johan Commelin (Nov 15 2018 at 08:05):

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

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

#### Johan Commelin (Nov 15 2018 at 08:06):

Maybe I'm just very confused about terminology.

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


#### Mario Carneiro (Nov 15 2018 at 08:22):

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

#### Mario Carneiro (Nov 15 2018 at 08:23):

which is not necessarily an endofunctor btw

#### Mario Carneiro (Nov 15 2018 at 08:23):

I was saying that _root_.functor is unbundled

#### Mario Carneiro (Nov 15 2018 at 08:26):

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

#### Mario Carneiro (Nov 15 2018 at 08:26):

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

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

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

#### Johan Commelin (Nov 15 2018 at 08:35):

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

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

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

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

#### Johan Commelin (Nov 15 2018 at 09:03):

Aah sure, that was an "edito"

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

#### Johan Commelin (Nov 15 2018 at 09:07):

I see, that makes sense.

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

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

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

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


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

#### Johan Commelin (Nov 15 2018 at 11:29):

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

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

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

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

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

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


Looks fine.

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

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

#### Kevin Buzzard (Nov 20 2018 at 17:05):

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

#### Patrick Massot (Nov 20 2018 at 17:05):

not for poly_vars and R

#### Reid Barton (Nov 20 2018 at 17:32):

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

#### Reid Barton (Nov 20 2018 at 17:34):

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

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

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

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

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

#### Kevin Buzzard (Nov 20 2018 at 17:37):

I see, I didn't know about mk_ob

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

#### Reid Barton (Nov 20 2018 at 17:38):

using \<_, _\>

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

#### Reid Barton (Nov 20 2018 at 17:38):

Yes, looks like a good start

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

#### Kevin Buzzard (Nov 20 2018 at 17:38):

Maybe I'm writing it :-)

#### Reid Barton (Nov 20 2018 at 17:39):

I think possibly nobody has used it before

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


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


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


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

#### Reid Barton (Nov 29 2018 at 16:14):

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

#### Reid Barton (Nov 29 2018 at 16:20):

And I guess we should state these simultaneously somehow

#### Johan Commelin (Nov 29 2018 at 17:13):

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

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

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

No

#### Johan Commelin (Nov 29 2018 at 17:26):

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

#### Reid Barton (Dec 03 2018 at 04:21):

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

#### Reid Barton (Dec 03 2018 at 04:22):

Nothing is defeq to anything...

#### Reid Barton (Dec 03 2018 at 04:43):

Maybe we should just not do anything here?

#### Johan Commelin (Dec 03 2018 at 05:22):

What does "not do anything" mean?

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

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

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

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

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

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

#### Johan Commelin (Dec 03 2018 at 18:33):

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

#### Reid Barton (Dec 03 2018 at 18:33):

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

#### Reid Barton (Dec 03 2018 at 18:33):

it's a right adjoint

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

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

#### Reid Barton (Dec 03 2018 at 18:36):

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

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

#### Johan Commelin (Dec 03 2018 at 18:38):

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

#### Reid Barton (Dec 03 2018 at 18:38):

functor.of_function and similar things

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

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

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

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

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

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

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

#### Scott Morrison (Dec 04 2018 at 07:31):

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

#### Johan Commelin (Dec 04 2018 at 07:39):

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

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

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

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

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

#### Johan Commelin (Dec 04 2018 at 14:22):

I think I agree with both of you.

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

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

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

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

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

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

#### Reid Barton (Dec 04 2018 at 19:12):

No, don't do that

#### Reid Barton (Dec 04 2018 at 19:13):

Better: provide specialized ways to construct is_limit cones

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

#### Scott Morrison (Dec 04 2018 at 19:15):

(supposing we're in an algebraic category)

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

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

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

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

#### Reid Barton (Dec 04 2018 at 19:18):

What two functors?

#### Reid Barton (Dec 04 2018 at 19:20):

Do you mean Type x Type -> Type?

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

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

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

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

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

#### Scott Morrison (Dec 04 2018 at 20:54):

And learn what we need from that development.

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

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

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

#### Johan Commelin (Dec 09 2018 at 17:47):

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

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

#### Reid Barton (Dec 09 2018 at 20:39):

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

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

#### Kevin Buzzard (Dec 12 2018 at 22:05):

What does whisker mean?

#### Kevin Buzzard (Dec 12 2018 at 22:05):

I know what a cocone is.

#### Scott Morrison (Dec 12 2018 at 22:09):

No, sorry, haven't done this.

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

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

#### Reid Barton (Dec 12 2018 at 22:18):

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

#### Scott Morrison (Dec 12 2018 at 22:31):

I agree, these would be good changes.

#### Johan Commelin (Dec 13 2018 at 05:52):

Only seeing this now, but sounds good to me.

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

#### Johan Commelin (Dec 15 2018 at 10:21):

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

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

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

#### Mario Carneiro (Dec 15 2018 at 17:08):

Any advice on where to focus?

(eg #503, #505)

#### Reid Barton (Dec 15 2018 at 17:18):

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

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

Indeed

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

#### Mario Carneiro (Dec 15 2018 at 17:34):

I'm not sure about the op thing though

#### Mario Carneiro (Dec 15 2018 at 17:35):

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

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

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

#### Mario Carneiro (Dec 15 2018 at 17:37):

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

#### Reid Barton (Dec 15 2018 at 17:37):

Oh yeah, that could be annoying...

#### Mario Carneiro (Dec 15 2018 at 17:38):

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

#### Mario Carneiro (Dec 15 2018 at 17:38):

I tend to shy away from it for that reason

#### Reid Barton (Dec 15 2018 at 17:40):

I notice that PR doesn't build currently anyways

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

#### Johan Commelin (Dec 15 2018 at 17:49):

@Mario Carneiro Thanks for the merges!

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

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

#### Mario Carneiro (Dec 15 2018 at 18:28):

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

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


#### Johan Commelin (Dec 15 2018 at 18:37):

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

#### Patrick Massot (Dec 15 2018 at 18:38):

it's a variation on dunfold

#### Patrick Massot (Dec 15 2018 at 18:40):

I've never used it

#### Mario Carneiro (Dec 15 2018 at 18:56):

it's a very low level definition unfolding tactic

#### Mario Carneiro (Dec 15 2018 at 18:57):

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

#### Mario Carneiro (Dec 15 2018 at 18:57):

although I guess in this case dunfold suffices

#### Mario Carneiro (Dec 15 2018 at 19:00):

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

#### Mario Carneiro (Dec 15 2018 at 19:00):

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

#### Patrick Massot (Dec 15 2018 at 19:01):

I knew I saw it not a long time ago!

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

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

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

#### Johan Commelin (Dec 21 2018 at 03:02):

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

#### Scott Morrison (Dec 21 2018 at 03:22):

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

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

#### Johan Commelin (Dec 21 2018 at 08:17):

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

#### Mario Carneiro (Dec 21 2018 at 08:18):

okay, then progress it

#### Johan Commelin (Dec 21 2018 at 08:18):

I think the rest is fine.

#### Mario Carneiro (Dec 21 2018 at 08:18):

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

#### Johan Commelin (Dec 21 2018 at 09:04):

Done (finally): #550

#### Scott Morrison (Dec 21 2018 at 10:15):

Thanks @Johan Commelin.

Last updated: May 06 2021 at 18:20 UTC