* isomorphisms @ 2010-05-29 21:18 Eduardo J. Dubuc 2010-05-30 15:11 ` isomorphisms Colin McLarty 2010-06-01 12:57 ` Peter LeFanu Lumsdaine 0 siblings, 2 replies; 6+ messages in thread From: Eduardo J. Dubuc @ 2010-05-29 21:18 UTC (permalink / raw) To: Categories list isomorphims appear not only in examples but are essential also in the theory. For example Grothendieck defines limits and colimits of categories (as universal pseudocones) in SGA4 by means of an isomorphism of categories. Same for toposes. [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: isomorphisms 2010-05-29 21:18 isomorphisms Eduardo J. Dubuc @ 2010-05-30 15:11 ` Colin McLarty 2010-05-31 2:51 ` isomorphisms Michael Shulman 2010-06-01 12:57 ` Peter LeFanu Lumsdaine 1 sibling, 1 reply; 6+ messages in thread From: Colin McLarty @ 2010-05-30 15:11 UTC (permalink / raw) To: Categories list; +Cc: Eduardo J. Dubuc 2010/5/29 Eduardo J. Dubuc <edubuc@dm.uba.ar> Expresses my main point when I quoted Grothendieck on equivalence and isomorphism. > isomorphisms appear not only in examples but are essential also in the > theory. > For example Grothendieck defines limits and colimits of categories (as > universal pseudocones) in SGA4 by means of an isomorphism of categories. > Same for toposes. When AG says "none of the equivalences we meet in practice are isomorphisms" he has in mind lots of examples that I will not even try to survey. (For a really simple one, the category of sheaves defined as espaces etales on on a topological space versus the category of sheaves defined as suitable functors on the site of open subsets.) But when he defines functor categories, or derived categories, and a lot of other things like that, he defines them up to unique isomorphism over the data. A topos E will often be defined only up to equivalence. But, given E, its derived category is defined up to unique isomorphism and one constantly uses the fact that various induced functors are isomorphisms. AG's practice constantly distinguishes isomorphisms from equivalences, and thus distinguishes identity of objects from isomorphism of them. best, Colin [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: isomorphisms 2010-05-30 15:11 ` isomorphisms Colin McLarty @ 2010-05-31 2:51 ` Michael Shulman 2010-06-01 3:26 ` Equality and fibration Joyal, André 0 siblings, 1 reply; 6+ messages in thread From: Michael Shulman @ 2010-05-31 2:51 UTC (permalink / raw) To: Categories list It seems to me that there is an important distinction here that is not being emphasized. Isomorphisms of categories can be *technically* quite useful. Knowing that a given equivalence of categories is an isomorphism, rather than merely an equivalence, can certainly make things much simpler, or even make things possible that we didn't know how to do before. Many examples of this sort have been mentioned. Another that should be added to the list is the theory of strict 2-categories, 2-limits, 2-adjoints, and so on, all of which is defined using ordinary enriched category theory over Cat, and hence involves many isomorphisms of hom-categories. However, I find that in most or all of these examples, one is not actually interested in the fact of an isomorphism of categories for its own sake. There is no "real meaning" in the fact that two categories are isomorphic, rather than equivalent; generally it's a technical accident of how we chose to define them. It may be a very *convenient* technical accident, but it is an accident nonetheless. If we chose our definitions differently, or worked in a different foundational system (such as one where the notion of "isomorphism of categories" cannot even be defined), some or all of our isomorphisms of categories might change to become only equivalences, but I don't believe that any of the real content of category theory would go away; it would just become harder to prove. Mike [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Equality and fibration 2010-05-31 2:51 ` isomorphisms Michael Shulman @ 2010-06-01 3:26 ` Joyal, André 2010-06-02 9:34 ` Prof. Peter Johnstone 0 siblings, 1 reply; 6+ messages in thread From: Joyal, André @ 2010-06-01 3:26 UTC (permalink / raw) To: Categories list Dear category theorists, I have not been able to define the notion of Grothendieck fibration without using the equality relation between the objects of the base category. Can you? André [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: Equality and fibration 2010-06-01 3:26 ` Equality and fibration Joyal, André @ 2010-06-02 9:34 ` Prof. Peter Johnstone 0 siblings, 0 replies; 6+ messages in thread From: Prof. Peter Johnstone @ 2010-06-02 9:34 UTC (permalink / raw) To: Joyal, André; +Cc: Categories list On Mon, 31 May 2010, Joyal, André wrote: > Dear category theorists, > > I have not been able to define the notion of Grothendieck fibration > without using the equality relation between the objects of the base category. > Can you? > > André > No, because an equivalence of categories is not a Grothendieck fibration in general. However, there is a weaker version of the notion where one replaces equality by the existence of a (specified) isomorphism; there are some comments about this in my paper "Fibrations and partial products in a 2-category" in Applied Categorical Structures 1 (1993), 141--179. Peter Johnstone [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
* Re: Equality and fibration 2010-05-29 21:18 isomorphisms Eduardo J. Dubuc 2010-05-30 15:11 ` isomorphisms Colin McLarty @ 2010-06-01 12:57 ` Peter LeFanu Lumsdaine 1 sibling, 0 replies; 6+ messages in thread From: Peter LeFanu Lumsdaine @ 2010-06-01 12:57 UTC (permalink / raw) To: André; +Cc: Categories list On Mon, May 31, 2010 23:26, Joyal, André wrote: > Dear category theorists, > > I have not been able to define the notion of Grothendieck fibration > without using the equality relation between the objects of the base > category. Can you? In a dependent language (eg ML, FOLDS, etc), this can be done. The twist is that it is _not_ just some extra algebraic structure on a functor p: \E --> \C; for an arbitrary such p, as you say, the lifting conditions can't be specified without referring to equality of objects. Rather, it first of all requires the objects and arrows of \E to be dependent types over the objects of \C; then, the "equalities" needed become part of the _typing specification_ of a lifting. This refinement of the definition complicates the theory a little, but is a quite natural requirement, I think. (Just as in this setting, a fibration of types is no longer an arbitrary map f:A --> B, but rather a dependent type A over B.) ===== Precisely, you can define it as follows: Say \C is a category (i.e. a type C_0, and a dependent type C_1(a,b), for a,b: C_0, an "equality" type on C_1, and appropriate composition/identity operations). The a (cloven) Grothendieck fibration \E over \C is: a dependent type E_0(a), for a: C_0; a dependent type E_1(a,b;i,j), for a,b: C_0, i:E_0(a), j:E_0(b) (we can write just E_1(i,j), since a,b are implicit in the types of i,j); operations making this a category over E_0; and an operation which, given an arrow a,b:C_0, f:C_1(a,b), and a lift j:E_0(b) of the target, returns liftings i:E_0(a) and \bar{f}:E_1(i,j), with p(\bar{f}) = f, and appropriately cartesian. (The definition of cartesian similarly doesn't need to refer to equality of objects, since they're included in the typings.) ===== If we were dealing with higher categories, and hence didn't have equality on C_1, then we would require E_1 to be a dependent type not just over a,b:C_0 and i:E_0(a), j:E_0(b), but also over f:C_1(a,b), so the condition that \bar{f} is a lift of f would again be part of its typing. This is reminiscent of latching/matching objects etc... Cheers, -Peter. -- Peter LeFanu Lumsdaine Carnegie Mellon University [For admin and other information see: http://www.mta.ca/~cat-dist/ ] ^ permalink raw reply [flat|nested] 6+ messages in thread
end of thread, other threads:[~2010-06-02 9:34 UTC | newest] Thread overview: 6+ messages (download: mbox.gz / follow: Atom feed) -- links below jump to the message on this page -- 2010-05-29 21:18 isomorphisms Eduardo J. Dubuc 2010-05-30 15:11 ` isomorphisms Colin McLarty 2010-05-31 2:51 ` isomorphisms Michael Shulman 2010-06-01 3:26 ` Equality and fibration Joyal, André 2010-06-02 9:34 ` Prof. Peter Johnstone 2010-06-01 12:57 ` Peter LeFanu Lumsdaine
This is a public inbox, see mirroring instructions for how to clone and mirror all data and code used for this inbox; as well as URLs for NNTP newsgroup(s).