[Merged by Bors] - feat: tensor products of coalgebras #11975
Conversation
…ty/mathlib4 into coalgtensorproduct
leanprover-community-mathlib4-bot
added
the
blocked-by-other-PR
|
|
||
| section | ||
|
|
||
| variable {R M N P Q : Type u} [CommRing R] |
There was a problem hiding this comment.
This is the big downside of doing everything via the categorical API; it forces universe monomorphism.
There was a problem hiding this comment.
(I note that https://github.com/ImperialCollegeLondon/FLT/blob/main/FLT/for_mathlib/Coalgebra/TensorProduct.lean contains a more direct approach without going via category theory, which preserves universe polymorphism)
There was a problem hiding this comment.
Yeah that is a shame but I'd been hoping it's not too much of an issue in practice. I like the idea of getting non-category-theory library API using category theory (but only in proofs so for the most part you can't tell)... and I thought this was worth the drawback of universe monomorphism. But I'm aware of the other formalisation. Do you think it's more suited to mathlib?
There was a problem hiding this comment.
I think the category-free version is more suited, yes. I'm glad to see you removed the "I'll close my PRs" section of your comment; the categorical API is still worth having, just not for the purpose of obtaining this instance.
There was a problem hiding this comment.
Okay. yeah I guess I could just close this one and remove the second half of #11974 (or actually just replace that PR with the equivalence CoalgebraCat R ≌ Comon_ (ModuleCat R)). And base the others on the category-free instance when it exists.
There was a problem hiding this comment.
After talking to Amelia, I am quite keen to merge this after the merge-conflict is resolved. We will, of course, when it is ready, provide the universe generalization enabled by doing this non-categorically, but this PR is blocking important work that Amelia is doing, and I don't want to block ongoing work for generalisations that aren't quite ready to merge.
There was a problem hiding this comment.
I am quite keen to merge this after the merge-conflict is resolved.
note there is still a dependent PR
There was a problem hiding this comment.
There is, sorry about this - if it's indeed ok to proceed with these 2 PRs I'm going to refactor the dependent PR to use CoalgebraCat R ≌ Comon_ (ModuleCat R). I'm at a workshop so didn't finish that yet, but I have a free afternoon today.
There was a problem hiding this comment.
Modulo CI I've hopefully finished refactoring this and #11974 to use comonoid objects instead of monoid objects. But fixing the second half of Mathlib.Algebra.Category.Coalgebra.ComonEquivalence gave me the impression the code is quite brittle. I'm sorry this situation is a bit of a mess - it could all have been avoided if I'd made a Zulip thread asking for advice about 2 months ago so I've learnt my lesson. If it ultimately doesn't get merged, or it gets merged and then gets entirely replaced, I won't be offended haha
leanprover-community-mathlib4-bot
added
the
merge-conflict
leanprover-community-bot-assistant
added
the
merge-conflict
leanprover-community-bot-assistant
removed
the
merge-conflict
|
bors d+ |
|
✌️ 101damnations can now approve this pull request. To approve and merge a pull request, simply reply with |
|
bors r+ |
Given two `R`-coalgebras `M, N`, we can define a natural comultiplication map `Δ : M ⊗[R] N → (M ⊗[R] N) ⊗[R] (M ⊗[R] N)` and counit map `ε : M ⊗[R] N → R` induced by the comultiplication and counit maps of `M` and `N`. These `Δ, ε` are declared as linear maps in `TensorProduct.instCoalgebraStruct` in `Mathlib.RingTheory.Coalgebra.Basic`. In this PR we show that `Δ, ε` satisfy the axioms of a coalgebra, and also define other data in the monoidal structure on `R`-coalgebras, like the tensor product of two coalgebra morphisms as a coalgebra morphism. Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Amelia Livingston <[email protected]>
|
Build failed (retrying...): |
Given two `R`-coalgebras `M, N`, we can define a natural comultiplication map `Δ : M ⊗[R] N → (M ⊗[R] N) ⊗[R] (M ⊗[R] N)` and counit map `ε : M ⊗[R] N → R` induced by the comultiplication and counit maps of `M` and `N`. These `Δ, ε` are declared as linear maps in `TensorProduct.instCoalgebraStruct` in `Mathlib.RingTheory.Coalgebra.Basic`. In this PR we show that `Δ, ε` satisfy the axioms of a coalgebra, and also define other data in the monoidal structure on `R`-coalgebras, like the tensor product of two coalgebra morphisms as a coalgebra morphism. Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Amelia Livingston <[email protected]>
|
Build failed: |
|
bors r+ |
Given two `R`-coalgebras `M, N`, we can define a natural comultiplication map `Δ : M ⊗[R] N → (M ⊗[R] N) ⊗[R] (M ⊗[R] N)` and counit map `ε : M ⊗[R] N → R` induced by the comultiplication and counit maps of `M` and `N`. These `Δ, ε` are declared as linear maps in `TensorProduct.instCoalgebraStruct` in `Mathlib.RingTheory.Coalgebra.Basic`. In this PR we show that `Δ, ε` satisfy the axioms of a coalgebra, and also define other data in the monoidal structure on `R`-coalgebras, like the tensor product of two coalgebra morphisms as a coalgebra morphism. Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Amelia Livingston <[email protected]>
|
Canceled. |
|
bors merge |
Given two `R`-coalgebras `M, N`, we can define a natural comultiplication map `Δ : M ⊗[R] N → (M ⊗[R] N) ⊗[R] (M ⊗[R] N)` and counit map `ε : M ⊗[R] N → R` induced by the comultiplication and counit maps of `M` and `N`. These `Δ, ε` are declared as linear maps in `TensorProduct.instCoalgebraStruct` in `Mathlib.RingTheory.Coalgebra.Basic`. In this PR we show that `Δ, ε` satisfy the axioms of a coalgebra, and also define other data in the monoidal structure on `R`-coalgebras, like the tensor product of two coalgebra morphisms as a coalgebra morphism. Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Amelia Livingston <[email protected]>
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Given two `R`-coalgebras `M, N`, we can define a natural comultiplication map `Δ : M ⊗[R] N → (M ⊗[R] N) ⊗[R] (M ⊗[R] N)` and counit map `ε : M ⊗[R] N → R` induced by the comultiplication and counit maps of `M` and `N`. These `Δ, ε` are declared as linear maps in `TensorProduct.instCoalgebraStruct` in `Mathlib.RingTheory.Coalgebra.Basic`. In this PR we show that `Δ, ε` satisfy the axioms of a coalgebra, and also define other data in the monoidal structure on `R`-coalgebras, like the tensor product of two coalgebra morphisms as a coalgebra morphism. Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Amelia Livingston <[email protected]>
Monoidal category structure on coalgebras, using the definitions in `Mathlib.RingTheory.Coalgebra.TensorProduct` added in #11975 Co-authored-by: Eric Wieser <[email protected]> Co-authored-by: Amelia Livingston <[email protected]>
Given two
R-coalgebrasM, N, we can define a natural comultiplication mapΔ : M ⊗[R] N → (M ⊗[R] N) ⊗[R] (M ⊗[R] N)and counit mapε : M ⊗[R] N → Rinduced by the comultiplication and counit maps ofMandN. TheseΔ, εare declared as linear maps inTensorProduct.instCoalgebraStructinMathlib.RingTheory.Coalgebra.Basic.In this PR we show that
Δ, εsatisfy the axioms of a coalgebra, and also define other data in the monoidal structure onR-coalgebras, like the tensor product of two coalgebra morphisms as a coalgebra morphism.We keep the linear maps underlying
Δ, εand other definitions in this PR syntactically equal to the corresponding definitions for tensor products of modules in the hope that this makes life easier. However, to fill in Prop fields, we use the API in #11974. That PR defines the monoidal category structure on coalgebras induced by an equivalence with comonoid objects in the category of modules,CoalgebraCat.instMonoidalCategoryAux, but we do not declare this as an instance - we just use it to prove things in this PR and #11976.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.