Monoidal instance on R-algebras

Stream: maths

[Amelia Livingston]

What's the mathlib-preferable way to show R-algebras are a monoidal category? You could transport an instance across the equivalence with the category of monoid objects in R-Mod, but I thought proving that the resulting structure behaves as it should might be a pain. I've emulated the file algebra.category.Module.monoidal instead, which was still a bit painful as things kept timing out. Or maybe there's a better way than these two?

[Adam Topaz]

I think Module R should just have a monoidal instance? sorry, misread

[Kevin Buzzard]

Dumb question: do we have the category of R-algebras? I guess it could be defined as some slice category in the category of rings, or perhaps directly using bumdled somehow?

[Eric Wieser]

docs#Algebra?

[Adam Topaz]

Well, I guess the question is what does "Algebra" mean? Are you thinking of commutative rings only?

[Kevin Buzzard]

I suspect that Amelia was talking about commutative R-algebras. If you drop commutativity then are they a monoidal category?

[Adam Topaz]

You can take the cartesian monoidal structure, I guess, but I assume Amelia is looking for the cocartesian structure on commutative algebras (where the tensor product is the "usual" tensor product of algebras)

[Kevin Buzzard]

She's thinking about R-schemes so I suspect that the commutative case is the relevant one.

[Scott Morrison]

Unfortunately I think you've reached the bleeding edge here. :-)

The dream way to do it is to transport the monoidal structure over from the CommMon_ (Module R), and get lucky that the transported structure is actually usable. :-)

I don't remember trying to do that myself, although it was on my radar at some point. I would be very interested to know how it turns out!

[Amelia Livingston]

I do ultimately need this for CommAlg R (not in mathlib but I have it in a file), yeah. I didn't use Mon_ to do this for Algebra R but I'll try using CommMon_ for commutative algebras and see if it's easier

[Eric Wieser]

I've made a start on this in #7598

[Eric Wieser]

The sorrys are all very boring, but they're also very slow and there is a lot of noise to clean up now sorry-free

[Eric Wieser]

I would guess now that we have docs#AlgebraCat.instMonoidalCategory, it's pretty easy to transfer that strategy to your CommAlg R via docs#CategoryTheory.Monoidal.induced

[Eric Wieser]

@Scott Morrison said:

The dream way to do it is to transport the monoidal structure over from the CommMon_ (Module R), and get lucky that the transported structure is actually usable. :-)

Presumably we should instead show there's an isomorphism between the two that preserves the monoidal structure?