feat(Combinatorics/SimpleGraph/InducedCopy): add Copy.inducedShape#38
Closed
FordUniver wants to merge 1 commit into
Closed
feat(Combinatorics/SimpleGraph/InducedCopy): add Copy.inducedShape#38FordUniver wants to merge 1 commit into
FordUniver wants to merge 1 commit into
Conversation
For a copy `f : Copy G H`, the *induced shape* of `f` is the pullback
`H.comap f.toEmbedding`: a graph on `V` whose adjacency records the induced
adjacency of `H` restricted to the image of `f`.
Adds:
* `Copy.inducedShape`, `Copy.inducedShape_adj`, `Copy.le_inducedShape`.
* `Copy.toEmbeddingOfInducedShapeEq`: promotes a copy whose induced shape
equals a prescribed supergraph `G' ≥ G` to an embedding `G' ↪g H`.
* `Copy.fiberInducedShapeEquiv`: the per-supergraph bijection
`{f : Copy G H // f.inducedShape = G'} ≃ Embedding G' H`.
This material is the load-bearing fiber decomposition consumed by the
Möbius inversion `copyCount_eq_sum_embeddingCount` /
`embeddingCount_eq_sum_signed_copyCount` (downstream PR).
`Copy.toEmbeddingOfInducedShapeEq` is `@[expose]` for the same reason as
`Copy.toEmbeddingOfIsInduced`: its `_apply` simp lemma needs the body to
unfold across modules.
FordUniver
force-pushed
the
feat/copy-induced-shape
branch
from
May 27, 2026 15:34
66510d0 to
67bb8d3
Compare
FordUniver
changed the title
FordUniver
changed the base branch from
feat/ind-copy-count
to
feat/simplegraph-aut
May 27, 2026 15:37
Owner
Author
|
Rolled into the Möbius PR — the inducedShape API doesn't make sense standalone without the Möbius bijection that consumes it. |
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.
Adds
Copy.inducedShape, the pullbackH.comap f.toEmbeddingrecording the adjacency of the host graph at the image of a copy, together with the per-fiber bijectionCopy.fiberInducedShapeEquiv: forG' ≥ G, copies ofGinHwith induced shapeG'are canonically embeddingsG' ↪g H. The companion promotion lemmaCopy.toEmbeddingOfInducedShapeEqis the supergraph variant of the existingCopy.toEmbeddingOfIsInducedin this file, takingCopy G HtoEmbedding G' Hrather than toEmbedding G H.Co-authored-by: Malte Jackisch 45597826+MaltyBlanket@users.noreply.github.com
Came up while writing a Möbius inversion between copy counts and induced copy counts in a downstream PR. The fiber decomposition is the load-bearing structural fact: every copy uniquely decomposes as a choice of induced shape (a supergraph of the guest on the same vertex type) together with an embedding of that shape into the host.
Aut,autCount, and orbit-stabiliser for copies and embeddings leanprover-community/mathlib4#39573Diff for the changes just in this PR over its predecessor: link