feat(category_theory): opposites, and the category of types #249

semorrison · 2018-08-11T15:01:43Z

This adds

opposite categories and functors
the category of types
universe lifting for types
some lemmas about functors and transformations into the category of types
the hom pairing as a functor
an extensionality lemma for ulift

digama0 · 2018-08-13T06:35:56Z

category_theory/opposites.lean

+variables {D : Type u₂} [𝒟 : category.{u₂ v₂} D]
+include 𝒟
+
+definition opposite (F : C ↝ D) : (Cᵒᵖ) ↝ (Dᵒᵖ) := 


this could be just op, protected

digama0 · 2018-08-13T06:39:05Z

category_theory/opposites.lean

+
+variable (C)
+
+definition hom_pairing : (Cᵒᵖ × C) ↝ (Type v₁) := 


Hm, to me this is not an obvious name. I guess this is the functor mathematicians call Hom(-,-); can we call it Hom or functor.Hom or functor.hom? Or are you trying to call attention to the fact that this is an uncurried functor?

This is a fairly common name amongst mathematicians (ha!): the idea is that it is a pairing, like the pairing between a vector space and its dual. I think the common usage is just because "the hom functor for C" doesn't really specify what you mean, but "the hom pairing for C" is unambiguously a "bilinear" thing, i.e. a functor out of Cᵒᵖ × C.

I can change it to just functor.hom, but I think this is more descriptive.

Another thing: I've been thinking that the field category.Hom should be category.hom. What do you think?

Re: category.hom: I think that's a good idea, and it will free Hom up for other uses (such as here?).

