Commit 2024-07-16 19:50 9ed238fc

View on Github →

feat: category equivalence between coalgebras and comonoid objects (#11974) Given a commutative ring R, this PR defines the equivalence of categories between R-coalgebras and comonoid objects in the category of R-modules. We then use this to set up boilerplate for the monoidal structure on R-coalgebras defined in #11975 and #11976.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/CoalgebraCat/ComonEquivalence.lean

added theorem CoalgebraCat.MonoidalCategoryAux.associator_hom_toLinearMap

added theorem CoalgebraCat.MonoidalCategoryAux.comul_tensorObj

added theorem CoalgebraCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_left

added theorem CoalgebraCat.MonoidalCategoryAux.comul_tensorObj_tensorObj_right

added theorem CoalgebraCat.MonoidalCategoryAux.counit_tensorObj

added theorem CoalgebraCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_left

added theorem CoalgebraCat.MonoidalCategoryAux.counit_tensorObj_tensorObj_right

added theorem CoalgebraCat.MonoidalCategoryAux.leftUnitor_hom_toLinearMap

added theorem CoalgebraCat.MonoidalCategoryAux.rightUnitor_hom_toLinearMap

added theorem CoalgebraCat.MonoidalCategoryAux.tensorHom_toLinearMap

added theorem CoalgebraCat.MonoidalCategoryAux.tensorObj_comul

added def CoalgebraCat.ofComon

added def CoalgebraCat.ofComonObj

added def CoalgebraCat.toComon

added def CoalgebraCat.toComonObj

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Symmetric.lean

added theorem ModuleCat.MonoidalCategory.tensor_μ_apply

added theorem ModuleCat.MonoidalCategory.tensor_μ_eq_tensorTensorTensorComm

Modified Mathlib/CategoryTheory/Monoidal/Braided/Opposite.lean

added theorem CategoryTheory.BraidedCategory.op_tensor_μ

added theorem CategoryTheory.BraidedCategory.unop_tensor_μ

Modified Mathlib/RingTheory/Coalgebra/Basic.lean