# mathlibdocumentation

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_npow {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (ᾰ : ) (ᾰ_1 : (A.X)) :
ᾰ_1 = monoid.npow._default ((A.one) 1) (λ (x y : (A.X)), (A.mul) (x ⊗ₜ[R] y)) _ _ ᾰ_1
@[simp]
theorem Module.Mon_Module_equivalence_Algebra.Mon_.X.ring_nsmul {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (ᾰ : ) (ᾰ_1 : (A.X)) :
ᾰ_1 = ᾰ_1
@[simp]
theorem Module.Mon_Module_equivalence_Algebra.Mon_.X.ring_zsmul {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (ᾰ : ) (ᾰ_1 : (A.X)) :
ᾰ_1 = ᾰ_1
@[simp]
theorem Module.Mon_Module_equivalence_Algebra.Mon_.X.ring_int_cast {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (ᾰ : ) :
@[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 = ᾰ_1
@[protected, instance]
Equations
@[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_nat_cast {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (ᾰ : ) :
@[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 = ᾰ_1
@[protected, instance]
Equations
@[simp]
theorem Module.Mon_Module_equivalence_Algebra.algebra_map {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (r : R) :
(A.X)) r = (A.one) r
@[simp]
theorem Module.Mon_Module_equivalence_Algebra.functor_map_apply {R : Type u} [comm_ring R] (A B : Mon_ (Module R)) (f : A B) (ᾰ : (A.X)) :

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

Equations
@[simp]

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

Equations
@[simp]
@[simp]
theorem Module.Mon_Module_equivalence_Algebra.inverse_map_hom {R : Type u} [comm_ring R] (A B : Algebra R) (f : A B) :

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

Equations
@[simp]

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