mathlib documentation

category_theory.monoidal.internal.Module

Mon_ (Module R) ≌ Algebra R

The category of internal monoid objects in Module R is equivalent to the category of "native" bundled R-algebras.

Moreover, this equivalence is compatible with the forgetful functors to Module R.

@[simp]
theorem Module.Mon_Module_equivalence_Algebra.Mon_.X.ring_mul {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (x y : (A.X)) :
x * y = (A.mul) (x ⊗ₜ[R] y)

@[simp]
theorem Module.Mon_Module_equivalence_Algebra.Mon_.X.ring_one {R : Type u} [comm_ring R] (A : Mon_ (Module R)) :
1 = (A.one) 1

@[simp]
theorem Module.Mon_Module_equivalence_Algebra.Mon_.X.ring_add {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (ᾰ ᾰ_1 : (A.X)) :
+ ᾰ_1 = add_comm_group.add ᾰ_1

@[simp]
theorem Module.Mon_Module_equivalence_Algebra.Mon_.X.ring_neg {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (ᾰ : (A.X)) :

@[simp]
theorem Module.Mon_Module_equivalence_Algebra.Mon_.X.ring_sub {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (ᾰ ᾰ_1 : (A.X)) :
- ᾰ_1 = add_comm_group.sub ᾰ_1

@[simp]
theorem Module.Mon_Module_equivalence_Algebra.algebra_map {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (r : R) :
(algebra_map R (A.X)) r = (A.one) r

@[simp]

Converting a monoid object in Module R to a bundled algebra.

Equations

Converting a bundled algebra to a monoid object in Module R.

Equations

The category of internal monoid objects in Module R is equivalent to the category of "native" bundled R-algebras.

Equations

The equivalence Mon_ (Module R) ≌ Algebra R is naturally compatible with the forgetful functors to Module R.

Equations