From 64e84746221459246a0cf71dfe88757d2fedf723 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Sat, 13 Jan 2024 07:57:05 +0800 Subject: [PATCH 1/2] feat: transfer of graph properties over maps --- Mathlib/Combinatorics/SimpleGraph/Clique.lean | 5 ++++ Mathlib/Combinatorics/SimpleGraph/Maps.lean | 29 ++++++++++++++++--- 2 files changed, 30 insertions(+), 4 deletions(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean index 71695b5bb4dc8..5e87f93931e47 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Clique.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Clique.lean @@ -281,6 +281,11 @@ theorem CliqueFree.anti (h : G ≤ H) : H.CliqueFree n → G.CliqueFree n := forall_imp fun _ ↦ mt <| IsNClique.mono h #align simple_graph.clique_free.anti SimpleGraph.CliqueFree.anti +/-- If a graph is cliquefree, any graph that embeds into it is also cliquefree. -/ +theorem CliqueFree.map {H : SimpleGraph β} (f : H ↪g G) : G.CliqueFree n → H.CliqueFree n := by + intro h; contrapose h + exact not_cliqueFree_of_top_embedding <| f.comp (topEmbeddingOfNotCliqueFree h) + /-- See `SimpleGraph.cliqueFree_of_chromaticNumber_lt` for a tighter bound. -/ theorem cliqueFree_of_card_lt [Fintype α] (hc : card α < n) : G.CliqueFree n := by by_contra h diff --git a/Mathlib/Combinatorics/SimpleGraph/Maps.lean b/Mathlib/Combinatorics/SimpleGraph/Maps.lean index db9a64a83331f..332789e87648b 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Maps.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Maps.lean @@ -578,11 +578,16 @@ def mapNeighborSet (v : V) : G.neighborSet v ≃ G'.neighborSet (f v) right_inv w := by simp #align simple_graph.iso.map_neighbor_set SimpleGraph.Iso.mapNeighborSet -theorem card_eq_of_iso [Fintype V] [Fintype W] (f : G ≃g G') : Fintype.card V = Fintype.card W := by +theorem card_eq [Fintype V] [Fintype W] : Fintype.card V = Fintype.card W := by rw [← Fintype.ofEquiv_card f.toEquiv] - -- porting note: need to help it to find the typeclass instances from the target expression - apply @Fintype.card_congr' _ _ (_) (_) rfl -#align simple_graph.iso.card_eq_of_iso SimpleGraph.Iso.card_eq_of_iso + convert rfl +#align simple_graph.iso.card_eq_of_iso SimpleGraph.Iso.card_eq + +theorem card_edgeFinset_eq [Fintype G.edgeSet] [Fintype G'.edgeSet] : + G.edgeFinset.card = G'.edgeFinset.card := by + apply Finset.card_eq_of_equiv + simp only [Set.mem_toFinset] + exact f.mapEdgeSet /-- Given a bijection, there is an embedding from the comapped graph into the original graph. -/ @@ -651,4 +656,20 @@ def induceUnivIso (G : SimpleGraph V) : G.induce Set.univ ≃g G where map_rel_iff' := by simp only [Equiv.Set.univ, Equiv.coe_fn_mk, comap_adj, Embedding.coe_subtype, Subtype.forall, Set.mem_univ, forall_true_left, implies_true] +section Finite + +variable [Fintype V] {n : ℕ} + +/-- Given a graph over a finite vertex type `V` and a proof `hc` that `Fintype.card V = n`, +`G.overFin n` is an isomorphic (as shown in `overFinIso`) graph over `Fin n`. -/ +def overFin (hc : Fintype.card V = n) : SimpleGraph (Fin n) where + Adj x y := G.Adj ((Fintype.equivFinOfCardEq hc).symm x) ((Fintype.equivFinOfCardEq hc).symm y) + symm x y := by simp_rw [adj_comm, imp_self] + +/-- The isomorphism between `G` and `G.overFin hc`. -/ +noncomputable def overFinIso (hc : Fintype.card V = n) : G ≃g G.overFin hc := by + use Fintype.equivFinOfCardEq hc; simp [overFin] + +end Finite + end SimpleGraph From ecccbe5c5c6239370f6a80aa9a4d02f8ac04ffb0 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Tue, 16 Jan 2024 21:01:20 +0800 Subject: [PATCH 2/2] `comap` --- Mathlib/Combinatorics/SimpleGraph/Clique.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/Combinatorics/SimpleGraph/Clique.lean b/Mathlib/Combinatorics/SimpleGraph/Clique.lean index f6779992c6b13..d2885c05fcef6 100644 --- a/Mathlib/Combinatorics/SimpleGraph/Clique.lean +++ b/Mathlib/Combinatorics/SimpleGraph/Clique.lean @@ -282,7 +282,7 @@ theorem CliqueFree.anti (h : G ≤ H) : H.CliqueFree n → G.CliqueFree n := #align simple_graph.clique_free.anti SimpleGraph.CliqueFree.anti /-- If a graph is cliquefree, any graph that embeds into it is also cliquefree. -/ -theorem CliqueFree.map {H : SimpleGraph β} (f : H ↪g G) : G.CliqueFree n → H.CliqueFree n := by +theorem CliqueFree.comap {H : SimpleGraph β} (f : H ↪g G) : G.CliqueFree n → H.CliqueFree n := by intro h; contrapose h exact not_cliqueFree_of_top_embedding <| f.comp (topEmbeddingOfNotCliqueFree h)