feat(CategoryTheory): Distributive Categories #20182
Conversation
|
messageFile.md |
joelriou
added
the
awaiting-author
sinhp
removed
the
awaiting-author
remove #[Mathlib.CategoryTheory.Monoidal.OfHasFiniteProducts]
joelriou
changed the title
Co-authored-by: Joël Riou <[email protected]>
|
|
||
| /-- The evaluation of a binary product of functors at an object is isomorphic to | ||
| the product of the evaluations at that object. -/ | ||
| noncomputable def prodObjIso (X Y : K ⥤ C) (k : K) : (X ⨯ Y).obj k ≅ (X.obj k) ⨯ (Y.obj k) := |
There was a problem hiding this comment.
Do you use the definitions in this file somewhere else in this PR? If not, could you remove it from this PR?
There was a problem hiding this comment.
This file does not seem to be needed anymore. I just removed the whole file which is about binary product and coproduction in the functor category.
joelriou
added
the
awaiting-author
sinhp
removed
the
awaiting-author
| ## References | ||
| - [J.R.B.Cockett, Introduction to distributive categories, 1992][] |
There was a problem hiding this comment.
Could you add this to docs/references.bib?
joelriou
added
the
awaiting-author
sinhp
removed
the
awaiting-author
…eorder category of a meet-semilattice with a top element (#21094) The preorder category of a meet-semilattice `C` with a top element has chosen finite products. Motivation: I plan to use the induced monoidal structure to show that the preorder category of a distributive lattice is distributive. See this PR on Monoidal and cartesian distributive categories: #20182
Co-authored-by: Joël Riou <[email protected]>
| abbrev CartesianDistributive := | ||
| IsMonoidalLeftDistrib C |
There was a problem hiding this comment.
I think this should be defined as IsMonoidalDistrib, and the next instance should be a lemma.
There was a problem hiding this comment.
The idea is if a user wants to prove something is CartesianDistributive they only need to supply the left distrib data
preservesBinaryCoproducts_tensorLeft, and the right should be filled in by default since we are in symmetric situation. In above, we decided to make the following instance into a lemma, so I don't think right distrib is inferred from left by default for CartesianDistributive.
SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib
So, I implemented your suggestion together the following mk definition:
def mkOfIsMonoidalLeftDistrib [IsMonoidalLeftDistrib C] : CartesianDistributive C :=
SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib
Let me know if you had some other idea.
| IsMonoidalRightDistrib C where | ||
| preservesBinaryCoproducts_tensorRight X := by | ||
| refine { | ||
| preservesColimit := by |
There was a problem hiding this comment.
Is not it possible to use preservesBinaryCoproducts_of_isIso_coprodComparison?
There was a problem hiding this comment.
good catch, it became 8 lines shorter!
feat: Monoidal and cartesian distributive categories
This PR defines monoidal and cartesian distributive categories, develop the API, and prove some main results. We show a closed monoidal category is distributive.
We also show that, for a category
Cwith binary coproducts, the category of endofunctorsC ⥤ Cis left distributive. This requires the following new file which develops a convenient API for the binary (co)products in the functor categories:CategoryTheory/Limits/FunctorCategory/Shapes/BinaryProducts
In Mathlib/CategoryTheory/Distributive/Cartesian.lean we show that the coproduct coprojections are monic in a cartesian distributive category.