feat(Combinatorics/SimpleGraph/Automorphism): Aut, autCount, and orbit-stabiliser for copies and embeddings#25
Closed
FordUniver wants to merge 1 commit into
Closed
Conversation
FordUniver
changed the title
Aut and autCount
FordUniver
force-pushed
the
feat/simplegraph-aut
branch
from
May 18, 2026 09:45
8fb9896 to
9e24568
Compare
FordUniver
force-pushed
the
feat/ind-copy-count
branch
from
May 18, 2026 12:22
e238d00 to
8d07210
Compare
FordUniver
force-pushed
the
feat/simplegraph-aut
branch
11 times, most recently
from
May 18, 2026 17:40
41d8fe1 to
791718b
Compare
1 task
…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.
FordUniver
force-pushed
the
feat/simplegraph-aut
branch
from
May 19, 2026 11:17
c74f5c5 to
af93dec
Compare
FordUniver
changed the base branch from
feat/ind-copy-count
to
feat/copy-toUnlabeled-out
May 19, 2026 11:17
FordUniver
changed the title
Aut and autCountAut, autCount, and orbit-stabiliser for copies and embeddings
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.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 leanprover-community#38631), plus a small prerequisite (leanprover-community#38631) extracting the standaloneQuot.mk/Quot.out-style toolage between labeled and unlabeled copies.UnlabeledEmbedding,unlabeledEmbeddingCountandembeddingCountleanprover-community/mathlib4#38631Diff for the changes just in this PR over its predecessor: link