Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-09-01 00:04 e053bdab

View on Github →

feat(category_theory/monoidal/internal): Mon_ (Module R) ≌ Algebra R (#3695) 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.

Estimated changes

Modified src/algebra/category/Module/monoidal.lean

deleted theorem Module.monoidal_category.associator_hom

added theorem Module.monoidal_category.associator_hom_apply

added theorem Module.monoidal_category.hom_apply

deleted theorem Module.monoidal_category.left_unitor_hom

added theorem Module.monoidal_category.left_unitor_hom_apply

deleted theorem Module.monoidal_category.right_unitor_hom

added theorem Module.monoidal_category.right_unitor_hom_apply

Modified src/algebra/module/basic.lean

added theorem linear_map.lcongr_fun

Created src/category_theory/monoidal/internal/Module.lean

added theorem Module.Mon_Module_equivalence_Algebra.algebra_map

added def Module.Mon_Module_equivalence_Algebra.functor

added def Module.Mon_Module_equivalence_Algebra.inverse

added def Module.Mon_Module_equivalence_Algebra.inverse_obj

added def Module.Mon_Module_equivalence_Algebra

added def Module.Mon_Module_equivalence_Algebra_forget

Modified src/category_theory/monoidal/types.lean

Modified src/ring_theory/algebra.lean

added theorem algebra.linear_map_apply

added def algebra.lmul'

added theorem algebra.lmul'_apply