Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration finite foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf sheaves simplicial space spin-geometry stable-homotopy-theory stack string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorDavidRoberts
    • CommentTimeSep 3rd 2018

    Added reference to the paper

    Paul Blain Levy, Formulating Categorical Concepts using Classes, arXiv:1801.08528

    diff, v10, current

    • CommentRowNumber2.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMay 6th 2019

    What kind of properties can we expect from the “category” of classes in ZFC? In general, power objects do not exist because of Russell’s paradox, but what about (co)limits (not necessarily small) and exponentials?

    • CommentRowNumber3.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 6th 2019

    It’s a model of algebraic set theory.

    • CommentRowNumber4.
    • CommentAuthorTodd_Trimble
    • CommentTimeMay 7th 2019

    Dmitri, the category of classes is a pretopos (you can perform first-order logic internally). Exponentials are of course problematic unless one plays games with universes.

    • CommentRowNumber5.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 7th 2019

    To expand on my comment: you have a Boolean pretopos with a subobject classifier, and sets are exponentiable. More generally, I think dependent product exists along maps whose fibres are sets. You can define finite coproducts by taking the disjunction of the formulas defining the sets. Taking infinite coproducts requires infinite disjunctions. Essentially one is using Separation and carving out a subclass of VV, so need to be able to express the condition to be in the colimit you’re constructing using first-order logic, or whatever you wish to use.

    • CommentRowNumber6.
    • CommentAuthorSam Staton
    • CommentTimeMay 7th 2019
    Regarding #2 and #4, I understand that there's some difficulty around exactness (quotients by equivalence relations). Or is this not an issue in the Boolean setting?
    • CommentRowNumber7.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 7th 2019
    • (edited May 7th 2019)

    Here is an old M.SE question of mine on the issue. In particular, I eventually found this source that lays things out nicely.

    For equivalence relations, if we think of them as internal groupoids in the category of ZF-classes (no choice necessary here), then Scott’s trick cooks up a subgroupoid that is weakly equivalent, and such that each orbit consists of a set. This then has a quotient, for instance because the resulting equivalence relation is classified via a function to the power class of subsets, and the image of this function is a quotient of the new equivalence relation, and hence of the old one. I’m not sure it’s a Boolean vs Heyting thing, but it might manifest itself via the indexing of the cumulative hierarchy, which is what Scott’s trick relies on.

    More subtle is if one can generate an equivalence relation from a general (wlog symmetric reflexive) relation. This relies I think on knowing that one can take countable nested unions of subclasses of a fixed class. I’m not sure how to do this.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeMay 7th 2019
    • CommentRowNumber9.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMay 7th 2019

    Am I correct that classes in ZFC admit all small colimits, via Scott’s trick? What about small limits?

    • CommentRowNumber10.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMay 7th 2019

    On a second thought, the notion of a small diagram D:I→Class of classes must be defined carefully. I guess one could say that we have a map of classes T→Ob(I), with the fiber over i∈I being the value of D(i). This essentially postulates the existence of small coproducts by definition.

    Re #7: I do not understand why the case of arbitrary class relations is different from class equivalence relations. Given a relation R⊂C⨯C, where C is a proper class, we can define another relation S⊂C⨯C by postulating that S(x,y) holds for x,y∈C if there is a subset A⊂C together with a map g:[0,n]→A such that R(g(i),g(i+1)) holds for all i∈[0,n) and g(0)=x, g(n)=y. This defines the transitive closure of any class relation.

    • CommentRowNumber11.
    • CommentAuthorSam Staton
    • CommentTimeMay 7th 2019
    #7 -- Ah, Scott's trick, of course, you're right. Thanks.
    • CommentRowNumber12.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 7th 2019

    @Dmitri I thought of something like that, but wasn’t convinced at the time. Thanks for an independent check. Note that one doesn’t really need the subset AA, since functions [0,n]C[0,n]\to C are meaningful in ZFC.

    • CommentRowNumber13.
    • CommentAuthorDmitri Pavlov
    • CommentTimeMay 7th 2019

    Proved that the category of classes admits arbitrary colimits.

    diff, v12, current

    • CommentRowNumber14.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 8th 2019

    Added section on finite colimits of external diagrams. We need to tighten up the claim around Scott’s trick for coequalisers in an arbitrary category of classes. One needs a cumulative hierarchy to make this work, or more generally some stratification into sets with a well-founded indexing class.

    diff, v13, current

    • CommentRowNumber15.
    • CommentAuthorDavidRoberts
    • CommentTimeMay 8th 2019

    Added section on finite colimits of external diagrams. We need to tighten up the claim around Scott’s trick for coequalisers in an arbitrary category of classes. One needs a cumulative hierarchy to make this work, or more generally some stratification into sets with a well-founded indexing class.

    diff, v14, current

    • CommentRowNumber16.
    • CommentAuthorDmitri Pavlov
    • CommentTimeDec 12th 2020

    Relocated properties of the category of classes to a separate article.

    diff, v17, current

  1. added links to category of classes and type of classes

    Anonymous

    diff, v18, current

  2. renaming this to the more general notion of class.

    Anonymous

    diff, v18, current

  3. modified ideas section so that it introduces the general notion of “class” as well, rather than only the notion of “proper class”.

    Anonymous

    diff, v18, current

  4. added a few definitions of classes in certain foundations of mathematics

    Anonymous

    diff, v18, current

  5. added reference

    Anonymous

    diff, v18, current

  6. added context sidebar with foundations sidebar

    Anonymous

    diff, v18, current

  7. added links to family of sets, large set, and small set

    Anonymous

    diff, v18, current

  8. added the definition of “class” in type theory as an arbitrary modal operator (isn’t required to be idempotent or monadic) on a set-level type theory which takes sets/types to h-propositions.

    Anonymous

    diff, v20, current

  9. added the definition of class in type theory, where the propositions as types interpretation is used.

    Anonymous

    diff, v21, current

  10. added a few examples of classes

    Anonymous

    diff, v21, current