feat(Combinatorics/SimpleGraph): canonical projection and representative between labeled and unlabeled copies#32
Closed
FordUniver wants to merge 1 commit into
Closed
Conversation
…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, ...⟩`.
1 task
FordUniver
changed the title
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.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,unlabeledEmbeddingCountandembeddingCountleanprover-community/mathlib4#38631Diff for the changes just in this PR over its predecessor: link