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 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 internal-categories k-theory lie-theory limits linear linear-algebra locale localization logic mathematics measure 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 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).

nLab > Latest Changes: axiom of separation

Bottom of Page

1 to 33 of 33

  1.  
    • CommentRowNumber1.
    • CommentAuthorTobyBartels
    • CommentTimeSep 5th 2011

    This finally exists: axiom of separation.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeSep 6th 2011

    Hooray, thanks! I edited the comment about autology to accord with my answer in the other thread.

    • CommentRowNumber3.
    • CommentAuthorFinnLawler
    • CommentTimeJan 20th 2014

    New page at comprehension, describing Lawvere’s version of the comprehension schema in a hyperdoctrine, and also Jacobs’s variant.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2014

    Thanks, nice, I had not been aware of this.

    I have added the tautological example (the hyperdoctrine over SetSet of posets of subsets) to offer the reader help to see what the abstract definition is trying to achieve.

    Apart from this I made two trivial formatting edits, please feel free to disagree:

    • gave Lawvere’s and Jacobs’ definition separate subsection

    • changed the notation EXE X for the fibers to E XE_X (okay?)

    • CommentRowNumber5.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2014

    I have also made “comprehension scheme” a redirect and added links to old entries mentioning comprehension, such as second-order arithmetic and Trimble on ETCS III.

    I notice that looking at axiom of separation that the relation between the two entries remains a bit vague at the moment.

    • CommentRowNumber6.
    • CommentAuthorFinnLawler
    • CommentTimeJan 21st 2014

    Looks fine. I’ve done some minor tidying-up, and added the example of the category of elements of a presheaf.

    • CommentRowNumber7.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2014

    Since you use the word “extension” now, should we add a remark that if the right adjoint exists, then it is called “extension”. So that “comprehension means that we have extension.” Is that the right way of speaking?

    • CommentRowNumber8.
    • CommentAuthorFinnLawler
    • CommentTimeJan 21st 2014

    Yes, good point. I have rephrased things slightly.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeJan 21st 2014
    • (edited Jan 21st 2014)

    We have an old stub entry extension (semantics) which used to just point to Wikipedia and otherwise receive a link from extensional type theory.

    I have added a bare minimum to extension (semantics) and cross-linked it with comprehension.

    • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeJan 26th 2014

    I’m inclined to say that the contents of comprehension belong in axiom of separation, in the (so far quite brief) section on structural versions. It is the same axiom. (Note that a few axioms called ‘comprehension’ are defined at axiom of separation; also, axiom of comprehension and several variants already redirect there, although the particular phrases that currently redirect to comprehension.)

    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeJan 26th 2014

    That sounds very reasonable to me. I am in favor of merging the entries. (But I won’t do it myself, now.)

    • CommentRowNumber12.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 26th 2014

    There’s something else called the “comprehensive factorization”, but I can’t remember now how it goes. Maybe someone can add something to this effect, if it can be made to fit?

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeJan 26th 2014

    there is comprehensive factorization (michaelshulman).

    But is “comprehensive” here really related to “comprehension”?

    • CommentRowNumber14.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 26th 2014

    Thanks, Urs. I’m going to have to study what Mike wrote to remind myself how this is supposed to go, but if I remember correctly there is supposed to be a connection (it was originally called the comprehensive factorization because of some connection with comprehension).

    It has something to do with generalizing the fact that an external predicate or relation on a set AA, given by a monomorphism S↪AS \hookrightarrow A, is ’reified’ by a function A→ΩA \to \Omega or an element 1→P(A)1 \to P(A), only that in Mike’s context we are replacing relations by discrete op-fibrations over AA and functions A→ΩA \to \Omega by functors A→SetA \to Set, or at least so in the motivating examples. So comprehension is supposed to be abstracted: in a hyperdoctrine S:E op→PosS: E^{op} \to Pos (with motivating example Sub:E op→PosSub: E^{op} \to Pos, with EE a topos), comprehension allows us to ’reflect’ a predicate p∈S(E)p \in S(E) down into a morphism in the base category EE. In the generalization we consider instead the pseudofunctor S:E op→CatS: E^{op} \to Cat corresponding to a fibration, and then factor through a discrete fibration…

    Sorry, I realize that I’m making a mess here and am speaking something close to gibberish – I’ll have to think harder, or maybe someone can help out. I thought there was supposed to be a connection (due originally to Lawvere).

    • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 26th 2014
    • (edited Jan 26th 2014)

    Well, instead of watching me babble here, maybe try this link where Claudio Hermida explains it. At least my memory wasn’t completely fabricated. (Maybe to babble a bit further, though, the factorization of a fibration F→AF \to A through a discrete op-fibration is supposed to remind one of a classifier A→ΩA \to \Omega, where Ω\Omega is now standing for SetSet and A→SetA \to Set classifies the discrete op-fibration.)

    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeJan 26th 2014

    Ah, thanks. I’ll try to read this when I have a minute.

    • CommentRowNumber17.
    • CommentAuthorFinnLawler
    • CommentTimeJan 26th 2014

    I was planning to add something on the comprehensive factorization to comprehension when I got the chance, so I’ll do that this evening, and move the whole lot to axiom of separation at the same time.

    There’s nothing complicated about the factorization system, really: a fibration with full comprehension gives a subfibration of the codomain fibration, and if the resulting ’subtype inclusions’ are closed under composition, then that gives you a factorization system on the base category (this is in Carboni et. al., On localization and stabilization for factorization systems). The factorization of a morphism is the commuting triangle given by the unit of the reflection. For the subobject fibration of a regular category this is the usual epi-mono factorization, whereas for the presheaf fibration over Cat it gives the factorization of an arbitrary functor into a final functor followed by a discrete fibration.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeJan 26th 2014

    When you do these edits, I suppose you could cross-link with reflective factorization system and stable factorization system.

    • CommentRowNumber19.
    • CommentAuthorFinnLawler
    • CommentTimeJan 26th 2014

    Right, I’ve moved everything to axiom of separation and added a section on the comprehensive factorization, as well as a redirect from the page comprehension. I’ve blanked the latter, but now I’m not sure whether that’s the right thing to do in this situation.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeJan 26th 2014
    • (edited Jan 26th 2014)

    Thanks!

    I have also renamed the now blank page to something (to “comprehension >\gt history” as it were, but it does not matter much) (and made sure to kill the automatically created redirect in the process)

    • CommentRowNumber21.
    • CommentAuthorMike Shulman
    • CommentTimeJan 27th 2014

    Could also cross-link factorization system in a 2-category?

    • CommentRowNumber22.
    • CommentAuthorFinnLawler
    • CommentTimeJan 27th 2014

    I’ve given it a mention, beside the link to your page comprehensive factorization (michaelshulman). (Note to self: read and understand that page!)

    • CommentRowNumber23.
    • CommentAuthorUrs
    • CommentTimeJan 29th 2014
    • (edited Jan 29th 2014)

    Mike just indirectly reminded me elsewhere of my going off into the blue in the thread on Finn’s thesis about dependent linear type theory and comprehension. Thinking about it, let me have another go:

    Isn’t it right that: a linear hyperdoctrine having Lawvere-ian comprehension means equivalently that it has a dependent !-modality

    ?

    Here I am assuming that in the definition of Lawvere-ian comprehension we say we are pushing the tensor unit instead of pushing the terminal object, which anyway seems to be a more robust way of going about it, I’d think.

    Then following Ponto-Shulman 12, (4.3) (and using that by linear Frobenius reciprocity context extension/pullback preserves tensor units) the linearization functor Σ\Sigma is

    Σ:H /X⟶Mod(X) \Sigma \;\colon\; \mathbf{H}_{/X} \longrightarrow Mod(X)

    given by sending any (p:Y→X)∈H X(p : Y \to X) \in \mathbf{H}_X to p !1 Y∈Mod(X)p_! 1_Y \in Mod(X) and this having a right adjoint RR that induces the dependent linear type theory ! X!_X-comonad is precisely Lawvere’s comprehension in this case.

    Right?

    • CommentRowNumber24.
    • CommentAuthorMike Shulman
    • CommentTimeJan 29th 2014

    Yes, exactly. That’s what I was trying to say “elsewhere”.

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeJan 29th 2014

    Okay, thanks.

    I have now briefly recorded this at comprehension – Examples – In linear dependent type theory. Also cross-linked with dependent linear type theory.

    Created a stub for !-modality in the process.

  26. This is a minor comment, but I did some digging up of references and noticed that what is described in the article as “Jacobs’ reformulation” is actually from Thomas Ehrhard’s thesis. That is stated clearly in Jacobs’ older article, “Comprehension categories and the semantics of type dependency”, and see also Ehrhard’s A Categorical Semantics of Constructions. I don’t have time to edit the article now, but will try to do it next week if no one gets around to it earlier.

    • CommentRowNumber27.
    • CommentAuthortonyjones
    • CommentTimeFeb 27th 2016

    Any thoughts on Bart Jacobs recent work on Quotient-Comprehension Chains? http://arxiv.org/abs/1511.01570 ”This paper reveals that quotients and comprehension are related to measurement, not only in quantum logic, but also in probabilistic and classical logic”

    Also his work on the notion of effectus? http://arxiv.org/abs/1512.05813 “Effectus theory is a new branch of categorical logic that aims to capture the essentials of quantum logic, with probabilistic and Boolean logic as special cases. Predicates in effectus theory are not subobjects having a Heyting algebra structure, like in topos theory, but ‘characteristic’ functions, forming effect algebras. Such effect algebras are algebraic models of quantitative logic, in which double negation holds. Effects in quantum theory and fuzzy predicates in probability theory form examples of effect algebras.”

    • CommentRowNumber28.
    • CommentAuthorMike Shulman
    • CommentTimeDec 3rd 2018

    As far as I can tell, Ehrhard’s definition of comprehension requires not just that the fibers have terminal objects but that these are preserved by the reindexing functors. This is automatic if the fibration is a bifibration, as in Lawvere’s version; it’s fairly explicit in Ehrhard’s formulation, and somewhat implicit in Jacobs’ but I believe still present (his “terminal object functor” must, I think, be a fibered terminal object).

    diff, v14, current

    • CommentRowNumber29.
    • CommentAuthorMike Shulman
    • CommentTimeDec 3rd 2018

    BTW, this new thread could be merged with this one and (more obviously, but less interestingly) this one.

  30. Re #29: Done. Comments #1 and #2 are from a Latest Changes thread entitled ’The axiom of separation’, the second of the two threads that Mike mentioned. Comments #3- #27 are from a Latest Changes thread entitled ’comprehension’, the first of the two threads that Mike mentioned.

  31. Adding disambiguation message to top of page

    Anonymous

    diff, v19, current

    • CommentRowNumber32.
    • CommentAuthorrisingtides
    • CommentTimeOct 29th 2023

    Add a temporary reference to Shulman’s paper (https://arxiv.org/abs/1004.3802) for the definition of autological category. An “autological category” page should be made eventually (or created as a subsection of the “axiom of separation” page).

    diff, v23, current

    • CommentRowNumber33.
    • CommentAuthorvarkor
    • CommentTimeNov 29th 2023

    Added a reference to Clemens Berger and Ralph M. Kaufmann’s Comprehensive Factorization Systems.

    diff, v24, current

1 to 33 of 33

  1.