mathlib docs: category_theory.monoidal.internal.Module

source

@[simp]

theorem Module.Mon_Module_equivalence_Algebra.ring_one {R : Type u} [comm_ring R] (A : Mon_ (Module R)) :

1 = ⇑(A.one) 1

source

@[simp]

theorem Module.Mon_Module_equivalence_Algebra.ring_zero {R : Type u} [comm_ring R] (A : Mon_ (Module R)) :

0 = add_comm_group.zero

source

@[simp]

theorem Module.Mon_Module_equivalence_Algebra.ring_mul {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (x y : ↥(A.X)) :

x * y = ⇑(A.mul) (x ⊗ₜ[R] y)

source

@[instance]

def Module.Mon_Module_equivalence_Algebra.ring {R : Type u} [comm_ring R] (A : Mon_ (Module R)) :

ring ↥(A.X)

Equations

Module.Mon_Module_equivalence_Algebra.ring A = {add := add_comm_group.add A.X.is_add_comm_group, add_assoc := _, zero := add_comm_group.zero A.X.is_add_comm_group, zero_add := _, add_zero := _, neg := add_comm_group.neg A.X.is_add_comm_group, add_left_neg := _, add_comm := _, mul := λ (x y : ↥(A.X)), ⇑(A.mul) (x ⊗ₜ[R] y), mul_assoc := _, one := ⇑(A.one) 1, one_mul := _, mul_one := _, left_distrib := _, right_distrib := _}

source

@[simp]

theorem Module.Mon_Module_equivalence_Algebra.ring_neg {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (a : ↥(A.X)) :

-a = add_comm_group.neg a

source

@[simp]

theorem Module.Mon_Module_equivalence_Algebra.ring_add {R : Type u} [comm_ring R] (A : Mon_ (Module R)) (a a_1 : ↥(A.X)) :

a + a_1 = add_comm_group.add a a_1

source

@[instance]

def Module.Mon_Module_equivalence_Algebra.algebra {R : Type u} [comm_ring R] (A : Mon_ (Module R)) :

algebra R ↥(A.X)

Equations

Module.Mon_Module_equivalence_Algebra.algebra A = {to_has_scalar := mul_action.to_has_scalar distrib_mul_action.to_mul_action, to_ring_hom := {to_fun := A.one.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}

source

@[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

source

@[simp]

theorem Module.Mon_Module_equivalence_Algebra.functor_map_to_fun {R : Type u} [comm_ring R] (A B : Mon_ (Module R)) (f : A ⟶ B) (a : ↥(A.X)) :

⇑(Module.Mon_Module_equivalence_Algebra.functor.map f) a = ⇑(f.hom) a

source

def Module.Mon_Module_equivalence_Algebra.functor {R : Type u} [comm_ring R] :

Mon_ (Module R) ⥤ Algebra R

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

Equations

Module.Mon_Module_equivalence_Algebra.functor = {obj := λ (A : Mon_ (Module R)), Algebra.of R ↥(A.X), map := λ (A B : Mon_ (Module R)) (f : A ⟶ B), {to_fun := ⇑(f.hom), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}, map_id' := _, map_comp' := _}

source

@[simp]

theorem Module.Mon_Module_equivalence_Algebra.functor_obj {R : Type u} [comm_ring R] (A : Mon_ (Module R)) :

Module.Mon_Module_equivalence_Algebra.functor.obj A = Algebra.of R ↥(A.X)

source

def Module.Mon_Module_equivalence_Algebra.inverse_obj {R : Type u} [comm_ring R] (A : Algebra R) :

Mon_ (Module R)

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

Equations

Module.Mon_Module_equivalence_Algebra.inverse_obj A = {X := Module.of R ↥A algebra.to_semimodule, one := algebra.linear_map R ↥A A.is_algebra, mul := algebra.lmul' R ↥A A.is_algebra, one_mul' := _, mul_one' := _, mul_assoc' := _}

source

@[simp]

theorem Module.Mon_Module_equivalence_Algebra.inverse_obj_mul {R : Type u} [comm_ring R] (A : Algebra R) :

(Module.Mon_Module_equivalence_Algebra.inverse_obj A).mul = algebra.lmul' R ↥A

source

@[simp]

theorem Module.Mon_Module_equivalence_Algebra.inverse_obj_one {R : Type u} [comm_ring R] (A : Algebra R) :

(Module.Mon_Module_equivalence_Algebra.inverse_obj A).one = algebra.linear_map R ↥A

source

@[simp]

theorem Module.Mon_Module_equivalence_Algebra.inverse_obj_X {R : Type u} [comm_ring R] (A : Algebra R) :

(Module.Mon_Module_equivalence_Algebra.inverse_obj A).X = Module.of R ↥A

source

@[simp]

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

(Module.Mon_Module_equivalence_Algebra.inverse.map f).hom = alg_hom.to_linear_map f

source

def Module.Mon_Module_equivalence_Algebra.inverse {R : Type u} [comm_ring R] :

Algebra R ⥤ Mon_ (Module R)

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

Equations

Module.Mon_Module_equivalence_Algebra.inverse = {obj := Module.Mon_Module_equivalence_Algebra.inverse_obj _inst_1, map := λ (A B : Algebra R) (f : A ⟶ B), {hom := alg_hom.to_linear_map f, one_hom' := _, mul_hom' := _}, map_id' := _, map_comp' := _}

source

@[simp]

theorem Module.Mon_Module_equivalence_Algebra.inverse_obj_2 {R : Type u} [comm_ring R] (A : Algebra R) :

Module.Mon_Module_equivalence_Algebra.inverse.obj A = Module.Mon_Module_equivalence_Algebra.inverse_obj A

source

def Module.Mon_Module_equivalence_Algebra {R : Type u} [comm_ring R] :

Mon_ (Module R) ≌ Algebra R

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

Equations

Module.Mon_Module_equivalence_Algebra = {functor := Module.Mon_Module_equivalence_Algebra.functor _inst_1, inverse := Module.Mon_Module_equivalence_Algebra.inverse _inst_1, unit_iso := category_theory.nat_iso.of_components (λ (A : Mon_ (Module R)), {hom := {hom := {to_fun := id ↥(((𝟭 (Mon_ (Module R))).obj A).X), map_add' := _, map_smul' := _}, one_hom' := _, mul_hom' := _}, inv := {hom := {to_fun := id ↥(((Module.Mon_Module_equivalence_Algebra.functor ⋙ Module.Mon_Module_equivalence_Algebra.inverse).obj A).X), map_add' := _, map_smul' := _}, one_hom' := _, mul_hom' := _}, hom_inv_id' := _, inv_hom_id' := _}) Module.Mon_Module_equivalence_Algebra._proof_11, counit_iso := category_theory.nat_iso.of_components (λ (A : Algebra R), {hom := {to_fun := id ↥((Module.Mon_Module_equivalence_Algebra.inverse ⋙ Module.Mon_Module_equivalence_Algebra.functor).obj A), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}, inv := {to_fun := id ↥((𝟭 (Algebra R)).obj A), map_one' := _, map_mul' := _, map_zero' := _, map_add' := _, commutes' := _}, hom_inv_id' := _, inv_hom_id' := _}) Module.Mon_Module_equivalence_Algebra._proof_24, functor_unit_iso_comp' := _}

source

def Module.Mon_Module_equivalence_Algebra_forget {R : Type u} [comm_ring R] :

Module.Mon_Module_equivalence_Algebra.functor ⋙ category_theory.forget₂ (Algebra R) (Module R) ≅ Mon_.forget (Module R)

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

Equations

Module.Mon_Module_equivalence_Algebra_forget = category_theory.nat_iso.of_components (λ (A : Mon_ (Module R)), {hom := {to_fun := id ↥((Module.Mon_Module_equivalence_Algebra.functor ⋙ category_theory.forget₂ (Algebra R) (Module R)).obj A), map_add' := _, map_smul' := _}, inv := {to_fun := id ↥((Mon_.forget (Module R)).obj A), map_add' := _, map_smul' := _}, hom_inv_id' := _, inv_hom_id' := _}) Module.Mon_Module_equivalence_Algebra_forget._proof_7

mathlib documentation

`Mon_ (Module R) ≌ Algebra R`