forget₂ : CommRingCat ⥤ RingCat preserves epimorphisms

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

open CategoryTheory Functor

instance : (forget₂ CommRingCat RingCat).PreservesEpimorphisms := sorry

[Kenny Lau]

Proof sketch: let f : X ⟶ Y be a morphism in CommRingCat, and g₁ g₂ : forget₂.obj Y ⟶ Z two morphisms in RingCat.

Note that $g_1(Y)$ is a commutative subring of Z (even though Z is not commutative), and same for $g_2(Y)$, so one can form the product $g_1(Y) \times g_2(Y)$ instead of using Z, which (the product) is commutative, so everything goes through the original CommRingCat (maybe using the adjoint functor (!) to make it a neater argument).

[Kenny Lau]

(note that the adjoint of forget₂ is not in Mathlib :melt: )

[Kenny Lau]

diagram:
image.png

[Kenny Lau]

another roadblock here is that we still don't have Subring.IsComm

[Kenny Lau]

@Edison Xie what's the current status of Subring.IsComm?

[Aaron Liu]

Kenny Lau said:

(maybe using the adjoint functor (!) to make it a neater argument).

How does this work?

[Kenny Lau]

@Aaron Liu we have a special adjoint here satisfying LRX = X

[Kenny Lau]

specific to the case CRing => Ring

[Kenny Lau]

(aka counit is iso)

[Joël Riou]

Kenny Lau said:

Note that $g_1(Y)$ is a commutative subring of Z (even though Z is not commutative), and same for $g_2(Y)$, so one can form the product $g_1(Y) \times g_2(Y)$ instead of using Z...

I think you should be more explicit about what you mean by "instead of using Z".

[Kenny Lau]

@Joël Riou Z is not a commutative ring, but $g_1(Y) \times g_2(Y)$ is

[Kenny Lau]

and by "instead" I mean that you can form a new statement by replacing Z with $g_1(Y) \times g_2(Y)$

[Kenny Lau]

so that you get a diagram in CommRingCat

[Joël Riou]

How do you use that f is an epi?

[Kenny Lau]

the new diagram is in CommRingCat so you can use f epi there

[Kenny Lau]

category theoretically, this proof uses three facts:

1. the image of a morphism R(Y) -> Z factors through CRing
2. product exists in CRing and Ring and is preserved by R
3. LRX = X
   (L is left adjoint, R : CRing => Ring is right adjoint)

[Joël Riou]

I think there are missing facts.

[Kenny Lau]

i mean, i don't even know if my proof works, i just made it up

[Kenny Lau]

but what's missing?

[Kenny Lau]

probably that R is fully faithful?

[Joël Riou]

I believe you should investigate this more: in order to use f is epi, you need to introduce two morphisms $Y \rightarrow g_1(Y)\times g_2(Y)$ (and I can see only one).

[Kenny Lau]

oh... hmm

[Kenny Lau]

do you know a faster categorical argument?

[Joël Riou]

I do not know any argument.