I think "hom pairing" sounds more like a way to speak the symbol in a mathematical context without the opportunity for notational or typing disambiguation. In our case, I think this should be called functor.hom rather than functor.hom_pairing, unless you think that there is another definition that has a better claim to the name functor.hom. (I thought about the curried version of this functor, but I guess that's usually called yoneda or a variant...)

digama0 · 2018-08-13T06:40:21Z

category_theory/products.lean

-@[simp, ematch] lemma prod_obj (F : A ↝ B) (G : C ↝ D) (a : A) (c : C) : F.prod G (a, c) = (F a, G c) := rfl
-@[simp, ematch] lemma prod_map (F : A ↝ B) (G : C ↝ D) {a a' : A} {c c' : C} (f : (a, c) ⟶ (a', c')) : (F.prod G).map f = (F.map f.1, G.map f.2) := rfl
+@[simp, ematch] lemma prod_obj  (F : A ↝ B) (G : C ↝ D) (a : A) (c : C) : (functor.prod F G)     (a, c) = (F a, G c) := rfl
+@[simp, ematch] lemma prod_map  (F : A ↝ B) (G : C ↝ D) {a a' : A} {c c' : C} (f : (a, c) ⟶ (a', c')) : (functor.prod F G).map f = (F.map f.1, G.map f.2) := rfl


What happened here? I liked it better before - did projection stop working?

Projection is still fine. It just looked awfully lopsided to me, for a very symmetric construction: like F was doing something to G, rather than just combining them side by side. The projection notation here saves 6 characters, but not much else that I can see.

I can of course change it back if you say so!

I like to think of the projection notation as a poor-man's binary operator, since it puts the word in infix position. For uniformity I also remove unnecessary parentheses in places like this.

Part of my "what happened here" reaction was on the inclusion of strange extra spaces, though.

digama0 · 2018-08-13T06:40:58Z

category_theory/types.lean

+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Stephen Morgan, Scott Morrison
+
+import .functor_category


No relative imports

digama0 · 2018-08-15T14:06:21Z

category_theory/types.lean

+
+end functor_to_types
+
+definition type_lift : (Type u) ↝ (Type (max u v)) := 


I think this should just be called ulift or functor.ulift

also explaining the lack of notation for functor.prod and nat_trans.prod

semorrison · 2018-08-17T11:05:36Z

I think this has fixed all the suggestions above; thanks!

johoelzl · 2018-08-17T17:09:41Z

Does it make sense to de-bundle hom? I.e. have it as a parameter to category instead of as a field?

digama0 · 2018-08-17T17:41:20Z

This was an option we discussed during the plans leading to the first PR. I think the problem is that it makes it a lot more cumbersome to talk about specific categories, since you will always have to mention both the objects and the morphisms, i.e. "the category of groups and group homomorphisms" instead of "the category of groups". Since we don't usually have a terse notation for the homs, this is even more inconvenient. I can imagine that in some circumstances it can be useful to separate the homs out, but I think that the primary class for categories should be half-bundled like this.

semorrison · 2018-08-17T22:15:25Z

Further to Mario's comment, if you want to talk about multiple category structures on the same objects, it seems fairly straightforward to just use wrapper definitions as in `category_theory/opposities.lean`. I think even this is quite intuitive to mathematicians, who will just read the wrapper as a little flag "oh, I'm thinking of it as an object in this other category now". (I probably should add an explanation of this in the documentation.) The current setup seems quite usable and notationally convenient (the glaring exception being having to specify the universe levels of the homs manually when declaring `category` variables), and moreover close to standard mathematical usage. If there's a particular use case where unbundling further seems useful I'd by happy to investigate it further.

…

On Sat, Aug 18, 2018 at 3:41 AM Mario Carneiro ***@***.***> wrote: This was an option we discussed during the plans leading to the first PR. I think the problem is that it makes it a lot more cumbersome to talk about specific categories, since you will always have to mention both the objects and the morphisms, i.e. "the category of groups and group homomorphisms" instead of "the category of groups". Since we don't usually have a terse notation for the homs, this is even more inconvenient. I can imagine that in some circumstances it can be useful to separate the homs out, but I think that the primary class for categories should be half-bundled like this. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#249 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAdLBKrRxTot31iCgPMHPdO5n7JnXZlJks5uRwBBgaJpZM4V5MmV> .

semorrison added 5 commits August 11, 2018 16:18

fix(category_theory): consistent use of coercions, consistent naming

3cc4266

better naming

4ab4110

feat(category_theory): opposites, and the category of types

ed06add

minor: typo and formatting

4c32476

using ext more, apply less

52246b1

digama0 reviewed Aug 13, 2018

View reviewed changes

review corrections

cf76212

digama0 reviewed Aug 15, 2018

View reviewed changes

semorrison added 5 commits August 17, 2018 20:19

fixing relative imports

0d6b7ca

renaming fields

10a03b9

renaming hom_pairing

4bd617a

fixing spacing

8055b68

also explaining the lack of notation for functor.prod and nat_trans.prod

merge

670d159

digama0 merged commit cfb27cb into leanprover-community:master Aug 18, 2018

semorrison deleted the category_theory_3 branch August 18, 2018 10:01

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(category_theory): opposites, and the category of types #249

feat(category_theory): opposites, and the category of types #249

semorrison commented Aug 11, 2018

digama0 Aug 13, 2018

semorrison Aug 13, 2018

digama0 Aug 13, 2018

semorrison Aug 13, 2018

semorrison Aug 13, 2018

digama0 Aug 15, 2018 •

edited

digama0 Aug 13, 2018

semorrison Aug 13, 2018

semorrison Aug 13, 2018

digama0 Aug 15, 2018

digama0 Aug 13, 2018

semorrison Aug 13, 2018

digama0 Aug 15, 2018 •

edited

semorrison commented Aug 17, 2018

johoelzl commented Aug 17, 2018

digama0 commented Aug 17, 2018

semorrison commented Aug 17, 2018 via email


		variable (C)

		definition hom_pairing : (Cᵒᵖ × C) ↝ (Type v₁) :=


		end functor_to_types

		definition type_lift : (Type u) ↝ (Type (max u v)) :=

feat(category_theory): opposites, and the category of types #249

feat(category_theory): opposites, and the category of types #249

Conversation

semorrison commented Aug 11, 2018

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

digama0 Aug 15, 2018 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

digama0 Aug 15, 2018 • edited

Choose a reason for hiding this comment

semorrison commented Aug 17, 2018

johoelzl commented Aug 17, 2018

digama0 commented Aug 17, 2018

semorrison commented Aug 17, 2018 via email

digama0 Aug 15, 2018 •

edited

digama0 Aug 15, 2018 •

edited