Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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

1. • CommentRowNumber1.
   • CommentAuthorMike Shulman
   • CommentTimeJan 2nd 2010
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownWrote [[generic proof]] with some comments about a couple seemingly weaker versions of the [[axiom of choice]] that I've never seen mentioned anywhere before (has anyone else?). Toby and I noticed these a little bit ago while thinking about [[exact completion]]s, but I just now realized that they're actually good for something: proving that the category of [[anafunctors]] between two small categories is essentially small (in the "projective" way).

   Wrote generic proof with some comments about a couple seemingly weaker versions of the axiom of choice that I've never seen mentioned anywhere before (has anyone else?). Toby and I noticed these a little bit ago while thinking about exact completions, but I just now realized that they're actually good for something: proving that the category of anafunctors between two small categories is essentially small (in the "projective" way).

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeFeb 21st 2013
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI wrote in some material at [[generic proof]] which replaces one of the "seemingly"s with something more definitive (that the assumption "$Set_{ex/lex}$ is wellpowered" is weaker than "$Set_{ex/lex}$ is a topos").

   I wrote in some material at generic proof which replaces one of the “seemingly”s with something more definitive (that the assumption “$Set_{ex/lex}$ is wellpowered” is weaker than “$Set_{ex/lex}$ is a topos”).

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeFeb 21st 2013
   • (edited Feb 21st 2013)
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexI added a diagram to [[generic proof]], and explanations of what $\nu^*\theta$ and $Set^\to$ mean (I assume).

   I added a diagram to generic proof, and explanations of what $\nu^*\theta$ and $Set^\to$ mean (I assume).

4. • CommentRowNumber4.
   • CommentAuthorUrs
   • CommentTimeFeb 21st 2013
   • PermaLink
   Author: Urs
   Format: MarkdownItextrivial edit: I changed an \rlap to \mathrlap The former has no effect. The latter does what you think it should do.

   trivial edit:

   I changed an

    \rlap
   

   to

    \mathrlap
   

   The former has no effect. The latter does what you think it should do.

