[Merged by Bors] - feat: category equivalence between coalgebras and comonoid objects #11974
Conversation
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
101damnations
changed the title
101damnations
added
awaiting-review
t-algebra
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-mathlib4-bot
removed
the
merge-conflict
| @@ -103,6 +103,12 @@ theorem braiding_inv_apply {M N : ModuleCat.{u} R} (m : M) (n : N) : | |||
| set_option linter.uppercaseLean3 false in | |||
| #align Module.monoidal_category.braiding_inv_apply ModuleCat.MonoidalCategory.braiding_inv_apply | |||
|
|
|||
| @[simp] | |||
There was a problem hiding this comment.
I'm not sure if this should be a simp lemma by default. Because the RHS is quite a long expr.
There was a problem hiding this comment.
With TensorProduct open, it's ↑(tensorTensorTensorComm R ↑A ↑B ↑C ↑D) : (↑A ⊗[R] ↑B) ⊗[R] ↑C ⊗[R] ↑D →ₗ[R] (↑A ⊗[R] ↑C) ⊗[R] ↑B ⊗[R] ↑D. I think that people like Eric like this kind of expression because ext fires very well on it. It looks simpler than the left hand side as well :-) However mathlib does build without the attribute so it's not being used yet...
There was a problem hiding this comment.
Thank you both for the reviews! I've removed the @[simp] on this lemma but added this
@[simp]
theorem tensor_μ_apply
{A B C D : ModuleCat R} (x : A) (y : B) (z : C) (w : D) :
tensor_μ _ (A, B) (C, D) ((x ⊗ₜ y) ⊗ₜ (z ⊗ₜ w)) = (x ⊗ₜ z) ⊗ₜ (y ⊗ₜ w) := rfl
as a simp lemma, more in line with other API for the monoidal structure on modules.
|
✌️ 101damnations can now approve this pull request. To approve and merge a pull request, simply reply with |
| @@ -101,7 +101,8 @@ def rightUnitor (M : ModuleCat.{u} R) : ModuleCat.of R (M ⊗[R] R) ≅ M := | |||
| (LinearEquiv.toModuleIso (TensorProduct.rid R M) : of R (M ⊗ R) ≅ of R M).trans (ofSelfIso M) | |||
| #align Module.monoidal_category.right_unitor ModuleCat.MonoidalCategory.rightUnitor | |||
|
|
|||
| instance : MonoidalCategoryStruct (ModuleCat.{u} R) where | |||
| @[simps (config := .lemmasOnly)] | |||
| instance instMonoidalCategoryStruct : MonoidalCategoryStruct (ModuleCat.{u} R) where | |||
There was a problem hiding this comment.
What's going on here, out of interest?
There was a problem hiding this comment.
It's like @[simps] except it doesn't tag the resulting lemmas with simp
| @@ -103,6 +103,12 @@ theorem braiding_inv_apply {M N : ModuleCat.{u} R} (m : M) (n : N) : | |||
| set_option linter.uppercaseLean3 false in | |||
| #align Module.monoidal_category.braiding_inv_apply ModuleCat.MonoidalCategory.braiding_inv_apply | |||
|
|
|||
| @[simp] | |||
There was a problem hiding this comment.
With TensorProduct open, it's ↑(tensorTensorTensorComm R ↑A ↑B ↑C ↑D) : (↑A ⊗[R] ↑B) ⊗[R] ↑C ⊗[R] ↑D →ₗ[R] (↑A ⊗[R] ↑C) ⊗[R] ↑B ⊗[R] ↑D. I think that people like Eric like this kind of expression because ext fires very well on it. It looks simpler than the left hand side as well :-) However mathlib does build without the attribute so it's not being used yet...
PR summary 715478e721
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.RingTheory.Coalgebra.Basic | 770 | 772 | +2 (+0.26%) |
Import changes for all files
| Files | Import difference |
|---|---|
4 filesMathlib.RingTheory.Coalgebra.Basic Mathlib.RingTheory.Coalgebra.Hom Mathlib.Algebra.Category.CoalgebraCat.Basic Mathlib.RingTheory.Coalgebra.Equiv |
2 |
Mathlib.Algebra.Category.CoalgebraCat.ComonEquivalence |
913 |
Declarations diff
+ associator_hom_toLinearMap
+ comonEquivalence
+ comul_tensorObj
+ comul_tensorObj_tensorObj_left
+ comul_tensorObj_tensorObj_right
+ counit_tensorObj
+ counit_tensorObj_tensorObj_left
+ counit_tensorObj_tensorObj_right
+ instCoalgebraStruct
+ instMonoidalCategoryAux
+ instMonoidalCategoryStruct
+ leftUnitor_hom_toLinearMap
+ ofComon
+ ofComonObj
+ ofComonObjCoalgebraStruct
+ op_tensor_μ
+ rightUnitor_hom_toLinearMap
+ tensorHom_toLinearMap
+ tensorObj_comul
+ tensor_μ_apply
+ tensor_μ_eq_tensorTensorTensorComm
+ toComon
+ toComonObj
+ unop_tensor_μ
+ we
- instance : MonoidalCategoryStruct (ModuleCat.{u} R)
You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>
|
bors r+ |
…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. Co-authored-by: Eric Wieser <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Given a commutative ring
R, this PR defines the equivalence of categories betweenR-coalgebras and comonoid objects in the category ofR-modules. We then use this to set up boilerplate for the monoidal structure onR-coalgebras defined in #11975 and #11976.Possibly everything after the equivalence of categories should be in a separate PR, but here's its explanation.
We make the definition
CoalgebraCat.instMonoidalCategoryAuxin this PR, which is the monoidal structure onCoalgebraCatinduced by the equivalence withComon(R-Mod), and we prove lemmas about this declaration which are essentially true by definition. But our actual 1.Coalgebrainstance on a tensor product of coalgebras and 2.MonoidalCategoryinstance onCoalgebraCatare constructed in #11975 and #11976 respectively. We construct the instances to have simple data - i.e. the underlying linear maps are more obviously stuff fromLinearAlgebra.TensorProduct.Basic. But to fill in the Prop fields in those PRs, we useCoalgebraCat.instMonoidalCategoryAuxand the API in the second half of this PR.I really don't know how necessary this roundabout approach is; I was just pleased to have got it working. The idea was to use category theory to get non-category theory API for free-ish, without performance issues or the category theory leaking through.