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

1. • CommentRowNumber1.
   • CommentAuthorTodd_Trimble
   • CommentTimeAug 22nd 2012
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI added to [[allegory]] a section on division allegories and power allegories.

   I added to allegory a section on division allegories and power allegories.

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeOct 24th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexI've now moved power allegories into its own section and have expanded it to include an account I've developed over the last week or so, thus putting to rest some questions that had been hanging over what I wrote a little more than four years ago (as you can see from the previous comment). I'd like to mention some things about this here. I don't know how many of you have read the Freyd-Scedrov account of power allegories (and as for me, I haven't read what Johnstone does in the Elephant), but I prefer something different to F-S. It would be nice if one could simply say, naively, "a power allegory is an allegory $\mathcal{A}$ such that the inclusion $i: Map(\mathcal{A}) \to \mathcal{A}$ has a right adjoint $P$"; that would be a very clean formulation. F-S *almost* say that at the beginning, but then back off to give a more complicated-looking definition involving residuated or division allegory structure. Part of the problem may be that with the naive definition, one can't quite do everything one would like, and so some extra assumption has to be built in to get a good theory off the ground. (They offer some other sort of justification for how they proceed, which I've never fully understood.) My preferred proposal at the moment is just to say this: a power allegory is an allegory *with finite coproducts* such that the inclusion $i: Map(\mathcal{A}) \to \mathcal{A}$ has a right adjoint $P$. I find that a lot easier to say and more memorable than the F-S formulation, and it's just as strong (probably a little stronger), as indicated now in [[allegory]]. Indeed, the first thing done is to show that this implies division allegory structure. To me this is sort of dual to the usual development of topos theory. In standard accounts of topos theory, the initial emphasis is on negative types (finite limits, exponentials) and negative formulas (as I try to explain in [my notes](https://ncatlab.org/toddtrimble/published/An+elementary+approach+to+elementary+topos+theory)), and then assuming we have power objects, one constructs somehow or other positive types or formulas (finite colimits, existential quantifiers, internal unions, etc.). Here, it's just the other way around: in power allegory theory as developed here, the initial emphasis is on positive types (e.g., coproducts) and positive formulas (e.g., relational composition which is all about guarded existential quantifiers), and then assuming we have power objects, one constructs negative formulas such as divisions which are guarded universal quantifiers. (And we also get at least some exponentials, but I haven't discussed this yet.) I kind of like that.

   I’ve now moved power allegories into its own section and have expanded it to include an account I’ve developed over the last week or so, thus putting to rest some questions that had been hanging over what I wrote a little more than four years ago (as you can see from the previous comment). I’d like to mention some things about this here.

   I don’t know how many of you have read the Freyd-Scedrov account of power allegories (and as for me, I haven’t read what Johnstone does in the Elephant), but I prefer something different to F-S. It would be nice if one could simply say, naively, “a power allegory is an allegory $\mathcal{A}$ such that the inclusion $i: Map(\mathcal{A}) \to \mathcal{A}$ has a right adjoint $P$”; that would be a very clean formulation. F-S almost say that at the beginning, but then back off to give a more complicated-looking definition involving residuated or division allegory structure. Part of the problem may be that with the naive definition, one can’t quite do everything one would like, and so some extra assumption has to be built in to get a good theory off the ground. (They offer some other sort of justification for how they proceed, which I’ve never fully understood.)

   My preferred proposal at the moment is just to say this: a power allegory is an allegory with finite coproducts such that the inclusion $i: Map(\mathcal{A}) \to \mathcal{A}$ has a right adjoint $P$. I find that a lot easier to say and more memorable than the F-S formulation, and it’s just as strong (probably a little stronger), as indicated now in allegory. Indeed, the first thing done is to show that this implies division allegory structure.

   To me this is sort of dual to the usual development of topos theory. In standard accounts of topos theory, the initial emphasis is on negative types (finite limits, exponentials) and negative formulas (as I try to explain in my notes), and then assuming we have power objects, one constructs somehow or other positive types or formulas (finite colimits, existential quantifiers, internal unions, etc.). Here, it’s just the other way around: in power allegory theory as developed here, the initial emphasis is on positive types (e.g., coproducts) and positive formulas (e.g., relational composition which is all about guarded existential quantifiers), and then assuming we have power objects, one constructs negative formulas such as divisions which are guarded universal quantifiers. (And we also get at least some exponentials, but I haven’t discussed this yet.) I kind of like that.

3. • CommentRowNumber3.
   • CommentAuthorMike Shulman
   • CommentTimeOct 24th 2016
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexFWIW, Johnstone writes > ... we could define a power allegory as an allegory $\mathcal{A}$ for which the inclusion $Map(\mathcal{A}) \to\mathcal{A}$ has a right adjoint. It turns out, however, that in the presence of the division operation this description may be further simplified... > A division allegory is called a *power allegory* if there is an operation assigning to each object $A$ a morphism $\in_A : P A \nrightarrow A$ satisfying $(\in_A \mid \in_A) = 1_{P A}$ and $1_B \le (\phi \backslash \in_A)(\in_A \backslash \phi)$ for any $\phi : B\nrightarrow A$. (where $(\phi\mid\psi)$ denotes $(\phi \backslash \psi) \cap (\phi^\circ / \psi^\circ)$) I haven't read what you've written here yet, but offhand I probably agree with you -- I fail to see in what way this complicated definition is "simpler" than saying that $Map(\mathcal{A}) \to\mathcal{A}$ has a right adjoint. (-:

   FWIW, Johnstone writes

   … we could define a power allegory as an allegory $\mathcal{A}$ for which the inclusion $Map(\mathcal{A}) \to\mathcal{A}$ has a right adjoint. It turns out, however, that in the presence of the division operation this description may be further simplified…

   A division allegory is called a power allegory if there is an operation assigning to each object $A$ a morphism $\in_A : P A \nrightarrow A$ satisfying $(\in_A \mid \in_A) = 1_{P A}$ and $1_B \le (\phi \backslash \in_A)(\in_A \backslash \phi)$ for any $\phi : B\nrightarrow A$.

   (where $(\phi\mid\psi)$ denotes $(\phi \backslash \psi) \cap (\phi^\circ / \psi^\circ)$)

   I haven’t read what you’ve written here yet, but offhand I probably agree with you – I fail to see in what way this complicated definition is “simpler” than saying that $Map(\mathcal{A}) \to\mathcal{A}$ has a right adjoint. (-:

4. • CommentRowNumber4.
   • CommentAuthorTodd_Trimble
   • CommentTimeOct 24th 2016
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItex(But first I'd better double-check what is going on with coproducts and biproducts in allegories... )

   (But first I’d better double-check what is going on with coproducts and biproducts in allegories… )