5. • CommentRowNumber5.
   • CommentAuthorZhen Lin
   • CommentTimeFeb 21st 2013
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItexIs there a motivation behind the name? What is it a generic proof _of_?

   Is there a motivation behind the name? What is it a generic proof of?

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeFeb 21st 2013
   • (edited Feb 21st 2013)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI was about to suggest that a comment on that needs to be added. I suppose this is referring to _[Proof as in type theory](http://ncatlab.org/nlab/show/proof#Proof)_ being just a "term of a type", hence a map into some object. So a "generic proof" is like a universal bundle: any one on any given object is obtained from the generic/universal one by pulling it back along some classifying map. I won't add anything to the entry, since I don't know the background. But it would be good if somebody else did.

   I was about to suggest that a comment on that needs to be added.

   I suppose this is referring to Proof as in type theory being just a “term of a type”, hence a map into some object. So a “generic proof” is like a universal bundle: any one on any given object is obtained from the generic/universal one by pulling it back along some classifying map.

   I won’t add anything to the entry, since I don’t know the background. But it would be good if somebody else did.

7. • CommentRowNumber7.
   • CommentAuthorZhen Lin
   • CommentTimeFeb 21st 2013
   • PermaLink
   Author: Zhen Lin
   Format: MarkdownItexYes, that makes sense. I suppose its universal property is best understood in terms of some kind of fibred preorder reflection of the canonical codomain fibration of the category.

   Yes, that makes sense. I suppose its universal property is best understood in terms of some kind of fibred preorder reflection of the canonical codomain fibration of the category.

8. • CommentRowNumber8.
   • CommentAuthorTodd_Trimble
   • CommentTimeFeb 21st 2013
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexUndoubtedly related, the notion of [[tripos]] involves a notion of _generic predicate_, again involving a weak universal property that relates a base category of terms $C$ to a hyperdoctrine of predicates over $C$. It is especially easy to describe if $C$ is cartesian closed: if $Pred: C^{op} \to HeytAlg$ is the hyperdoctrine and ${|Pred|}: C^{op} \to Set$ its composition with the forgetful functor to $Set$, then a generic predicate is tantamount to weak representability of ${|Pred|}$, i.e., an object $P$ together with a given epimorphism $C(-, P) \to {|Pred|}$. The image of the identity $1_P$ as an element of ${|Pred|}(P)$ is the generic predicate in question. I don't have a very full understanding of this, but there are two paths to get from a partial combinatory algebra $A$ to a realizability topos. One is through triposes and generic predicates and involves a kind of allegorical way of passing to an exact completion: * First pass from a unitary pretabular allegory given by a tripos associated with $A$, to a unitary tabular allegory, by splitting coreflexives. This is analogous to a regular completion. * Then split equivalence relations in the unitary tabular allegory. This is analogous to taking an ex/reg completion. (The two steps can be combined into one by splitting PERs. But I find it more understandable to think of it in two steps.) The other path is through partitioned assemblies associated with $A$. This is a category with weak dependent products and a generic proof. By Menni's thesis, the exact completion of this category is a topos. I would really like to have a unified understanding of these two paths, and have this reflected in the nLab.

   Undoubtedly related, the notion of tripos involves a notion of generic predicate, again involving a weak universal property that relates a base category of terms $C$ to a hyperdoctrine of predicates over $C$. It is especially easy to describe if $C$ is cartesian closed: if $Pred: C^{op} \to HeytAlg$ is the hyperdoctrine and ${|Pred|}: C^{op} \to Set$ its composition with the forgetful functor to $Set$, then a generic predicate is tantamount to weak representability of ${|Pred|}$, i.e., an object $P$ together with a given epimorphism $C(-, P) \to {|Pred|}$. The image of the identity $1_P$ as an element of ${|Pred|}(P)$ is the generic predicate in question.

   I don’t have a very full understanding of this, but there are two paths to get from a partial combinatory algebra $A$ to a realizability topos. One is through triposes and generic predicates and involves a kind of allegorical way of passing to an exact completion:

   • First pass from a unitary pretabular allegory given by a tripos associated with $A$, to a unitary tabular allegory, by splitting coreflexives. This is analogous to a regular completion.

   • Then split equivalence relations in the unitary tabular allegory. This is analogous to taking an ex/reg completion.

   (The two steps can be combined into one by splitting PERs. But I find it more understandable to think of it in two steps.)

   The other path is through partitioned assemblies associated with $A$. This is a category with weak dependent products and a generic proof. By Menni’s thesis, the exact completion of this category is a topos.

   I would really like to have a unified understanding of these two paths, and have this reflected in the nLab.

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 21st 2013
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't quite understand the origin of the name "generic proof" either, except for the same vague intuition as in Urs's #6.

   I don’t quite understand the origin of the name “generic proof” either, except for the same vague intuition as in Urs’s #6.

10. • CommentRowNumber10.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 22nd 2013
    • PermaLink
    Author: TobyBartels
    Format: MarkdownItexEven if we don\'t know the truth, we could add the vague intuition of Urs #6 as a conjecture. It would make the whole thing seems less of a non sequitur.

    Even if we don't know the truth, we could add the vague intuition of Urs #6 as a conjecture. It would make the whole thing seems less of a non sequitur.

11. • CommentRowNumber11.
    • CommentAuthorFinnLawler
    • CommentTimeFeb 22nd 2013
    • PermaLink
    Author: FinnLawler
    Format: MarkdownItexI don't mean to highjack the thread, but I'd like to reply to what Todd wrote about the two kinds of realizability constructions: > I would really like to have a unified understanding of these two paths, and have this reflected in the nLab. So would I, and I'm writing my thesis on one aspect of that understanding, namely that you can organise predicates into either fibrations (like the effective tripos) or bicategories of relations (like Rel of the category of assemblies), and that with enough structure the 2-categories of these are equivalent. There is a(n unfinished) sketch of some of this on my personal web [here](http://ncatlab.org/finnlawler/show/thesis+--+realizability+constructions). (Do ask if you'd like to know more; I intend to flesh this out when I get time.) Here's what I'm not doing (this is all due to Pieter Hofstra): say you start with a pca $A$, e.g. the naturals with Kleene application. You can form an indexed poset that I'll call $Set(-,A)$ (even though the ordering is not the pointwise one but the 'realizability' one). The category of elements of this is the category of partitioned assemblies over $A$. For any pca $A$, the sets $P A$ and $P_* A$ of subsets and non-empty subsets of $A$ are again pcas and give indexed posets in the same way; the category of elements of $Set(-,P_* A)$ is the category of assemblies over $A$, while $Set(-,P A)$ is the realizability tripos over $A$. This last is a regular fibration, so corresponds to (what I call) a framed bicategory of relations, and the (underlying bicategory of the) coreflexive splitting of the latter is Rel of the category of assemblies over $A$. From that point on, the two paths coincide. (I'd very much like to understand the earlier parts of the two processes better, but then I'd also like to finish my thesis sometime this decade...)

    I don’t mean to highjack the thread, but I’d like to reply to what Todd wrote about the two kinds of realizability constructions:

    I would really like to have a unified understanding of these two paths, and have this reflected in the nLab.

    So would I, and I’m writing my thesis on one aspect of that understanding, namely that you can organise predicates into either fibrations (like the effective tripos) or bicategories of relations (like Rel of the category of assemblies), and that with enough structure the 2-categories of these are equivalent. There is a(n unfinished) sketch of some of this on my personal web here. (Do ask if you’d like to know more; I intend to flesh this out when I get time.)

    Here’s what I’m not doing (this is all due to Pieter Hofstra): say you start with a pca $A$, e.g. the naturals with Kleene application. You can form an indexed poset that I’ll call $Set(-,A)$ (even though the ordering is not the pointwise one but the ’realizability’ one). The category of elements of this is the category of partitioned assemblies over $A$. For any pca $A$, the sets $P A$ and $P_* A$ of subsets and non-empty subsets of $A$ are again pcas and give indexed posets in the same way; the category of elements of $Set(-,P_* A)$ is the category of assemblies over $A$, while $Set(-,P A)$ is the realizability tripos over $A$.

    This last is a regular fibration, so corresponds to (what I call) a framed bicategory of relations, and the (underlying bicategory of the) coreflexive splitting of the latter is Rel of the category of assemblies over $A$. From that point on, the two paths coincide. (I’d very much like to understand the earlier parts of the two processes better, but then I’d also like to finish my thesis sometime this decade…)

