Theorems · Definition · category theory

ModuleCat.MonModuleEquivalenceAlgebra.Algebra_of_Mon_

{R : Type u} → [inst : CommRing R] → (A : ModuleCat R) → [inst_1 : CategoryTheory.MonObj A] → Algebra R ↑A

The algebra structure on a monoid object. This instance is dangerous as it doesn't round trip from a ring to a monoid object and then back to a ring, since the npow field is lost in the middle. Therefore, it is scoped.

Defined in

Mathlib.CategoryTheory.Monoidal.Internal.Module

Cited by

2 results in Mathlib

Foundations

Depth 81 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingCategoryTheory.MonObj