Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-03-14 08:02 81d3ebf3

View on Github →

feat(algebra): monoidal category of R-modules (#2125)

feat(algebra): monoidal category of R-modules
docstrings
minor
tweaks
fix import
fixes
reduce use of @
broken
fixes
Update src/algebra/category/Module/basic.lean Co-Authored-By: Bryan Gin-ge Chen bryangingechen@gmail.com

Estimated changes

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

modified def Module.kernel_is_limit

added def Module.of_self

added def category_theory.iso.to_linear_equiv

added def linear_equiv.to_Module_iso

added def linear_equiv_iso_Group_iso

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

added def Module.monoidal_category.associator

added theorem Module.monoidal_category.associator_naturality

added def Module.monoidal_category.left_unitor

added theorem Module.monoidal_category.left_unitor_naturality

added theorem Module.monoidal_category.pentagon

added def Module.monoidal_category.right_unitor

added theorem Module.monoidal_category.right_unitor_naturality

added theorem Module.monoidal_category.tensor_comp

added def Module.monoidal_category.tensor_hom

added theorem Module.monoidal_category.tensor_id

added def Module.monoidal_category.tensor_obj

added theorem Module.monoidal_category.triangle

Modified src/category_theory/limits/types.lean

deleted def category_theory.limits.types.colimit

added def category_theory.limits.types.colimit_

deleted def category_theory.limits.types.colimit_is_colimit

added def category_theory.limits.types.colimit_is_colimit_

deleted def category_theory.limits.types.limit

added def category_theory.limits.types.limit_

deleted def category_theory.limits.types.limit_is_limit

added def category_theory.limits.types.limit_is_limit_

modified theorem category_theory.limits.types.types_limit_map

modified theorem category_theory.limits.types.types_limit_π

Modified src/linear_algebra/basic.lean

modified def linear_equiv.refl

modified def linear_equiv.symm

modified def linear_equiv.trans

added theorem linear_equiv.trans_apply

Modified src/linear_algebra/tensor_product.lean

added theorem tensor_product.assoc_tmul

added theorem tensor_product.ext_fourfold

added theorem tensor_product.ext_threefold

added theorem tensor_product.lid_tmul

added theorem tensor_product.rid_tmul