feat(Combinatorics/SimpleGraph/Automorphism): Aut, autCount, and orbit-stabiliser for copies and embeddings#39573
Draft
FordUniver wants to merge 19 commits into
Draft
Conversation
github-actions
Bot
added
large-import
PR summary 9255371060Import 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 |
Mathlib.Combinatorics.SimpleGraph.Automorphism (new file) |
779 |
Declarations diff (regex)
+ Aut
+ Copy.toEmbeddingOfIsInduced
+ Copy.toEmbeddingOfIsInduced_apply
+ 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
+ Iso.toCopy_toSubgraph
+ UnlabeledCopy
+ UnlabeledCopy.exists_toSubgraph_eq_val
+ UnlabeledCopy.out
+ UnlabeledCopy.toSubgraph_out
+ UnlabeledEmbedding
+ UnlabeledEmbedding.exists_toSubgraph_eq_val
+ UnlabeledEmbedding.out
+ UnlabeledEmbedding.toSubgraph_out
+ apply_eq_iff_eq
+ autCount
+ autCount_eq_nat_card
+ autCount_pos
+ comp_toCopy_injective
+ comp_toEmbedding_injective
+ copyCount_eq_nat_card
+ copyCount_eq_unlabeledCopyCount_mul_autCount
+ embeddingCount
+ embeddingCount_eq_nat_card
+ embeddingCount_eq_unlabeledEmbeddingCount_mul_autCount
+ 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 : Nonempty G.Aut := ⟨Iso.refl⟩
+ instance [Finite V] : Finite G.Aut
+ 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
+ one_le_autCount
+ range_toSubgraph
+ toCopy_comp
+ toEmbedding_apply
+ toHom_comp
+ 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
++ apply_mem_verts_toSubgraph
++ equivOfToSubgraphEq
++ equivOfToSubgraphEq_apply
++ equivSigma
++ equivUnlabeledProdAut
++ fiberAut
++ fiberAut_spec
++ fiberEquivAut
++ fiberEquivAutOf
++ mem_range_of_toSubgraph_eq
++ toSubgraph_adj_iff
++ toSubgraph_comp
++ toSubgraph_comp_iso
++ verts_toSubgraph
- 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 9255371060
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: |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
|
This pull request has conflicts, please merge |
FordUniver
force-pushed
the
feat/simplegraph-aut
branch
from
May 25, 2026 07:10
9536bac to
de72aec
Compare
github-actions
Bot
removed
the
merge-conflict
Collaborator
Author
|
I am marking all PRs depending on the #38631 stack as draft for now until that prerequisite is (close to) merged. |
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/simplegraph-aut
branch
from
June 13, 2026 19:55
de72aec to
c811407
Compare
github-actions
Bot
removed
the
merge-conflict
FordUniver
force-pushed
the
feat/simplegraph-aut
branch
from
June 13, 2026 20:16
c811407 to
bfd864f
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, ...⟩`.
…or copies and embeddings Introduce the type `SimpleGraph.Aut G := G ≃g G` of graph automorphisms with the associated count `SimpleGraph.autCount G`. Develop the free precomposition action of `Aut G` on `Copy G H` / `Embedding G H` and prove the orbit-stabiliser identities at both the cardinal and equivalence levels: * `H.copyCount G = H.unlabeledCopyCount G * G.autCount` * `H.embeddingCount G = H.unlabeledEmbeddingCount G * G.autCount` The fiber-of-`toSubgraph` machinery (`fiberAut`, `fiberAut_spec`, `fiberEquivAut`, `fiberEquivAutOf`) is fully mirrored between `Copy` and `Embedding`, with Embedding's side built independently rather than delegating to Copy's, so induced notions stand on equal footing with the ordinary ones. Adds supporting `Copy.lean` / `InducedCopy.lean` utility lemmas that were extracted for the orbit-stabiliser proof: * `Copy.apply_eq_iff_eq` (simp injectivity iff) * `Copy.toHom_comp` / `Embedding.toCopy_comp` (composition functoriality) * `Copy.verts_toSubgraph`, `Embedding.verts_toSubgraph` * `Copy.toSubgraph_adj_iff`, `Embedding.toSubgraph_adj_iff` * `Copy.toSubgraph_comp`, `Embedding.toSubgraph_comp` * `Copy.apply_mem_verts_toSubgraph`, `Embedding.apply_mem_verts_toSubgraph` * `Iso.toCopy_toSubgraph` * `Copy.mem_range_of_toSubgraph_eq`, `Embedding.mem_range_of_toSubgraph_eq` * `Copy.equivOfToSubgraphEq` + `_apply`, `Embedding.equivOfToSubgraphEq` + `_apply` * `Copy.toEmbeddingOfIsInduced` + `_apply` (canonical promotion from copy to embedding when the image is induced). The labeled-↔-unlabeled projection pair (`toUnlabeledCopy` / `out` and their Embedding mirrors) lands in the prerequisite PR; this PR consumes them.
…all lemmas Remove docstrings on `Copy.toSubgraph_comp_iso`, `Copy.comp_toCopy_injective`, and their Embedding mirrors. The names (`toSubgraph_comp_iso`, `comp_toCopy_injective` / `comp_toEmbedding_injective`) and signatures are self-evident; the docstrings just restated them in prose. Other docstrings (`Aut`, `autCount`, the `fiber*` defs, the `equiv*` packagings, and the two `**Orbit-stabiliser**`-tagged main theorems) all add content over their names and stay.
….{verts_toSubgraph,toSubgraph_adj_iff}`
The four lemmas don't pass the `simpNF` linter: the `verts_toSubgraph`
pair is already discharged by simp via the `@[simps]`-generated
`Subgraph.map_verts` + `Subgraph.verts_top` + `Set.image_univ`, and the
`toSubgraph_adj_iff` LHS gets rewritten under `Subgraph.map_adj` /
`Copy.coe_toHom` before the iff can match. The statements are still
useful as named non-simp rewrites (the `adj_iff` pair carries genuine
injectivity content used in `Automorphism.lean`, and the `verts`
equation supports `mem_range_of_toSubgraph_eq`), so just drop the
attribute.
…iberAut_spec` Rebasing onto current master (Lean v4.31.0-rc2) tightened the module system: an exported theorem may only unfold definitions that are `@[expose]`d. The `fiberAut_spec` proofs reduce `(fiberAut …).toCopy v` to `equivOfToSubgraphEq h v` by definitional unfolding of the local `fiberAut`, which is no longer permitted across the export boundary. Mark both `Copy.fiberAut` and `Embedding.fiberAut` `@[expose]` and drive the proofs with `simp [fiberAut]` (semireducible `@[expose] def`s are not unfolded by `simp` automatically). No change to the API or to `Copy.lean`.
FordUniver
force-pushed
the
feat/simplegraph-aut
branch
from
July 12, 2026 02:21
bfd864f to
9255371
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 the type
Aut G := G ≃g Gof graph automorphisms and the corresponding countautCount G, then uses the orbit-stabiliser principle on bothCopy G HandEmbedding G Hto proveH.copyCount G = H.unlabeledCopyCount G * G.autCountandH.embeddingCount G = H.unlabeledEmbeddingCount G * G.autCount. In both, the labeled copies decompose as a disjoint union of fibers indexed by the corresponding unlabelled copies, with each fiber a torsor underAut G. The fiber-action machinery and the sigma decompositions are the substantive content; the two multiplicative identities are the corollaries.Co-authored-by: Malte Jackisch 45597826+MaltyBlanket@users.noreply.github.com
The main achievement is to allow the user to freely convert between
{copy,embedding}Countandunlabeled{copy,embedding}CountthroughautCount. Sits on top of theCopy/InducedCopyrefactor-feat stack (final step #38631), plus a small prerequisite (#39571) extracting the standaloneQuot.mk/Quot.out-style toolage between labeled and unlabeled copies.Diff for the changes just in this PR over its predecessor: link