Continuous algebra homomorphisms

Stream: Is there code for X?

[Scott Morrison]

Ugh, I want to talk about continuous algebra homomorphisms.

I can't bear the thought of building yet another bundled structure, with pages of API about equivalences and subobjects and so on.

[Scott Morrison]

Can I just define the category TopAlgebra and work there? :-)

[Johan Commelin]

who knows... if it works, that would be great.

[Johan Commelin]

We really need the structure bundle builder gadget that people talked about at LT2021

[Eric Wieser]

Scott Morrison said:

Can I just define the category TopAlgebra and work there? :-)

Scott, is it remotely viable to use this approach everywhere, and build the non-category API as a thin later on top of the category API?

[Scott Morrison]

The thing you immediately lose is the ability to talk about homomorphisms between objects at different universe levels.

[Scott Morrison]

This is pretty annoying.

[Eric Wieser]

Are there situations where that makes statements weaker, or is it just super annoying but not strictly limiting (in that you need ulift everywhere)?

[Kevin Buzzard]

Scott says "this is pretty annoying" wrt this universe polymorphic stuff, however I spent 25 years of my life doing research mathematics without the ability to talk about homomorphisms between objects at different universe levels and this didn't bother me in the slightest.

[Kevin Buzzard]

Sticking to homs between objects of the same type is far less of an extreme restriction than my usual "why not just let everything be Type or Prop" rant which usually comes out at this point. This lets people be universe-polymorphic but not multi-polymorphic. Do we really need maps between groups of type u and type v in any application, or do we just do them because we can?

[Eric Wieser]

There's no way to generalize over both Type and Prop without also generalizing over all universes though, right?

[Scott Morrison]

@Eric Wieser, yes, but that's still orthogonal to Kevin's point.

[Scott Morrison]

I agree, I think, Kevin. Perhaps what I meant is that "it is pretty annoying that people bring this up as an objection". :-)

[Johan Commelin]

@Kevin Buzzard you've also spent 25 years of your life believing that $R[1/fg] = R[1/f][1/g]$...

[Eric Wieser]

Ah, I misread "type or prop" as "some wildcard that covers both" not "just pick one each time"

[Kevin Buzzard]

Yes I agree that it's annoying that there's no wildcard which covers both, however mathematicians are very good at distinguishing between them (for example I was carefully taught that the recursor from nat to Type was called "construction by recursion" and the recursor to Prop was called "proof by induction"). In my teaching tools there are Type and Prop everywhere and it's very rare that I want to explicitly unify these things. Mathematicians even have an arrow $\to$ for Type and a different arrow $\implies$ for Prop.

[Eric Wieser]

Perhaps a good example of where unifying the two is useful is docs#set.Union`, which enables the bounded union notation; but I agree even those cases are rare

[Yury G. Kudryashov]

Usually at this point of discussion @Mario Carneiro comes to the room and tells us about some exotic cases in parts of math I don't understand where it's important to have different universes. I still wonder if it's easier to use category theory almost everywhere and use ulift whenever we really need different universes.

[Yury G. Kudryashov]

One downside of using category theory homs everywhere is that we loose tricks like "monoid_hom both for monoid and group homs"

[Mario Carneiro]

I'm sympathetic to this point of view, but it doesn't really work to have everything in Type u (i.e. polymorphic but with only one universe) because lots of things are in Type

[Mario Carneiro]

I mean you can get by with ulift but it's really inconvenient

[Yury G. Kudryashov]

Indeed, we can't stick to "everything in Type u" without nat.{u} and real.{u}.

[Yury G. Kudryashov]

Good point.

[Yury G. Kudryashov]

(and we probably don't want to have lots of different nats around.

[Mario Carneiro]

The theory of cardinals does essentially this

[Mario Carneiro]

omega.{u} is defined as mk (ulift nat)

[Mario Carneiro]

It's also annoying to have universe parameters that aren't inferred because you usually can't omit them, i.e. you will actually be writing nat.{u} most of the time

[Mario Carneiro]

I recall early in the category theory development I suggested pinning the second universe argument of category (for the homs) to either v=u or v=u+1, but Scott argued that we want to prove things generic over both, so now we have two universe params. And once you start doing that it's really unnatural to restrict the parametricity in some specific areas because you wind up revising it eventually anyway (like the recent example with limit)

[Yaël Dillies]

@Scott Morrison, has this ever been done? Do you still need it? If so, I can produce it in an hour or so.

[Scott Morrison]

I assume you're talking about continuous algebra homomorphism?

[Scott Morrison]

If so, no, to my knowledge we don't have these.

[Scott Morrison]

The thing to look at is the end of the proof of the Stone-Weierstrass theorem.

[Yaël Dillies]

In mathlib or in real life?

[Scott Morrison]

We have to jump through an awkward hoop to talk about a function that is both continuous and an algebra map.

[Scott Morrison]

(the implementation in mathlib)

[Scott Morrison]

I think the test for a proposed implementation of continuous algebra homomorphisms should be: "does it make that argument cleaner".

[Yaël Dillies]

Bhavik is already out there telling me to work on my example sheets instead of writing boilerplate :stuck_out_tongue: