feat(Data/Set): representing the equivalence classes of a Quot by pimotte · Pull Request #21097 · leanprover-community/mathlib4

pimotte · 2025-01-26T17:28:50Z

Adds the SetLike instance for Quot along with the notion of Represents, which says that a Set represents a set of equivalence classes if it contains exactly one element of each class.

This is the more generic version of #20024

github-actions · 2025-01-26T17:29:43Z

PR summary 19daea86d0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
`Mathlib.Data.Set.Quot` (new file)	687

Declarations diff

+ Quot.ext
+ Quot.mem_coe
+ Represents
+ exact
+ instance : SetLike (Quot r) α
+ ncard_inter
+ ncard_sdiff_of_mem
+ ncard_sdiff_of_not_mem
+ out_image_represents
+ unique_rep

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).

EtienneC30

Thank you for this! I left some suggestions for shortening / readability / mathlib-friendly.

Mathlib/Data/Set/Quot.lean

Co-authored-by: Etienne <66847262+EtienneC30@users.noreply.github.com>

pimotte · 2025-01-28T06:48:12Z

Adopted all suggestions by @EtienneC30, thanks!

Mathlib/Data/Set/Quot.lean

EtienneC30

We're almost there!

Mathlib/Data/Set/Quot.lean

EtienneC30 · 2025-01-30T07:19:07Z

One last comment: after defining the structure, you use the variables {C : Set (Quot r)} {s : Set α} {c : Quot r} in nearly all lemmas. If you want you can introduce them once for all the results by doing variable {C : Set (Quot r)} {s : Set α} {c : Quot r} just before ncard_represents_inter. You could even put variable [Fintype α] before ncard_sdiff_represents_of_mem if you want. This is merely a suggestion, feel free to disregard it if you prefer to keep it that way.

Mathlib/Data/Set/Quot.lean

Co-authored-by: Etienne <66847262+EtienneC30@users.noreply.github.com>

EtienneC30 · 2025-01-30T09:06:26Z

Thanks!
maintainer merge

github-actions · 2025-01-30T09:06:44Z

🚀 Pull request has been placed on the maintainer queue by EtienneC30.

EtienneC30

Filling the lines

Mathlib/Data/Set/Quot.lean

Co-authored-by: Etienne <66847262+EtienneC30@users.noreply.github.com>

Mathlib/Data/Set/Quot.lean

eric-wieser · 2025-01-30T09:55:20Z

Mathlib/Data/Set/Quot.lean

+/-- Convert an equivalence class to a `Set`. -/
+def Quot.toSet (c : Quot r) : Set α := {v | Quot.mk r v = c}
+
+instance : SetLike (Quot r) α where


Can you add the other theorems that the module docstring for SetLike prescribes? For instance, that v ∈ c \iff Quot.mk r v = c?

I added the mem and ext lemma's. If the copy lemma's also apply here I'm not really sure how to implement that, so if it does, I'd appreciate a pointer:)

I think skipping copy is fine.

mattrobball · 2025-01-30T09:55:58Z

!bench

eric-wieser · 2025-01-30T09:55:58Z

Mathlib/Data/Set/Quot.lean

+namespace Set
+
+/-- A set represents a set of quotients if it contains exactly one element from each quotient. -/
+structure Represents (s : Set α) (C : Set (Quot r)) where


Is this the same as Set.BijOn Quot.mk s C?

Yep. That seems very clean. I switched to that as the definition and proved the previous components as results

leanprover-bot · 2025-01-30T10:23:05Z

Here are the benchmark results for commit a5a94d1.
There were no significant changes against commit a103782.

github-actions · 2025-01-30T10:23:35Z

File	Instructions	%
`build`	+14.106⬝10⁹	(+0.00%)
`Mathlib.CategoryTheory.Abelian.NonPreadditive`	+1.48⬝10⁹	(+4.02%)
CI run

…ib4 into PO_Quot_toSet

Mathlib/Data/Set/Quot.lean

Co-authored-by: Eric Wieser <efw@google.com>

eric-wieser · 2025-02-02T14:18:53Z

Mathlib/Data/Set/Quot.lean

+/-- A set represents a set of quotients if it contains exactly one element from each quotient. -/
+def Represents (s : Set α) (C : Set (Quot r)) := Set.BijOn (Quot.mk r) s C
+
+lemma out_image_represents (C : Set (Quot r)) : (Quot.out '' C).Represents C :=


Is there a general result about BijOn and functions which satisfy mk (out x) = x (RightInverse) here?

b-mehta · 2025-02-02T19:30:01Z

Mathlib/Data/Set/Quot.lean

+namespace Set
+
+/-- A set represents a set of quotients if it contains exactly one element from each quotient. -/
+def Represents (s : Set α) (C : Set (Quot r)) := Set.BijOn (Quot.mk r) s C


Suggested change

def Represents (s : Set α) (C : Set (Quot r)) := Set.BijOn (Quot.mk r) s C

def Represents (s : Set α) (C : Set (Quot r)) : Prop := Set.BijOn (Quot.mk r) s C

pimotte · 2025-02-06T15:34:15Z

On hold, likely to be superseded by #20024

pimotte · 2025-02-10T11:54:47Z

#20024 (the more specific version) was merged in favour of this one

feat(Data/Set): Representing the equivalence classes of a Quot

c1bc93f

pimotte added the t-data Data (lists, quotients, numbers, etc) label Jan 26, 2025

pimotte mentioned this pull request Jan 26, 2025

[Merged by Bors] - feat(Combinatorics/SimpleGraph/Path): representatives of connected components #20024