12. • CommentRowNumber12.
    • CommentAuthorZhen Lin
    • CommentTimeFeb 22nd 2013
    • (edited Feb 22nd 2013)
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItex@Todd: Johnstone (in Definition F2.2.4) uses "exemplary element" instead of "generic predicate" or "generic element". The definition is for a $\mathcal{C}$-indexed preorder $\mathbb{T}$, where $\mathcal{C}$ is cartesian closed: an **exemplary element** is an element $\xi \in \mathcal{T}^\Xi$ for some $\Xi \in \operatorname{ob} \mathcal{C}$ such that, for each $I \in \operatorname{ob} \mathcal{C}$, every object in $\mathcal{T}^I$ is isomorphic to $x^*(\xi)$ for some (not necessarily unique) $x : I \to \Xi$. Surely, the construction I suggested converts generic proofs into generic predicates? First of all, the preorder reflection is a 2-functor $\mathfrak{Cat} \to \mathfrak{Preord}$, so we can certainly do a fibrewise preorder reflection on any indexed category $\mathbb{E}$; call it $\mathbb{P}$ for now. If $\mathbb{E}$ is the self-indexing of a regular category $\mathcal{C}$ with the axiom of choice then this should be equivalent to the indexed preorder $\mathbb{S}ub (\mathcal{C})$, by the observations at [[generic proof]], and otherwise it's some kind of souped-up version of $\mathbb{S}ub (\mathbb{E})$. Regardless, a generic proof in $\mathbb{E}$ is precisely an object $\Theta$ in a fibre $\mathcal{E}^\Lambda$ such that $\Theta$, regarded as an object in $\mathcal{P}^\Lambda$, is a generic predicate in $\mathbb{P}$.

    @Todd:

    Johnstone (in Definition F2.2.4) uses “exemplary element” instead of “generic predicate” or “generic element”. The definition is for a $\mathcal{C}$-indexed preorder $\mathbb{T}$, where $\mathcal{C}$ is cartesian closed: an exemplary element is an element $\xi \in \mathcal{T}^\Xi$ for some $\Xi \in \operatorname{ob} \mathcal{C}$ such that, for each $I \in \operatorname{ob} \mathcal{C}$, every object in $\mathcal{T}^I$ is isomorphic to $x^*(\xi)$ for some (not necessarily unique) $x : I \to \Xi$.

    Surely, the construction I suggested converts generic proofs into generic predicates? First of all, the preorder reflection is a 2-functor $\mathfrak{Cat} \to \mathfrak{Preord}$, so we can certainly do a fibrewise preorder reflection on any indexed category $\mathbb{E}$; call it $\mathbb{P}$ for now. If $\mathbb{E}$ is the self-indexing of a regular category $\mathcal{C}$ with the axiom of choice then this should be equivalent to the indexed preorder $\mathbb{S}ub (\mathcal{C})$, by the observations at generic proof, and otherwise it’s some kind of souped-up version of $\mathbb{S}ub (\mathbb{E})$. Regardless, a generic proof in $\mathbb{E}$ is precisely an object $\Theta$ in a fibre $\mathcal{E}^\Lambda$ such that $\Theta$, regarded as an object in $\mathcal{P}^\Lambda$, is a generic predicate in $\mathbb{P}$.

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 22nd 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexWhoa, Part F exists now? Where can I find it?

    Whoa, Part F exists now? Where can I find it?

