categories - Category Theory list
 help / color / mirror / Atom feed
From: Andrew Swan <wakelin.swan@gmail.com>
To: Richard Garner <richard.garner@mq.edu.au>
Cc: Jon Sterling <jon@jonmsterling.com>,
	Vaughan Pratt <pratt@cs.stanford.edu>,
	 Francis Borceux <francis.borceux@uclouvain.be>,
	 "categories@mq.edu.au" <categories@mq.edu.au>
Subject: Re: Bénabou
Date: Tue, 23 Jan 2024 11:06:45 +0100	[thread overview]
Message-ID: <CA++Rs_mqDhkhhZCkbJ=xZHhmw02OSdf+AY=5pnAMsyVrrTG5bA@mail.gmail.com> (raw)
In-Reply-To: <m04jf4or24.fsf@mq.edu.au>

[-- Attachment #1: Type: text/plain, Size: 3929 bytes --]

In the preprint that Jon mentioned I had group structures (or more
specifically the forgetful functor from families of objects with group
structures to families of objects) in mind as instances of algebras for a
monad, which are definable whenever the fibration is locally small and the
base has finite limits. That argument requires having enough internal logic
to define the free group monad. However, I think the same ideas applied
directly should show that group structures are always definable for locally
small fibrations where the base has finite limits and the fibration has
finite products, which I think would cover the examples you gave. Of
course, that would only show existence without the nice concrete
descriptions.

Best,
Andrew

On Tue, 23 Jan 2024 at 01:03, Richard Garner <richard.garner@mq.edu.au>
wrote:

>
> > One thing I learned from Thomas Streicher's paper on universes in
> > toposes is that definability is related to descent — for instance, if
> > you restrict the codomain fibration to a stable class of maps, you get
> > a full subfibration, and definability in the sense of Bénabou is the
> > gap between this subfibration and its stack completion. There is a lot
> > of potential for this idea contributing to future works in category
> > theory; for example, Mike Shulman has extended Bénabou's definability
> > from "classes" of things in a fibration (i.e. properties) to a notion
> > of definability that makes sense for structures; Andrew Swan has given
> > a very interesting and thorough investigation of this generalised
> > definability and its practical implications here:
> > https://protect-au.mimecast.com/s/vucfC91W8rCBovRjhoxKeJ?domain=arxiv.org.
>
> Definability is quite a fascinating thing. Peter Freyd's work on the
> core of a topos and the subsequent work on isotropy groups of toposes I
> find very pretty. One related thing that I am reminded of is the
> following cute fact. Possibly it is well known; I do not know the SGAs
> and EGAs very well.
>
> Suppose I have a fibration E ---> B and some X in E(b). I can consider
> the existence of an "object G(X) of group structures on X". What this
> means is a map f: G(X) ---> b in B, together with a group structure on
> f^*(X) in E(G(X)), which is universal among such in the expected way.
> Clearly this is an instance of (the more general?) definability.
>
> Let us consider this for the following fibration. The base B is the
> category of affine schemes, CRng^op. The fibre over a ring k is the
> category of formal affine k-schemes, i.e., the Ind-completion of the
> k-Alg^op. This is a full subfibration of the codomain fibration of
> Ind(k-Alg^op).
>
> In the terminal fibre of this fibration we have the affine line L =
> Spec(Z[x]). This is an internal ring object in the fibre and so we can
> form its subobject N <= L of nilpotent elements ("Spec of Z[[x]]").
>
> Now for any commutative ring k, to give a group structure on k^*(N)
> ("Spec of k[[x]]") in the category of formal affine k-schemes is to give
> a formal group law with coefficients in k. It follows that the "object
> of group structures on N" is Lazard's universal coefficient ring for a
> formal group law.
>
> What is also quite fun is to compute the object of group structures on
> the generic group O in the (codomain fibration of) the group classifier
> [Grp_fp, Set]; this turns out to be O+O. This is because, given any
> group G, there are G+G ways of making it into a group. Indeed, each g in
> G yields two group structures on G, one with x * y = x.g^-1.y, and
> another with x * y = y.g^-1.x.
>
> Richard
>
>
> ----------
>
> You're receiving this message because you're a member of the Categories
> mailing list group from Macquarie University.
>
> Leave group:
>
> https://protect-au.mimecast.com/s/7xp5C0YKgRs36KJzuDXzeK?domain=outlook.office365.com
>

[-- Attachment #2: Type: text/html, Size: 4783 bytes --]

      reply	other threads:[~2024-01-23 10:29 UTC|newest]

Thread overview: 5+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2024-01-21  9:23 Benabou Francis Borceux
2024-01-22  7:31 ` Bénabou Vaughan Pratt
2024-01-22  9:14   ` Bénabou Jon Sterling
2024-01-22 23:34     ` Bénabou Richard Garner
2024-01-23 10:06       ` Andrew Swan [this message]

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to='CA++Rs_mqDhkhhZCkbJ=xZHhmw02OSdf+AY=5pnAMsyVrrTG5bA@mail.gmail.com' \
    --to=wakelin.swan@gmail.com \
    --cc=categories@mq.edu.au \
    --cc=francis.borceux@uclouvain.be \
    --cc=jon@jonmsterling.com \
    --cc=pratt@cs.stanford.edu \
    --cc=richard.garner@mq.edu.au \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
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).