Mon_ (Module R) ≌ Algebra R #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_zero
{R : Type u}
[comm_ring R]
(A : Mon_ (Module R)) :
@[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 _ _ _ _ ᾰ
@[protected, instance]
def
Module.Mon_Module_equivalence_Algebra.Mon_.X.ring
{R : Type u}
[comm_ring R]
(A : Mon_ (Module R)) :
Equations
- Module.Mon_Module_equivalence_Algebra.Mon_.X.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 := _, nsmul := add_comm_group.nsmul A.X.is_add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg A.X.is_add_comm_group, sub := add_comm_group.sub A.X.is_add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul A.X.is_add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, 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 _ _ _ _, 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 _ _, one := ⇑(A.one) 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := λ (x y : ↥(A.X)), ⇑(A.mul) (x ⊗ₜ[R] y), mul_assoc := _, one_mul := _, mul_one := _, npow := monoid.npow._default (⇑(A.one) 1) (λ (x y : ↥(A.X)), ⇑(A.mul) (x ⊗ₜ[R] y)) _ _, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[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 _ _ ᾰ
@[protected, instance]
def
Module.Mon_Module_equivalence_Algebra.Mon_.X.algebra
{R : Type u}
[comm_ring R]
(A : Mon_ (Module R)) :
Equations
- Module.Mon_Module_equivalence_Algebra.Mon_.X.algebra A = {to_has_smul := smul_zero_class.to_has_smul smul_with_zero.to_smul_zero_class, to_ring_hom := {to_fun := A.one.to_fun, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
Converting a monoid object in Module R to a bundled algebra.
@[simp]
theorem
Module.Mon_Module_equivalence_Algebra.functor_obj
{R : Type u}
[comm_ring R]
(A : 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_module, one := algebra.linear_map R ↥A A.is_algebra, mul := linear_map.mul' R ↥A _, one_mul' := _, mul_one' := _, mul_assoc' := _}
@[simp]
theorem
Module.Mon_Module_equivalence_Algebra.inverse_obj_mul
{R : Type u}
[comm_ring R]
(A : Algebra R) :
@[simp]
theorem
Module.Mon_Module_equivalence_Algebra.inverse_obj_one
{R : Type u}
[comm_ring R]
(A : Algebra R) :
@[simp]
theorem
Module.Mon_Module_equivalence_Algebra.inverse_obj_X
{R : Type u}
[comm_ring R]
(A : Algebra R) :
@[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
- 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' := _}
@[simp]
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' := _}
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