Closed

EtienneC30 reviewed Jan 27, 2025

View reviewed changes

EtienneC30 added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 27, 2025

pimotte and others added 2 commits January 28, 2025 07:44

Apply suggestions from code review

d6b7237

Co-authored-by: Etienne <66847262+EtienneC30@users.noreply.github.com>

Naming

f2f0726

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

EtienneC30 reviewed Jan 28, 2025

View reviewed changes

Mathlib/Data/Set/Quot.lean Outdated Show resolved Hide resolved

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

EtienneC30 self-assigned this Jan 28, 2025

EtienneC30 changed the title ~~feat(Data/Set): Representing the equivalence classes of a Quot~~ feat(Data/Set): representing the equivalence classes of a Quot Jan 28, 2025

Move newlines

758d27e

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

EtienneC30 reviewed Jan 28, 2025

View reviewed changes

Mathlib/Data/Set/Quot.lean Show resolved Hide resolved

Mathlib/Data/Set/Quot.lean Outdated Show resolved Hide resolved

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

Review comments

27cca52

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

EtienneC30 reviewed Jan 30, 2025

View reviewed changes

Mathlib/Data/Set/Quot.lean Outdated Show resolved Hide resolved

Variables

ffe0ad8

EtienneC30 added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 30, 2025

EtienneC30 reviewed Jan 30, 2025

View reviewed changes

Mathlib/Data/Set/Quot.lean Outdated Show resolved Hide resolved

Update Mathlib/Data/Set/Quot.lean

415ce9f

Co-authored-by: Etienne <66847262+EtienneC30@users.noreply.github.com>

pimotte removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 30, 2025

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jan 30, 2025

EtienneC30 reviewed Jan 30, 2025

View reviewed changes

Mathlib/Data/Set/Quot.lean Outdated Show resolved Hide resolved

Mathlib/Data/Set/Quot.lean Outdated Show resolved Hide resolved

Mathlib/Data/Set/Quot.lean Outdated Show resolved Hide resolved

Apply suggestions from code review

a5a94d1

Co-authored-by: Etienne <66847262+EtienneC30@users.noreply.github.com>

eric-wieser reviewed Jan 30, 2025

View reviewed changes

Mathlib/Data/Set/Quot.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 30, 2025

View reviewed changes

Ruben-VandeVelde added awaiting-author A reviewer has asked the author a question or requested changes. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jan 30, 2025

pimotte added 3 commits January 30, 2025 16:17

Add lemmas

f3843cb

Switch to bijOn

e321c07

Merge branch 'PO_Quot_toSet' of github.com:leanprover-community/mathl…

0b35b78

…ib4 into PO_Quot_toSet

pimotte removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 30, 2025

eric-wieser reviewed Jan 30, 2025

View reviewed changes

Mathlib/Data/Set/Quot.lean Outdated Show resolved Hide resolved

eric-wieser reviewed Jan 30, 2025

View reviewed changes

Mathlib/Data/Set/Quot.lean Show resolved Hide resolved

pimotte and others added 3 commits January 30, 2025 18:08

Apply suggestions from code review

ce555ea

Co-authored-by: Eric Wieser <efw@google.com>

Inline toSet

8e7e4fe

Fix naming

19daea8

eric-wieser reviewed Feb 2, 2025

View reviewed changes

b-mehta reviewed Feb 2, 2025

View reviewed changes

pimotte added the awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there label Feb 6, 2025

pimotte closed this Feb 10, 2025

pimotte removed the awaiting-zulip There is a Zulip discussion; the author should await and report/implement the decision reached there label Feb 10, 2025

YaelDillies deleted the PO_Quot_toSet branch August 17, 2025 11:41

	def Represents (s : Set α) (C : Set (Quot r)) := Set.BijOn (Quot.mk r) s C
	def Represents (s : Set α) (C : Set (Quot r)) : Prop := Set.BijOn (Quot.mk r) s C

Conversation

pimotte commented Jan 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Jan 26, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 19daea86d0

Import changes for modified files

Declarations diff

Uh oh!

EtienneC30 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

pimotte commented Jan 28, 2025

Uh oh!

Uh oh!

EtienneC30 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

EtienneC30 commented Jan 30, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

EtienneC30 commented Jan 30, 2025

Uh oh!

github-actions bot commented Jan 30, 2025

Uh oh!

EtienneC30 left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

eric-wieser Jan 30, 2025

Choose a reason for hiding this comment

Uh oh!

pimotte Jan 30, 2025

Choose a reason for hiding this comment

Uh oh!

eric-wieser Jan 30, 2025

Choose a reason for hiding this comment

Uh oh!

mattrobball commented Jan 30, 2025

Uh oh!

eric-wieser Jan 30, 2025

Choose a reason for hiding this comment

Uh oh!

pimotte Jan 30, 2025

Choose a reason for hiding this comment

Uh oh!

leanprover-bot commented Jan 30, 2025

Uh oh!

github-actions bot commented Jan 30, 2025

Uh oh!

Uh oh!

Uh oh!

eric-wieser Feb 2, 2025

Choose a reason for hiding this comment

Uh oh!

b-mehta Feb 2, 2025

Choose a reason for hiding this comment

Uh oh!

pimotte commented Feb 6, 2025

Uh oh!

pimotte commented Feb 10, 2025

Uh oh!

pimotte commented Jan 26, 2025 •

edited

Loading

github-actions bot commented Jan 26, 2025 •

edited

Loading

EtienneC30 commented Jan 30, 2025 •

edited

Loading