[Merged by Bors] - feat (CategoryTheory): constructing chosen finite products for the preorder category of a meet-semilattice with a top element #21094

sinhp · 2025-01-26T15:12:06Z

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

github-actions · 2025-01-26T15:13:04Z

PR summary 4f13c899e4

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic	408	413	+5 (+1.23%)

Import changes for all files

Files	Import difference
`Mathlib.CategoryTheory.Limits.Shapes.Preorder.Basic`	5
`Mathlib.CategoryTheory.Limits.Preorder` (new file)	412
`Mathlib.CategoryTheory.ChosenFiniteProducts.InfSemilattice` (new file)	578

Declarations diff

+ instance : HasInitial C := hasInitial_of_unique ⊥
+ instance : HasTerminal C := hasTerminal_of_unique ⊤
+ isColimitBinaryCofan
+ isLimitBinaryFan
+ isTerminalTop
+ tensorObj
+ tensorUnit
- instance : HasInitial J := hasInitial_of_unique ⊥
- instance : HasTerminal J := hasTerminal_of_unique ⊤
- isTerminalBot

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

joelriou · 2025-01-26T19:00:48Z

Mathlib/CategoryTheory/ChosenFiniteProducts/InfSemilattice.lean

+end
+
+/-- Chosen finite products for the preorder category of a meet-semilattice with a greatest element-/
+noncomputable instance : ChosenFiniteProducts C where


I am not sure we should make this an instance. It may be safer to make it a local or scoped instance.

made it scoped in the namespace CategoryTheory.SemilatticeInf.

joelriou · 2025-01-26T19:06:31Z

Mathlib/CategoryTheory/ChosenFiniteProducts/InfSemilattice.lean

+abbrev chosenTerminal : C := ⊤
+
+/-- The chosen terminal object in the preoder category of `C` is terminal. -/
+def chosenTerminalIsTerminal : IsTerminal (chosenTerminal C) where


This already appears in the file CategoryTheory.Limits.Shapes.Preorder.Basic since #20335.
I would suggest you create a new file/directory CategoryTheory.Limits.Preorder where you would put results about colimits in a preordered type. There, you could move my definitions isInitialBot, isTerminalTop, HasInitial, HasTerminal (and keep the rest in Shapes.Preorder.Basic which is about the existence of (co)limits indexed by a preordered type).
In CategoryTheory.Limits.Preorder, you could add results about max, min (and more...) as definitions saying that certain (co)cones are (co)limits.
Then, in CategoryTheory.ChosenFiniteProducts.SemiLatticeInf, you could define chosen finite products out of these definitions.

sounds like a good idea! just did that.

joelriou · 2025-01-26T19:16:47Z

Mathlib/CategoryTheory/ChosenFiniteProducts/InfSemilattice.lean

+def isLimit : IsLimit (BinaryFan.mk (fst X Y) (snd X Y)) where
+  lift s := homOfLE <| le_inf (leOfHom <| s.π.app <|
+  ⟨WalkingPair.left⟩) (leOfHom <| s.π.app <| ⟨WalkingPair.right⟩)


I do not think we need the separate definitions chosenProd, fst and snd:

def isLimitBinaryFan : IsLimit (BinaryFan.mk (P := X ⊓ Y) (homOfLE inf_le_left) (homOfLE inf_le_right)) := BinaryFan.isLimitMk (fun s ↦ homOfLE (le_inf (leOfHom s.fst) (leOfHom s.snd))) (by intros; rfl) (by intros; rfl) (by intros; rfl)

I also removed chosenTerminal, etc and imported stuff from Limits.Preorder. All that is left is

noncomputable scoped instance chosenFiniteProducts : ChosenFiniteProducts C where terminal := ⟨_, Preorder.isTerminalTop C⟩ product X Y := ⟨_, Preorder.isLimitBinaryFan X Y⟩

Mathlib/CategoryTheory/Limits/Preorder.lean

Co-authored-by: Joël Riou <[email protected]>

Mathlib/CategoryTheory/Limits/Preorder.lean

joelriou · 2025-01-28T15:01:08Z

Mathlib/CategoryTheory/ChosenFiniteProducts/InfSemilattice.lean

+lemma tensorObj {C : Type u} [Lattice C] [OrderTop C] {X Y : C} : X ⊗ Y = X ⊓ Y := rfl
+
+lemma tensorUnit {C : Type u} [Lattice C] [OrderTop C] :


Do not you want to assume SemilatticeInf instead of Lattice?

🤦 indeed, thanks for spotting that! just fixed it!

Incidentally, it seems we do not have ChosenFiniteCoProducts in Mathlib, and I was wondering why that is? would it be worth it to add it and then prove join-semilattices have a monoidal structure. This is not directly relevant to the project about distributive categories, but maybe in a separate branch/PR it can be done if you think it'd be useful. If at some point in future one wants to define rig-categories (i.e. distributive bimonoidal) then we need both conoidal structures coming from meet and join to show that distributive lattices are example of rig-categories.

At this stage, I do not think it is necessary to develop ChosenFiniteCoproducts.

joelriou · 2025-01-28T15:06:40Z

Mathlib/CategoryTheory/ChosenFiniteProducts/InfSemilattice.lean

