feat(Combinatorics/SimpleGraph/InducedCopy): add UnlabeledEmbedding, unlabeledEmbeddingCount and embeddingCount#38631
Open
FordUniver wants to merge 25 commits into
Open
Conversation
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 0ef8fadc87Import changes exceeding 2%
|
| File | Base Count | Head Count | Change |
|---|---|---|---|
| Mathlib.Combinatorics.SimpleGraph.LineGraph | 600 | 779 | +179 (+29.83%) |
| Mathlib.Combinatorics.SimpleGraph.Copy | 599 | 777 | +178 (+29.72%) |
Import changes for all files
| Files | Import difference |
|---|---|
13 filesMathlib.Combinatorics.SimpleGraph.Circulant Mathlib.Combinatorics.SimpleGraph.Clique Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex Mathlib.Combinatorics.SimpleGraph.Coloring Mathlib.Combinatorics.SimpleGraph.CycleGraph Mathlib.Combinatorics.SimpleGraph.Hasse Mathlib.Combinatorics.SimpleGraph.Partition Mathlib.Combinatorics.SimpleGraph.Prod Mathlib.Combinatorics.SimpleGraph.Sum Mathlib.Combinatorics.SimpleGraph.Triangle.Basic Mathlib.Combinatorics.SimpleGraph.Triangle.Counting Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite |
1 |
Mathlib.Combinatorics.SimpleGraph.UnitDistance.Basic |
59 |
Mathlib.Combinatorics.SimpleGraph.Extremal.Basic |
99 |
Mathlib.Combinatorics.SimpleGraph.Copy |
178 |
Mathlib.Combinatorics.SimpleGraph.LineGraph |
179 |
Mathlib.Combinatorics.SimpleGraph.InducedCopy (new file) |
778 |
Declarations diff (regex)
+ Embedding.coe_ofIsInduced
+ Embedding.ofIsInduced
+ Embedding.toEmbedding_ofIsInduced
+ Embedding.toHom_ofIsInduced
+ IndFree
+ IndFree.congr_left
+ IndFree.congr_right
+ IsIndContained.congr_left
+ IsIndContained.congr_right
+ IsIndContained.trans'
+ IsInduced.map
+ IsInduced.map_iff
+ UnlabeledCopy
+ UnlabeledEmbedding
+ copyCount_eq_nat_card
+ embeddingCount
+ embeddingCount_eq_nat_card
+ embeddingCount_eq_zero
+ embeddingCount_le_copyCount
+ embeddingCount_of_isEmpty
+ embeddingCount_pos
+ indFree_bot
+ indFree_congr
+ indFree_congr_left
+ indFree_congr_right
+ instance : FunLike (Copy G H) V W
+ instance : IsPreorder (SimpleGraph V) IsContained
+ instance : IsPreorder (SimpleGraph V) IsIndContained
+ instance [Finite V] [Finite W] : Finite (Embedding G H)
+ instance [Finite V] [Finite W] : Finite (G.Copy H)
+ instance [Finite W] : Finite (G.UnlabeledCopy H) := Subtype.finite
+ instance [Finite W] : Finite (G.UnlabeledEmbedding H) := Subtype.finite
+ instance [IsEmpty V] : Nonempty (Copy G H) := IsContained.of_isEmpty
+ instance [IsEmpty V] : Nonempty (G.UnlabeledCopy H)
+ instance [IsEmpty V] : Nonempty (G.UnlabeledEmbedding H)
+ instance [IsEmpty V] : Subsingleton (G.UnlabeledCopy H)
+ instance [IsEmpty V] : Subsingleton (G.UnlabeledEmbedding H)
+ instance [IsEmpty V] : Unique (Embedding G H)
+ isIndContained_congr
+ isIndContained_congr_left
+ isIndContained_congr_right
+ le_card_edgeFinset_killCopies_add_unlabeledCopyCount
+ not_indFree
+ range_toSubgraph
+ toEmbedding_apply
+ toSubgraph_isInduced
+ topEmbedding_apply
+ uniqueUnlabeledCopyBot
+ unlabeledCopyCount
+ unlabeledCopyCount_bot
+ unlabeledCopyCount_eq_card_image_copyToSubgraph
+ unlabeledCopyCount_eq_nat_card
+ unlabeledCopyCount_eq_zero
+ unlabeledCopyCount_le_copyCount
+ unlabeledCopyCount_of_isEmpty
+ unlabeledCopyCount_pos
+ unlabeledEmbeddingCount
+ unlabeledEmbeddingCount_eq_nat_card
+ unlabeledEmbeddingCount_eq_zero
+ unlabeledEmbeddingCount_le_embeddingCount
+ unlabeledEmbeddingCount_le_unlabeledCopyCount
+ unlabeledEmbeddingCount_of_isEmpty
+ unlabeledEmbeddingCount_pos
- copyCount_bot
- copyCount_le_labelledCopyCount
- instance : FunLike (Copy A B) α β
- instance : IsPreorder (SimpleGraph α) IsContained
- instance : IsPreorder (SimpleGraph α) IsIndContained
- le_card_edgeFinset_killCopies_add_copyCount
-++ toSubgraph
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
Declarations diff (Lean -- pending)
Computed after the build finishes.
No changes to strong technical debt.
Decrease in weak tech debt: (relative, absolute) = (1.00, 0.00)
| Current number | Change | Type (weak) |
|---|---|---|
| 5012 | -1 | exposed public sections |
Current commit 0ef8fadc87
Reference commit 47550252e7
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
FordUniver
force-pushed
the
feat/ind-copy-count
branch
from
April 28, 2026 11:53
2b7a1dd to
578c033
Compare
SnirBroshi
added
the
LLM-generated
YaelDillies
reviewed
Apr 29, 2026
YaelDillies
added
the
awaiting-author
FordUniver
force-pushed
the
feat/ind-copy-count
branch
2 times, most recently
from
April 29, 2026 12:33
63c61b8 to
bed1873
Compare
FordUniver
removed
the
awaiting-author
YaelDillies
reviewed
Apr 29, 2026
YaelDillies
added
the
awaiting-author
plp127
reviewed
Apr 29, 2026
FordUniver
removed
the
awaiting-author
SnirBroshi
reviewed
Apr 29, 2026
SnirBroshi
reviewed
Apr 29, 2026
SnirBroshi
reviewed
Apr 29, 2026
Collaborator
|
Hey, can you please edit the PR description to avoid AI walls of text above the |
FordUniver
changed the title
1 task
Contributor
|
Following discussions in DMs, I find that this PR wasn't actually LLM-generated. Christoph merely asked his LLM questions about naming and proof style, rather than "generating" the code. |
YaelDillies
removed
the
LLM-generated
Collaborator
|
Oh, I was kinda happy that we got good-quality LLM code, I guess LLMs are still far from that |
YaelDillies
reviewed
May 1, 2026
YaelDillies
added
the
awaiting-author
|
This pull request has conflicts, please merge |
2 tasks
|
This pull request has conflicts, please 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.
… and `IsInduced.map` Three additions to the `SimpleGraph.Subgraph` API for induced subgraphs: * `Subgraph.IsInduced.map (hH : H.IsInduced) (e : G ↪g G') : (H.map e.toHom).IsInduced` — the image of an induced subgraph under a graph embedding is induced (an embedding both preserves and reflects adjacency, so adjacency in the image forces a preimage edge). * `Subgraph.IsInduced.map_iff (e : G ≃g G') : (H.map e.toHom).IsInduced ↔ H.IsInduced` — strengthens the above to an iff when `e` is an isomorphism, using the other direction via `e.symm`. Tagged `@[simp]`. * `Embedding.ofIsInduced (G' : G.Subgraph) (hG' : G'.IsInduced) : G'.coe ↪g G` — the canonical embedding of an induced subgraph into its ambient graph, paired with `toHom_ofIsInduced` and `ofIsInduced_apply` `@[simp]` lemmas. This is the embedding counterpart of `Subgraph.hom : G'.coe →g G`, which only produces a homomorphism because non-induced subgraphs do not reflect adjacency.
|
This pull request has conflicts, please merge |
…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.
…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 `UnlabeledCopy G H` carrier (introduced in the previous PR) is paired with the count `H.unlabeledCopyCount 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 guest-first (`Copy G H`, `UnlabeledCopy G H`); operations are host-first via dot notation (`H.copyCount G`, `H.unlabeledCopyCount 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 → unlabeledCopyCount` 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 → unlabeledCopyCount_bot` (count name rename only; `_bot` spelling preserved per @SnirBroshi). * 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 (`UnlabeledCopy` / `unlabeledCopyCount` bullets, logical-flow ordering, `SimpleGraph.Subgraph` cross-references); add TODOs for `homCount` and the three densities.
…th selective exposure
Replace `@[expose] public section` with a plain `public section` and
restore selective `@[expose]` on only the declarations that need
cross-module reduction:
* `Copy.toEmbedding`, `Copy.id`, `Copy.ofLE`, `Copy.topEmbedding` — the
small constructive copy `def`s, kept transparent so consumers can
elaborate against them by reducing.
* `copyCount`, `subCount` — the noncomputable counts. These need to be
exposed so downstream files (e.g. the upcoming `InducedCopy.lean` in
feat/ind-copy-count) can prove bridging inequalities like
`embCount_le_copyCount` and `indSubCount_le_subCount` directly via
`Nat.card_le_card_of_injective`.
Also:
* Inline the `@[simps!]` projections of `Copy.topEmbedding` into a manual
`@[simp] lemma topEmbedding_apply` (and similarly for `Copy.toEmbedding`).
The auto-generated `simps` form attached to `@[simps!]` was opaque to
cross-module simp; the manual form is small enough to ship as a one-line
named lemma. The body of `topEmbedding` is also tightened from
`fun {v w} ↦ ⟨fun h ↦ by simpa using h.ne, _⟩` to
`fun {_ _} ↦ ⟨fun h ↦ f.injective.ne_iff.mp h.ne, _⟩`.
* `IsIndContained` switches from `def` to `abbrev`, since the body
`Nonempty (G ↪g H)` is small and downstream Lean elaboration benefits
from automatic unfolding here.
…yCount to Nat.card * `copyCount` and `unlabeledCopyCount` redefined via `Nat.card` instead of `Fintype.card`. * `Fintype` hypotheses weakened to `Finite` throughout (`copyCount_eq_zero`, `copyCount_pos`, `unlabeledCopyCount_eq_zero`, `unlabeledCopyCount_pos`, `unlabeledCopyCount_le_copyCount`, `uniqueUnlabeledCopyBot`, `unlabeledCopyCount_bot`, `unlabeledCopyCount_of_isEmpty`, `bot_isContained_iff_card_le`, `le_card_edgeFinset_killCopies`, `le_card_edgeFinset_killCopies_add_unlabeledCopyCount`). * `bot_isContained_iff_card_le`: `Fintype.card → Nat.card`. * New `Finite (G.Copy H)` instance (sibling to the existing `Fintype` instance). * New `Nonempty (Copy G H)` instance for `[IsEmpty V]`, used to give a one-line `copyCount_of_isEmpty` proof via `Nat.card_unique`. * New `copyCount_eq_nat_card` and `unlabeledCopyCount_eq_nat_card` bridge lemmas exposing the underlying `Nat.card`, intended as the public characterisation since the count bodies are deliberately not `@[expose]`d. * New private `Nonempty` / `Subsingleton` instances on `G.UnlabeledCopy H` for `[IsEmpty V]`, used to give a one-line `unlabeledCopyCount_of_isEmpty` proof via `Nat.card_unique`. * `le_card_edgeFinset_killCopies` proof simplified accordingly.
…nto new file Extract induced-containment material from `Copy.lean` into a new `Mathlib/Combinatorics/SimpleGraph/InducedCopy.lean`, parallelling the non-induced `copyCount` / `unlabeledCopyCount` API: * `IsIndContained`, `⊴`, and all related lemmas (`Embedding.isIndContained`, `Iso.isIndContained`/`'`, `Subgraph.IsInduced.isIndContained`, `IsIndContained.refl`/`rfl`/`trans`, `IsPreorder`/`Trans` instances, `IsIndContained.of_isEmpty`, `isIndContained_iff_exists_iso_subgraph`, `isIndContained_iff_exists_iso_induce`, `top_isIndContained_iff_top_isContained`, `compl_isIndContained_compl`, `isIndContained_iff_exists_comap_eq`) move from `Copy.lean` to `InducedCopy.lean`. * New `SimpleGraph.UnlabeledEmbedding G H` abbrev: induced subgraphs of `H` isomorphic to `G`, the induced analogue of `UnlabeledCopy G H`. * New `SimpleGraph.embeddingCount H G := Nat.card (G ↪g H)`: count of induced labeled copies (i.e. graph embeddings), with `_eq_nat_card`, `_of_isEmpty`, `_eq_zero`, `_pos`, `_le_copyCount`. * New `SimpleGraph.unlabeledEmbeddingCount H G := Nat.card (G.UnlabeledEmbedding H)`: count of induced unlabeled copies, with `_eq_nat_card`, `_eq_zero`, `_pos`, `_le_embeddingCount`, `_of_isEmpty`, `_le_unlabeledCopyCount`. * New `Embedding.toSubgraph` and `Embedding.range_toSubgraph` characterising induced subgraphs as the range of `(·.toCopy.toSubgraph) : (G ↪g H) → H.Subgraph`. Bookkeeping in `Copy.lean`: the module docstring is updated to point at `InducedCopy.lean` for the induced story; induced TODOs and placeholder sections are removed; `Copy.isContained`, `Embedding.isContained`, `Iso.isContained`/`'`, and `isContained_iff_exists_le_comap` (non-induced) move up into the `IsContained` section. Supporting additions in `Subgraph.lean` (from the diffbase merge of `feat/subgraph-ofIsInduced`): * `Subgraph.IsInduced.map` and `Subgraph.IsInduced.map_iff` (for embeddings and isomorphisms). * `Embedding.ofIsInduced`: the canonical embedding of an induced subgraph into the ambient graph, with `toHom_ofIsInduced` and `ofIsInduced_apply` simp lemmas. `LineGraph.lean` switches its `Copy` import to `InducedCopy`, as it uses `IsIndContained`.
…ubgraph` API to the top Moves the `namespace Embedding` block (containing `toSubgraph`, `toSubgraph_isInduced`, and `range_toSubgraph`) out of `section UnlabeledEmbeddingCount` to its own block immediately after the `SimpleGraph` namespace opens, with a section heading `Embedding to subgraph`. This mirrors `Copy.lean`'s structure (where `Copy.toSubgraph` and `range_toSubgraph` live in the early `section Copy` / `namespace Copy` block alongside the type's core API, separately from the count sections). The previous placement nested the core embedding-image API inside the unlabelled count section, which made it harder to find when navigating the file. Pure code motion: no statement, proof, or attribute changes.
…tead of `G ↪g H` Mirror the spelled-out `Copy G H` / `UnlabeledEmbedding G H` style throughout signatures, return types, subtype clauses, type-level operations (`Nat.card`, `Unique`, `Finite`, `Nonempty`), and docstring prose. The 2×2 grid Copy G H UnlabeledCopy G H Embedding G H UnlabeledEmbedding G H now reads as a grid everywhere. Re-flow two docstring lines to stay under the 100-char limit.
|
This pull request has conflicts, please merge |
…of of copyCount_le_labelledCopyCount
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Extracts the induced-containment material from
SimpleGraph/Copy.leaninto a newSimpleGraph/InducedCopy.leanand adds the induced analogues ofUnlabeledCopy/copyCount/unlabeledCopyCount: a typeUnlabeledEmbedding G Hfor induced subgraphs ofHisomorphic toG, a countH.embeddingCount G := Nat.card (G ↪g H)for induced labeled copies (i.e. graph embeddings), and a countH.unlabeledEmbeddingCount G := Nat.card (G.UnlabeledEmbedding H)for induced unlabelled copies, each with the parallel_of_isEmpty/_eq_zero/_pos/_le_*/_eq_nat_cardAPI.IsIndContained, the⊴notation,IndFree, and all related lemmas move fromCopy.leanto the new file.Embedding.range_toSubgraphcharacterises induced subgraphs as the range ofEmbedding.toSubgraph : (G ↪g H) → H.Subgraphand bridgesembeddingCounttounlabeledEmbeddingCount.Co-authored-by: Malte Jackisch 45597826+MaltyBlanket@users.noreply.github.com
Final step 5/5 of the
Copy/InducedCopyrefactor stack.The new file mirrors
Copy.lean's organisation (containment → counting → killing sections) for the induced row; the killing-induced-copies machinery is left as a TODO. Naming follows the convention established in #38745: types are guest-first (UnlabeledEmbedding G H,IsIndContained G H), operations host-first (H.embeddingCount G,H.unlabeledEmbeddingCount G). The induced labelled type isEmbedding, i.e.,G ↪g H, directly. Two bookkeeping changes inCopy.lean:Copy.isContained/Embedding.isContained/Iso.isContained/'andisContained_iff_exists_le_comap, which lived in the now-deleted "Induced containment" section but are non-induced, move up into theIsContainedsection.LineGraph.lean'sCopyimport switches toInducedCopysince it usesIsIndContained. The cross-module proofsembeddingCount_le_copyCountandunlabeledEmbeddingCount_le_unlabeledCopyCountbridge through the publiccopyCount_eq_nat_card/unlabeledCopyCount_eq_nat_cardlemmas introduced in #38931 (the counts themselves remain unexposed per @plp127's review).Embedding.ofIsInduced(used byEmbedding.range_toSubgraph) comes from the independent prerequisite #39288.Copy/copyCountUnlabeledCopy/unlabeledCopyCountEmbedding/embeddingCountUnlabeledEmbedding/unlabeledEmbeddingCountThis branch sits on top of an octopus-merge diffbase (
FordUniver:diffbase/ind-copy-count) ofchore/copy-nat-cardandfeat/subgraph-ofIsInduced, so the link below shows only the changes intrinsic to this PR.Fintype.cardwithNat.card#38931Embedding.ofIsInducedandIsInduced.map#39288Diff for the changes just in this PR over its predecessors: link.