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_npow {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (ᾰ : ) (ᾰ_1 : (A.X)) :
ring.npow ᾰ_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)) :
ring.nsmul ᾰ_1 = add_comm_group.nsmul ᾰ_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)) :
ring.zsmul ᾰ_1 = add_comm_group.zsmul ᾰ_1
@[simp]
theorem Module.Mon_Module_equivalence_Algebra.Mon_.X.ring_int_cast {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (ᾰ : ) :
ring.int_cast = add_comm_group_with_one.int_cast._default (add_comm_group_with_one.nat_cast._default ((A.one) 1) add_comm_group.add _ add_comm_group.zero _ _ add_comm_group.nsmul _ _) add_comm_group.add _ add_comm_group.zero _ _ add_comm_group.nsmul _ _ ((A.one) 1) _ _ add_comm_group.neg add_comm_group.sub _ add_comm_group.zsmul _ _ _ _
@[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
@[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)) (ᾰ : ) :
ring.nat_cast = add_comm_group_with_one.nat_cast._default ((A.one) 1) add_comm_group.add _ add_comm_group.zero _ _ add_comm_group.nsmul _ _
@[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

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