Skip to content

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

Closed
pimotte wants to merge 18 commits intomasterfrom
PO_component_rep
Closed

[Merged by Bors] - feat(Combinatorics/SimpleGraph/Path): representatives of connected components#20024
pimotte wants to merge 18 commits intomasterfrom
PO_component_rep

Conversation

@pimotte
Copy link
Copy Markdown
Collaborator

@pimotte pimotte commented Dec 17, 2024 •
edited by YaelDillies
Loading

Add the concept of a set of representatives of a connected component along with some basic lemma's on it.
In preparation for a proof of Tutte's theorem.

Open in Gitpod

Zulip thread on Tutte's

This PR is the result of cleaning up this file which gives some context to how this will be used further.

@pimotte pimotte added the t-combinatorics Combinatorics label Dec 17, 2024
@pimotte pimotte requested a review from YaelDillies December 17, 2024 14:34
@github-actions
Copy link
Copy Markdown

github-actions bot commented Dec 17, 2024 •
edited
Loading

messageFile.md

@YaelDillies YaelDillies requested a review from b-mehta December 23, 2024 14:46
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Dec 23, 2024

Looks okay to me, but I wonder whether we really want to provide API about some section rather than any section

@bryangingechen
Copy link
Copy Markdown
Contributor

bryangingechen commented Dec 23, 2024

I think "representant" (French, I'm assuming) is usually written as "representative" in English.

@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Dec 24, 2024
@pimotte pimotte changed the title feat(Combinatorics/SimpleGraph/Path): representant of connected component feat(Combinatorics/SimpleGraph/Path): representatives of connected components Dec 24, 2024
@pimotte
Copy link
Copy Markdown
Collaborator Author

pimotte commented Dec 24, 2024

Looks okay to me, but I wonder whether we really want to provide API about some section rather than any section

I've adapted it to this paradigm and added some more lemma's to see how it pans out, and I like the structure, I'm not entirely sure about naming.

@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Dec 24, 2024

Will wait on @b-mehta's opinion

@pimotte pimotte mentioned this pull request Jan 9, 2025
Closed
b-mehta
b-mehta reviewed Jan 24, 2025
View reviewed changes
Mathlib/Combinatorics/SimpleGraph/Path.lean Outdated
/-- A set of vertices represents a set of components if it contains exactly
one vertex from each component.
-/
structure _root_.Set.Represents (s : Set V) (C : Set (G.ConnectedComponent)) where
Copy link
Copy Markdown
Contributor

@b-mehta b-mehta Jan 24, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm, looking at this definition, it doesn't really seem like it's specific to graphs... That is, given a partition of a subset, it's reasonable to define a set of representatives for it. I could, however, believe that this formulation (using connectedComponent rather than an arbitrary partition) is helpful in your application. But it certainly doesn't look like it belongs in SimpleGraph/Path. Can we move this to a subfolder on connected components instead?

Copy link
Copy Markdown
Collaborator Author

@pimotte pimotte Jan 26, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have done this, but I have also put together #21097 as an alternative. In the past I have made missteps with Quot, and I'm still not really certain on the nuances and design of the Quot/ConnectedComponent situation.

If the alternative makes sense, I wonder if it also makes sense to migrate off supp and use the SetLike instance instead, so feel free to weigh in if you have any thoughts on that:)

Copy link
Copy Markdown
Collaborator Author

@pimotte pimotte Jan 27, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I just noticed we have the SetLike instance I introduced in that PR already for connected components

Is there a particular reason we use .supp explicitly and tend not to rely on this instance?

@b-mehta b-mehta added the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 24, 2025
@github-actions github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label Jan 26, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 26, 2025

messageFile.md

@github-actions
Copy link
Copy Markdown

github-actions bot commented Jan 26, 2025

messageFile.md

@pimotte pimotte mentioned this pull request Jan 26, 2025
Closed
@YaelDillies
Copy link
Copy Markdown
Contributor

YaelDillies commented Jan 26, 2025

Ah, can you merge master to fix the bot?

@github-actions
Copy link
Copy Markdown

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

PR summary 7e2b7f649c

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents (new file) 705

Declarations diff

+ Represents
+ disjoint_supp_of_not_mem
+ existsUnique_rep
+ image_out
+ ncard_inter
+ ncard_sdiff_of_mem
+ ncard_sdiff_of_not_mem

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

@pimotte pimotte removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 26, 2025
@pimotte
Copy link
Copy Markdown
Collaborator Author

pimotte commented Jan 30, 2025

Superseded by #21097 per discussion in the zulip thread linked above

@pimotte pimotte closed this Jan 30, 2025
@pimotte pimotte reopened this Feb 6, 2025
@pimotte
Copy link
Copy Markdown
Collaborator Author

pimotte commented Feb 6, 2025

Reopened after Zulip discussion on #21097 landing on it being better to not generalize for now.

YaelDillies
YaelDillies reviewed Feb 6, 2025
View reviewed changes
@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 6, 2025
pimotte and others added 2 commits February 6, 2025 17:23
@pimotte @YaelDillies
Apply suggestions from code review
535d35d 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@pimotte
Fixes
54fcfc3
@pimotte pimotte removed the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 6, 2025
YaelDillies
YaelDillies approved these changes Feb 6, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Feb 6, 2025

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

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Feb 6, 2025
pimotte and others added 2 commits February 6, 2025 20:11
@pimotte @YaelDillies
Apply suggestions from code review
6549fa7 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@pimotte
Formatting
7e2b7f6
@kbuzzard
Copy link
Copy Markdown
Member

kbuzzard commented Feb 10, 2025

Thanks!

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Feb 10, 2025
mathlib-bors bot pushed a commit that referenced this pull request Feb 10, 2025
@pimotte
feat(Combinatorics/SimpleGraph/Path): representatives of connected co…
db32519 
…mponents (#20024)

Add the concept of a set of representatives of a connected component along with some basic lemma's on it.
In preparation for a proof of Tutte's theorem.




Co-authored-by: Pim Otte <otte.pim@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Feb 10, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(Combinatorics/SimpleGraph/Path): representatives of connected components [Merged by Bors] - feat(Combinatorics/SimpleGraph/Path): representatives of connected components Feb 10, 2025
@mathlib-bors mathlib-bors bot closed this Feb 10, 2025
@mathlib-bors mathlib-bors bot deleted the PO_component_rep branch February 10, 2025 11:40
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@b-mehta b-mehta b-mehta left review comments

@YaelDillies YaelDillies YaelDillies approved these changes

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-combinatorics Combinatorics

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@pimotte @YaelDillies @bryangingechen @kbuzzard @b-mehta