Skip to content

feat(Combinatorics/SimpleGraph): canonical projection and representative between labeled and unlabeled copies #32

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
FordUniver wants to merge 1 commit into from
Closed

feat(Combinatorics/SimpleGraph): canonical projection and representative between labeled and unlabeled copies #32

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
25 changes: 19 additions & 6 deletions Mathlib/Combinatorics/SimpleGraph/Copy.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -438,6 +438,23 @@ abbrev UnlabeledCopy (G : SimpleGraph V) (H : SimpleGraph W) : Type _ :=

instance [Finite W] : Finite (G.UnlabeledCopy H) := Subtype.finite

/-- The canonical map from a labeled copy to its unlabeled image. -/
@[expose] def Copy.toUnlabeledCopy (f : Copy G H) : G.UnlabeledCopy H :=
⟨f.toSubgraph, ⟨f.isoToSubgraph⟩⟩

@[simp] lemma Copy.toUnlabeledCopy_val (f : Copy G H) : f.toUnlabeledCopy.val = f.toSubgraph := rfl

lemma UnlabeledCopy.exists_toSubgraph_eq_val (S : G.UnlabeledCopy H) :
∃ f : Copy G H, f.toSubgraph = S.val :=
Set.mem_range.mp (Copy.range_toSubgraph ▸ S.property)

/-- A noncomputable representative labeled copy of an unlabeled copy. -/
noncomputable def UnlabeledCopy.out (S : G.UnlabeledCopy H) : Copy G H :=
S.exists_toSubgraph_eq_val.choose

@[simp] lemma UnlabeledCopy.toSubgraph_out (S : G.UnlabeledCopy H) : S.out.toSubgraph = S.val :=
S.exists_toSubgraph_eq_val.choose_spec

/-- `H.unlabeledCopyCount G` is the number of `SimpleGraph.Subgraph`s of `H` isomorphic to `G`. See
`SimpleGraph.copyCount` for the number of labeled copies. -/
noncomputable def unlabeledCopyCount (H : SimpleGraph W) (G : SimpleGraph V) : ℕ :=
Expand All @@ -458,12 +475,8 @@ lemma unlabeledCopyCount_eq_nat_card (H : SimpleGraph W) (G : SimpleGraph V) :
lemma unlabeledCopyCount_le_copyCount [Finite V] [Finite W] :
H.unlabeledCopyCount G ≤ H.copyCount G := by
rw [unlabeledCopyCount, copyCount]
apply Nat.card_le_card_of_surjective
(fun c : Copy G H ↦ (⟨c.toSubgraph, ⟨c.isoToSubgraph⟩⟩ : G.UnlabeledCopy H))
rintro ⟨H', hG'⟩
obtain ⟨c, hc⟩ : ∃ c, Copy.toSubgraph c = H' := by
rwa [← Set.mem_range, Copy.range_toSubgraph]
exact ⟨c, Subtype.ext hc⟩
exact Nat.card_le_card_of_surjective Copy.toUnlabeledCopy
fun S ↦ ⟨S.out, Subtype.ext S.toSubgraph_out⟩

instance uniqueUnlabeledCopyBot [Finite W] (H : SimpleGraph W) :
Unique ((⊥ : SimpleGraph W).UnlabeledCopy H) where
Expand Down
28 changes: 21 additions & 7 deletions Mathlib/Combinatorics/SimpleGraph/InducedCopy.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -274,6 +274,25 @@ abbrev UnlabeledEmbedding (G : SimpleGraph V) (H : SimpleGraph W) : Type _ :=

instance [Finite W] : Finite (G.UnlabeledEmbedding H) := Subtype.finite

/-- The canonical map from a labeled embedding to its unlabeled induced image. -/
@[expose] def Embedding.toUnlabeledEmbedding (f : Embedding G H) : G.UnlabeledEmbedding H :=
⟨f.toSubgraph, f.toSubgraph_isInduced, ⟨f.toCopy.isoToSubgraph⟩⟩

@[simp] lemma Embedding.toUnlabeledEmbedding_val (f : Embedding G H) :
f.toUnlabeledEmbedding.val = f.toSubgraph := rfl

lemma UnlabeledEmbedding.exists_toSubgraph_eq_val (S : G.UnlabeledEmbedding H) :
∃ f : Embedding G H, f.toSubgraph = S.val :=
Set.mem_range.mp (Embedding.range_toSubgraph ▸ S.property)

/-- A noncomputable representative labeled embedding of an unlabeled induced copy. -/
noncomputable def UnlabeledEmbedding.out (S : G.UnlabeledEmbedding H) : Embedding G H :=
S.exists_toSubgraph_eq_val.choose

@[simp] lemma UnlabeledEmbedding.toSubgraph_out (S : G.UnlabeledEmbedding H) :
S.out.toSubgraph = S.val :=
S.exists_toSubgraph_eq_val.choose_spec

/-- `H.unlabeledEmbeddingCount G` is the number of induced `SimpleGraph.Subgraph`s of `H`
isomorphic to `G`.
See `SimpleGraph.embeddingCount` for the number of induced labeled copies. -/
Expand All @@ -298,13 +317,8 @@ unlabeled ones. -/
lemma unlabeledEmbeddingCount_le_embeddingCount [Finite V] [Finite W] :
H.unlabeledEmbeddingCount G ≤ H.embeddingCount G := by
rw [unlabeledEmbeddingCount, embeddingCount]
apply Nat.card_le_card_of_surjective
(fun f : Embedding G H ↦ (⟨Embedding.toSubgraph f, f.toSubgraph_isInduced,
⟨f.toCopy.isoToSubgraph⟩⟩ : G.UnlabeledEmbedding H))
rintro ⟨H', hInd, ⟨e⟩⟩
obtain ⟨f, hf⟩ : ∃ f : Embedding G H, Embedding.toSubgraph f = H' := by
rw [← Set.mem_range, Embedding.range_toSubgraph]; exact ⟨hInd, ⟨e⟩⟩
exact ⟨f, Subtype.ext hf⟩
exact Nat.card_le_card_of_surjective Embedding.toUnlabeledEmbedding
fun S ↦ ⟨S.out, Subtype.ext S.toSubgraph_out⟩

private instance [IsEmpty V] : Nonempty (G.UnlabeledEmbedding H) :=
let ⟨H', hInd, ⟨e⟩⟩ := (IsIndContained.of_isEmpty (G := G) (H := H)).exists_iso_subgraph
Expand Down
Loading