feat(Combinatorics/SimpleGraph/Copy): introduce UnlabeledCopy carrier subtype#39307
feat(Combinatorics/SimpleGraph/Copy): introduce UnlabeledCopy carrier subtype#39307FordUniver wants to merge 9 commits into
UnlabeledCopy carrier subtype#39307Conversation
PR summary 40e1050f36Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
|
This pull request is now in draft mode. No active bors state needed cleanup. While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like |
387b6ac to
cfa3bc5
Compare
…y graph variables Aligns the labelled/unlabelled naming in `Copy.lean` so that the type `Copy G H` (labelled, injective hom from `G` into `H`) is paired with the count `H.copyCount G` (labelled count, host-first per mathlib op convention) and the `Sub G H` carrier (introduced in the previous PR) is paired with the count `H.subCount G`. Also unifies the graph-variable letters: the `A B C` set that was local to `Copy.lean` is dropped in favour of mathlib's wider `G H I` convention, with `α β γ` → `V W X` correspondingly. Within the new convention `G` is the guest (pattern, contained side) and `H` is the host (container), matching `G ⊑ H` and the hom direction `G →g H`. Types are pattern-first (`Copy G H`, `Sub G H`); operations are host-first via dot notation (`H.copyCount G`, `H.subCount G`, `H.killCopies G`). This matches the existing mathlib convention split (hom types use source-first, host-side operations use the host as the dot-notation receiver). Changes: * Rename `labelledCopyCount → copyCount` (with British `@[deprecated]` alias `labelledCopyCount`). The previous `copyCount → subCount` rename has no alias — `copyCount` is reassigned to mean the labelled count. Same for the `_of_isEmpty` / `_eq_zero` / `_pos` lemma families. * Rename `copyCount_bot → subCount_emptyGraph` and `uniqueSubBot → uniqueSubEmptyGraph` (folding the planned `_bot → _emptyGraph` naming alignment with leanprover-community#23838's convention; both names were introduced in the preceding `feat/copy-sub-abbrev` PR (leanprover-community#39307) and would otherwise have needed a separate rename PR with brief-window deprecated aliases). * Unify `A B C / α β γ` to `G H I / V W X` throughout. Variable block follows the mathlib convention (cf. `SimpleGraph/Maps.lean`): subscripted names (`G₁ G₂ G₃`) for same-vertex-type variants used in `≤` chains and `ofLE`; primed names (`G'`, `H'`) on independent universes (`V'`, `W'`) for the cross-universe variants used in `isContained_congr` / `free_congr` (and their `_left` / `_right` partial-iso forms). This preserves the universe polymorphism the old `A B C / α β γ` block provided implicitly and that `Extremal/Basic.lean` (line 96, `← free_congr .refl (.map e G)`) relies on. * Fix the docstring direction on `IsContained.trans` and `.trans'`: the previous wording ("`G` contains `H`") read the relation backwards relative to the lemma signature (`G ⊑ H` means `G` is contained in `H`). * Update module docstring (`Sub`/`subCount` bullets, logical-flow ordering, `SimpleGraph.Subgraph` cross-references); add TODOs for `homCount` and the three densities.
…y graph variables Aligns the labelled/unlabelled naming in `Copy.lean` so that the type `Copy G H` (labelled, injective hom from `G` into `H`) is paired with the count `H.copyCount G` (labelled count, host-first per mathlib op convention) and the `Sub G H` carrier (introduced in the previous PR) is paired with the count `H.subCount G`. Also unifies the graph-variable letters: the `A B C` set that was local to `Copy.lean` is dropped in favour of mathlib's wider `G H I` convention, with `α β γ` → `V W X` correspondingly. Within the new convention `G` is the guest (pattern, contained side) and `H` is the host (container), matching `G ⊑ H` and the hom direction `G →g H`. Types are pattern-first (`Copy G H`, `Sub G H`); operations are host-first via dot notation (`H.copyCount G`, `H.subCount G`, `H.killCopies G`). This matches the existing mathlib convention split (hom types use source-first, host-side operations use the host as the dot-notation receiver). Changes: * Rename `labelledCopyCount → copyCount` (with British `@[deprecated]` alias `labelledCopyCount`). The previous `copyCount → subCount` rename has no alias — `copyCount` is reassigned to mean the labelled count. Same for the `_of_isEmpty` / `_eq_zero` / `_pos` lemma families. * Rename `copyCount_bot → subCount_emptyGraph` and `uniqueSubBot → uniqueSubEmptyGraph` (folding the planned `_bot → _emptyGraph` naming alignment with leanprover-community#23838's convention; both names were introduced in the preceding `feat/copy-sub-abbrev` PR (leanprover-community#39307) and would otherwise have needed a separate rename PR with brief-window deprecated aliases). * Unify `A B C / α β γ` to `G H I / V W X` throughout. Variable block follows the mathlib convention (cf. `SimpleGraph/Maps.lean`): subscripted names (`G₁ G₂ G₃`) for same-vertex-type variants used in `≤` chains and `ofLE`; primed names (`G'`, `H'`) on independent universes (`V'`, `W'`) for the cross-universe variants used in `isContained_congr` / `free_congr` (and their `_left` / `_right` partial-iso forms). This preserves the universe polymorphism the old `A B C / α β γ` block provided implicitly and that `Extremal/Basic.lean` (line 96, `← free_congr .refl (.map e G)`) relies on. * Fix the docstring direction on `IsContained.trans` and `.trans'`: the previous wording ("`G` contains `H`") read the relation backwards relative to the lemma signature (`G ⊑ H` means `G` is contained in `H`). * Update module docstring (`Sub`/`subCount` bullets, logical-flow ordering, `SimpleGraph.Subgraph` cross-references); add TODOs for `homCount` and the three densities.
|
bors r+ |
|
🔒 Permission denied Existing reviewers: click here to make FordUniver a reviewer |
There was a problem hiding this comment.
I like how the definitions mirror the Copy equivalents.
What about UnlabeledCopy instead of Sub to be a bit more verbose? Then the file naming is consistent (eventually) and readable for the uninitiated.
*Copy* for labeled versions. *UnlabeledCopy* for unlabeled versions.
@mitchell-horner I'm also not 100% convinced by Already looking ahead at #38631, what do we use for the induced site? An induced labeled copy is already
|
FordUniver
changed the title
Sub carrier subtypeUnlabeledCopy carrier subtype
b229ca9 to
ec8a655
Compare
…y graph variables Aligns the labelled/unlabelled naming in `Copy.lean` so that the type `Copy G H` (labelled, injective hom from `G` into `H`) is paired with the count `H.copyCount G` (labelled count, host-first per mathlib op convention) and the `Sub G H` carrier (introduced in the previous PR) is paired with the count `H.subCount G`. Also unifies the graph-variable letters: the `A B C` set that was local to `Copy.lean` is dropped in favour of mathlib's wider `G H I` convention, with `α β γ` → `V W X` correspondingly. Within the new convention `G` is the guest (pattern, contained side) and `H` is the host (container), matching `G ⊑ H` and the hom direction `G →g H`. Types are pattern-first (`Copy G H`, `Sub G H`); operations are host-first via dot notation (`H.copyCount G`, `H.subCount G`, `H.killCopies G`). This matches the existing mathlib convention split (hom types use source-first, host-side operations use the host as the dot-notation receiver). Changes: * Rename `labelledCopyCount → copyCount` (with British `@[deprecated]` alias `labelledCopyCount`). The previous `copyCount → subCount` rename has no alias — `copyCount` is reassigned to mean the labelled count. Same for the `_of_isEmpty` / `_eq_zero` / `_pos` lemma families. * Rename `copyCount_bot → subCount_emptyGraph` and `uniqueSubBot → uniqueSubEmptyGraph` (folding the planned `_bot → _emptyGraph` naming alignment with leanprover-community#23838's convention; both names were introduced in the preceding `feat/copy-sub-abbrev` PR (leanprover-community#39307) and would otherwise have needed a separate rename PR with brief-window deprecated aliases). * Unify `A B C / α β γ` to `G H I / V W X` throughout. Variable block follows the mathlib convention (cf. `SimpleGraph/Maps.lean`): subscripted names (`G₁ G₂ G₃`) for same-vertex-type variants used in `≤` chains and `ofLE`; primed names (`G'`, `H'`) on independent universes (`V'`, `W'`) for the cross-universe variants used in `isContained_congr` / `free_congr` (and their `_left` / `_right` partial-iso forms). This preserves the universe polymorphism the old `A B C / α β γ` block provided implicitly and that `Extremal/Basic.lean` (line 96, `← free_congr .refl (.map e G)`) relies on. * Fix the docstring direction on `IsContained.trans` and `.trans'`: the previous wording ("`G` contains `H`") read the relation backwards relative to the lemma signature (`G ⊑ H` means `G` is contained in `H`). * Update module docstring (`Sub`/`subCount` bullets, logical-flow ordering, `SimpleGraph.Subgraph` cross-references); add TODOs for `homCount` and the three densities.
|
I have switched over to |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
ec8a655 to
8006d6e
Compare
github-actions
Bot
removed
the
merge-conflict
YaelDillies
left a comment
YaelDillies
left a comment
There was a problem hiding this comment.
Thanks! 🚀
maintainer merge
|
🚀 Pull request has been placed on the maintainer queue by YaelDillies. |
mathlib-triage
Bot
added
the
maintainer-merge
Adds `abbrev Sub A B := {B' : B.Subgraph // Nonempty (A ≃g B'.coe)}`, the
subtype of `SimpleGraph.Subgraph`s of `B` isomorphic to `A`. Redefines
`copyCount G H` via `Fintype.card (H.Sub G)`, replacing the previous inline
filter-set body, and rewrites the affected proofs (`copyCount_eq_zero`,
`copyCount_pos`, `copyCount_le_labelledCopyCount`, `copyCount_bot`,
`le_card_edgeFinset_killCopies`) to use `Sub` directly.
The singleton-empty-subgraph reasoning previously inlined in `copyCount_bot`'s
proof is factored out as `instance uniqueSubBot (G : SimpleGraph V) :
Unique ((⊥ : SimpleGraph V).Sub G)`, making `copyCount_bot` a one-liner via
`Fintype.card_unique`. The cardinality proof inside the instance stays inline
to keep the introduction minimal — extraction to a separate private helper
and the rename to `_emptyGraph` per the convention from leanprover-community#23838 (and adopted
in `AdjMatrix.lean`) happen in the next PR.
Drops `copyCount_eq_card_image_copyToSubgraph` (the legacy bridge between the
filter-set and Finset.image-of-Copy.toSubgraph forms) — unused after the
type-form refactor.
8006d6e to
65fb74a
Compare
SnirBroshi
left a comment
SnirBroshi
left a comment
There was a problem hiding this comment.
Please avoid force-pushing (as the contribution guide recommends)
b-mehta
added
the
awaiting-author
FordUniver
removed
the
awaiting-author
…copyToSubgraph as deprecated Restores the exact statement of the legacy bridge lemma dropped when copyCount was redefined via UnlabeledCopy, now carrying @[deprecated] (since 2026-07-12) per review, with a proof against the new Fintype.card (H.UnlabeledCopy G) body.
b-mehta
left a comment
b-mehta
left a comment
There was a problem hiding this comment.
Large parts of this PR, including the description, appear LLM-generated. Can you comment on your use of AI here?
|
|
||
| /-- `UnlabeledCopy A B` is the type of `SimpleGraph.Subgraph`s of `B` isomorphic to `A`. | ||
| The corresponding count is `SimpleGraph.copyCount`. -/ | ||
| abbrev UnlabeledCopy (A : SimpleGraph α) (B : SimpleGraph β) : Type _ := |
There was a problem hiding this comment.
What's the reason this is an abbrev as opposed to a definition (like all the other analogous definitions)?
There was a problem hiding this comment.
I'm gonna be honest that I don't yet fully understand the current conventions on def vs abbrev vs @[expose] def. My intuition here was that it was previously defined inline (using Set rather than as a subtype) and abbrev stays closest to that. But I am happy to change it to def (and then presumably to @[expose] def in #38843 where the file wide exposure is removed).
There was a problem hiding this comment.
So changing it to @[expose] def in this PR introduces some nastiness since it precedes the switch from Fintype.card to Nat.card. In #38931 (which already introduces a Finite (G.UnlabeledCopy H) instance) it is a much cleaner transition and only requires to additional rw.
I would suggest to keep it as abbrev here and I update #38931, but I'll leave this unresolved for now.
b-mehta
added
awaiting-author
…of of copyCount_le_labelledCopyCount
FordUniver
removed
the
awaiting-author
Thank you for your review. Two of your points were easy to address, one I would defer until #38931. This PR was not "in large parts LLM generated" and I don't see how you reached this conclusion. We had this discussion before, please let me know if anything changed and I am happy to again include the same disclaimer that I had previously included. I am frankly not ecstatic about the fact that the (very valid) annoyance of mathlib maintainers and reviewers at the onslaught of vibed PRs seems to result in denigrating contributions that took genuine effort. All issues that you rightfully flagged are not due to an LLM but instead due to an originally compact and self-contained PR that closed an explicit TODO (#38631 ) being explicitly asked to deal with:
I didn't particularly enjoy any of these tasks or managing a PR stack of this size, nor do I claim to be an expert at either. But I am happy to try and contribute in this very small way. Any actually feedback about content I am very happy about and usually address quickly. Yet another comment on a docstring looking like ChatGPT I don't really care for. |
5 participants
Adds
abbrev UnlabeledCopy A B := {B' : B.Subgraph // Nonempty (A ≃g B'.coe)}and uses it to replace the previous inline filter-set body ofcopyCount G H. Drops the now unused legacy Finset-image bridgecopyCount_eq_card_image_copyToSubgraph. AddsuniqueUnlabeledCopyBotinstance socopyCount_botis a one-liner viaFintype.card_unique.Co-authored-by: Malte Jackisch 45597826+MaltyBlanket@users.noreply.github.com
Step 1/5 of the
Copy/InducedCopyrefactor-feat stack.This PR isolates the
UnlabeledCopytype introduction and the count's type-form redefinition from the larger rename/convention work in the rest of the stack. Note that resolving the current clash in naming (CopyandUnlabeledCopyvslabelledCopyCountandcopyCount) is part of #38745.