+/-- A monoidal structure on the preorder category of a meet-semilattice with a greatest element
+is provided by the instance `monoidalOfChosenFiniteProducts`. -/
+noncomputable scoped instance monoidalCategory : MonoidalCategory C := by
+  infer_instance
+
+/-- The symmetric monoidal structure on the preorder category of a
+meet-semilattice with a greatest element. -/
+noncomputable scoped instance symmetricCategory : SymmetricCategory C := by
+  infer_instance
+


There is no need to declare these as they can already be infered automatically. You may add a comment in docstring of the file saying C is automatically endowed with a symmetric category structure.

sounds good. added a sentence in the preamble doc-string.

joelriou · 2025-01-28T15:07:09Z

Mathlib/CategoryTheory/ChosenFiniteProducts/InfSemilattice.lean

+namespace Monoidal
+


Suggested change

namespace Monoidal

I am not sure we need to put the two lemmas in a subnamespace.

Co-authored-by: Joël Riou <[email protected]>

joelriou · 2025-01-28T22:06:57Z

Thanks!

bors merge

…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

mathlib-bors · 2025-01-28T22:32:59Z

Pull request successfully merged into master.

Build succeeded:

Create InfSemilattice.lean

c821072

github-actions bot added the t-category-theory Category theory label Jan 26, 2025

lake exe mk_all

c8d8ecd

sinhp added the good first issue Good for newcomers label Jan 26, 2025

add doc strings

256e91d

joelriou reviewed Jan 26, 2025

View reviewed changes

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 26, 2025

sinhp added 6 commits January 27, 2025 15:42

make instance scoped

f3e6114

CategoryTheory.SemilatticeInf.chosenFiniteProducts

30da0b6

refactoring into Limits.Preorder

9d2467b

more clear doc string

6d9636c

lake exe mk_all

c1d2bcf

doc string addition

b6ef16e

sinhp removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 27, 2025

joelriou reviewed Jan 28, 2025

View reviewed changes

Mathlib/CategoryTheory/Limits/Preorder.lean Outdated Show resolved Hide resolved

joelriou reviewed Jan 28, 2025

View reviewed changes

Mathlib/CategoryTheory/Limits/Preorder.lean Outdated Show resolved Hide resolved

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 28, 2025

sinhp and others added 2 commits January 28, 2025 15:13

Update Mathlib/CategoryTheory/Limits/Preorder.lean

460a4bb

Co-authored-by: Joël Riou <[email protected]>

Update Mathlib/CategoryTheory/Limits/Preorder.lean

adc4997

Co-authored-by: Joël Riou <[email protected]>

sinhp removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 28, 2025

joelriou reviewed Jan 28, 2025

View reviewed changes

Mathlib/CategoryTheory/Limits/Preorder.lean Outdated Show resolved Hide resolved

joelriou reviewed Jan 28, 2025

View reviewed changes

Mathlib/CategoryTheory/Limits/Preorder.lean Outdated Show resolved Hide resolved

joelriou reviewed Jan 28, 2025

View reviewed changes

joelriou added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 28, 2025

weaker assumption

32813e7

sinhp added 2 commits January 28, 2025 16:17

pruning

2035e61

more pruning

a762174

sinhp removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 28, 2025

sinhp and others added 2 commits January 28, 2025 16:55

Update Mathlib/CategoryTheory/Limits/Preorder.lean

25553d8

Co-authored-by: Joël Riou <[email protected]>

Update Mathlib/CategoryTheory/Limits/Preorder.lean

4f13c89

Co-authored-by: Joël Riou <[email protected]>

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jan 28, 2025

mathlib-bors bot closed this Jan 28, 2025

mathlib-bors bot deleted the sina-chosen_finite_products_for_meet_semilattices branch January 28, 2025 22:33

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat (CategoryTheory): constructing chosen finite products for the preorder category of a meet-semilattice with a top element #21094

[Merged by Bors] - feat (CategoryTheory): constructing chosen finite products for the preorder category of a meet-semilattice with a top element #21094

sinhp commented Jan 26, 2025 •

edited

Loading

github-actions bot commented Jan 26, 2025 •

edited

Loading

Import changes for modified files

Declarations diff

joelriou Jan 26, 2025

sinhp Jan 27, 2025

joelriou Jan 26, 2025

sinhp Jan 27, 2025

joelriou Jan 26, 2025

sinhp Jan 27, 2025

joelriou Jan 28, 2025

sinhp Jan 28, 2025

joelriou Jan 28, 2025

joelriou Jan 28, 2025

sinhp Jan 28, 2025

joelriou Jan 28, 2025

joelriou commented Jan 28, 2025

mathlib-bors bot commented Jan 28, 2025

		lemma tensorObj {C : Type u} [Lattice C] [OrderTop C] {X Y : C} : X ⊗ Y = X ⊓ Y := rfl

		lemma tensorUnit {C : Type u} [Lattice C] [OrderTop C] :

[Merged by Bors] - feat (CategoryTheory): constructing chosen finite products for the preorder category of a meet-semilattice with a top element #21094

[Merged by Bors] - feat (CategoryTheory): constructing chosen finite products for the preorder category of a meet-semilattice with a top element #21094

Conversation

sinhp commented Jan 26, 2025 • edited Loading

github-actions bot commented Jan 26, 2025 • edited Loading

PR summary 4f13c899e4

Import changes for modified files

Declarations diff

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

joelriou commented Jan 28, 2025

mathlib-bors bot commented Jan 28, 2025

sinhp commented Jan 26, 2025 •

edited

Loading

github-actions bot commented Jan 26, 2025 •

edited

Loading