Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: collecting proofs that RxS is a Rng just when R,S are rings

Eric M Downes (Apr 02 2024 at 17:41):

$R,S\in \mathsf{Rng}\implies R\times S\in\mathsf{Rng}$
One can approach this simple fact at many levels of sophistication. What's your favorite level?

Sketches I can think of:

• elementary proof -- manipulate generic elements, check axioms
• Lawvere theory translation of elementary proof using $\mu_{R\times S}:=(\mu_R\times\mu_S)\circ(23)$ etc.
• $\mathsf{Rng}$ is complete, so has all limits so has products, and is concrete, product is cartesian
• $\mathsf{Rng}$ is a composition of monads ($\mathsf{Ab ⨾ Mon}$) from categories where products exist, and we have a distributive law, apply $\circ,\times$-distributivity
• something something model category, fibrant replacement?

I want more! Just collecting key concepts for now, you don't need to write the proof, but referencing nLab / standard terminology preferred.

Side-stepping the fascinating topic of intensional identity types, I am less concerned at this time with wether these proofs are "truly different" (mostly they aren't?) and more interested in what concepts you personally would use when considering this fact. What's your own opinion about the "correct" level of generality, or just your preferred level of generality today.

(If this should instead be in community: discussion lemme know! thx)

John Baez (Apr 02 2024 at 18:11):

I guess if I wanted to mininize work I'd say that rings are defined by a Lawvere theory, so the category of rings has products and the forgetful functor to Set is a right adjoint hence preserves products. All of this has nothing to do particular to do with rings; it works for any Lawvere theory.

So, this is like some blend of your second and third arguments... but really there is no need for mucking around with formulas like $\mu_{R \times S} = (\mu_R \times \mu_S) \circ (23)$. The fact that the operations on a product of a ring are defined componentwise is another way of saying that the projections $R \times S \to R, R \times S \to S$ are homomorphisms, which comes from the category of rings having binary products.

John Baez (Apr 02 2024 at 18:12):

There must also be an argument parallel to the one I gave but phrased in the language of traditional universal algebra, since the argument works for any variety. However, I fear that in traditional universal algebra they'd have to muck around with a lot of syntax.

Eric M Downes (Apr 02 2024 at 20:00):

Good point. Birkoff's HSP variety theorem is intermediate between bog-standard undergrad math and categories; define a lattice closure (which will be familiar from topology) and a variety. I think it makes a nice transition and motivation for the more abstract categorical picture, actually.

Harold Kimmey (Apr 05 2024 at 17:31):

John Baez said:

I guess if I wanted...

Thinking back to UseNet newsgroup days. Is there a conical list, web site, or database of the majority of mathematical proofs?
(apologize if I posted in the wrong topic... - I'm new here).

Eric M Downes (Apr 05 2024 at 19:06):

Not too many categorical proofs here, but
https://proofwiki.org/wiki/Main_Page