14. • CommentRowNumber14.
    • CommentAuthorZhen Lin
    • CommentTimeFeb 22nd 2013
    • PermaLink
    Author: Zhen Lin
    Format: MarkdownItexI'm not sure if Part F exists _in full_, but Johnstone is basically lecturing Chapter F2 as a graduate course in Cambridge this term. Perhaps he might email you a copy if you ask? All I have (so far) are paper printouts of the first three sections. Parts of Chapter F1 have also been written up, at least according to a fellow student who works in synthetic differential geometry.

    I’m not sure if Part F exists in full, but Johnstone is basically lecturing Chapter F2 as a graduate course in Cambridge this term. Perhaps he might email you a copy if you ask? All I have (so far) are paper printouts of the first three sections. Parts of Chapter F1 have also been written up, at least according to a fellow student who works in synthetic differential geometry.

15. • CommentRowNumber15.
    • CommentAuthorTodd_Trimble
    • CommentTimeFeb 22nd 2013
    • PermaLink
    Author: Todd_Trimble
    Format: MarkdownItexI have now replaced the other tentative assertion in the section [axioms of choice](http://ncatlab.org/nlab/show/generic+proof#axioms_of_choice_4) with something more definitive: another paper of Menni's shows that the exact completion of a Boolean Grothendieck topos with enough points is also a topos.

    I have now replaced the other tentative assertion in the section axioms of choice with something more definitive: another paper of Menni’s shows that the exact completion of a Boolean Grothendieck topos with enough points is also a topos.

16. • CommentRowNumber16.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 22nd 2013
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItex@Zhen: Cool! I'll probably wait for the final version; I don't exactly need more reading material right now.

    @Zhen: Cool! I’ll probably wait for the final version; I don’t exactly need more reading material right now.