feat(Combinatorics/SimpleGraph): canonical projection and representative between labeled and unlabeled copies#39571
Draft
FordUniver wants to merge 15 commits into
Draft
Conversation
1 task
github-actions
Bot
added
large-import
PR summary 21db757fdbImport 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)
+ Copy.toUnlabeledCopy
+ Copy.toUnlabeledCopy_val
+ Embedding.coe_ofIsInduced
+ Embedding.ofIsInduced
+ Embedding.toEmbedding_ofIsInduced
+ Embedding.toHom_ofIsInduced
+ Embedding.toUnlabeledEmbedding
+ Embedding.toUnlabeledEmbedding_val
+ IndFree
+ IndFree.congr_left
+ IndFree.congr_right
+ IsIndContained.congr_left
+ IsIndContained.congr_right
+ IsIndContained.trans'
+ IsInduced.map
+ IsInduced.map_iff
+ UnlabeledCopy
+ UnlabeledCopy.exists_toSubgraph_eq_val
+ UnlabeledCopy.out
+ UnlabeledCopy.toSubgraph_out
+ UnlabeledEmbedding
+ UnlabeledEmbedding.exists_toSubgraph_eq_val
+ UnlabeledEmbedding.out
+ UnlabeledEmbedding.toSubgraph_out
+ 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_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) |
|---|---|---|
| 5002 | -1 | exposed public sections |
Current commit 21db757fdb
Reference commit 80ffd59621
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).
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
|
This PR/issue depends on: |
1 task
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
FordUniver
force-pushed
the
feat/copy-toUnlabeled-out
branch
from
May 25, 2026 07:10
71644f4 to
ec5fe6b
Compare
github-actions
Bot
removed
the
merge-conflict
FordUniver
marked this pull request as draft
May 28, 2026 08:04
Contributor
|
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 |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
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.
FordUniver
force-pushed
the
feat/copy-toUnlabeled-out
branch
from
June 13, 2026 19:55
ec5fe6b to
ff84003
Compare
github-actions
Bot
removed
the
merge-conflict
FordUniver
force-pushed
the
feat/copy-toUnlabeled-out
branch
from
June 13, 2026 20:16
ff84003 to
2f0b68f
Compare
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
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.
…opy.out` (and embedding mirror) Add the standard `Quot.mk` / `Quot.out` style toolage for converting between labeled and unlabeled copies / embeddings: * `Copy.toUnlabeledCopy : Copy G H → G.UnlabeledCopy H` — canonical projection (computable). * `UnlabeledCopy.out : G.UnlabeledCopy H → Copy G H` — non-canonical representative (noncomputable). * `Copy.toUnlabeledCopy_val` and `UnlabeledCopy.toSubgraph_out` give the matching simp specs. * `UnlabeledCopy.exists_toSubgraph_eq_val` packages the underlying existence statement. Mirrored on the Embedding side: `Embedding.toUnlabeledEmbedding`, `UnlabeledEmbedding.exists_toSubgraph_eq_val`, `UnlabeledEmbedding.out`, and their respective spec lemmas. Refactor the existing `unlabeledCopyCount_le_copyCount` and `unlabeledEmbeddingCount_le_embeddingCount` proofs to use the new names — both shrink from a 5- and 7-line `apply ... ; rintro ...; obtain ...; exact ...` chain to a two-line `exact Nat.card_le_card_of_surjective ... fun S ↦ ⟨S.out, ...⟩`.
FordUniver
force-pushed
the
feat/copy-toUnlabeled-out
branch
from
July 12, 2026 02:21
2f0b68f to
21db757
Compare
github-actions
Bot
added
tech debt
|
This pull request has conflicts, please merge |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
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
1 participant
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.
Introduces canonical projection and noncomputable representative functions between labeled and unlabeled copies (and their embedding analogues) in
SimpleGraph, in the spirit ofQuot.mk/Quot.out. The pair gives a name to a construction that previously appeared as inlined anonymous-constructor and destructuring patterns; two pre-existing proofs inCopy.leanandInducedCopy.leanare tightened by routing through the new functions instead.Co-authored-by: Malte Jackisch 45597826+MaltyBlanket@users.noreply.github.com
Split out from a downstream PR introducing
SimpleGraph.Autand the orbit-stabiliser identities for copies and embeddings, where the projection and representative primitives recur in fiber decompositions and product equivalences. Sits on top of theCopy/InducedCopystack and inherits the "large-import" tag from it.UnlabeledEmbedding,unlabeledEmbeddingCountandembeddingCount#38631Diff for the changes just in this PR over its predecessor: link