Skip to content
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

[Merged by Bors] - feat: transfer of graph properties over maps #9708

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - feat: transfer of graph properties over maps #9708

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
64e8474
feat: transfer of graph properties over maps
Parcly-Taxel Jan 12, 2024
e6f01b8
Merge branch 'master' into graphtransfer
Parcly-Taxel Jan 16, 2024
ecccbe5
`comap`
Parcly-Taxel Jan 16, 2024
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
5 changes: 5 additions & 0 deletions Mathlib/Combinatorics/SimpleGraph/Clique.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.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)

/-- 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
Expand Down
29 changes: 25 additions & 4 deletions Mathlib/Combinatorics/SimpleGraph/Maps.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/
Expand Down Expand Up @@ -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