feat(combinatorics/simple_graph): Construct a tripartite graph from its triangles #19202
Conversation
YaelDillies
added
awaiting-review
github-actions
bot
added
the
modifies-synchronized-file
kim-em
added
too-late
| @[simp] lemma locally_linear_comap {G : simple_graph β} {e : α ≃ β} : | ||
| (G.comap e).locally_linear ↔ G.locally_linear := | ||
| begin | ||
| refine ⟨λ h, _, _⟩, | ||
| { rw [←comap_map_eq e.symm.to_embedding G, comap_symm, map_symm], | ||
| exact h.map _ }, | ||
| { rw [←equiv.coe_to_embedding, ←map_symm], | ||
| exact locally_linear.map _ } | ||
| end |
There was a problem hiding this comment.
Is one direction of this true for embeddings?
|
|
||
| instance : decidable G.edge_disjoint_triangles := | ||
| decidable_of_iff ((G.clique_finset 3 : set (finset α)).pairwise $ λ x y, (x ∩ y).card ≤ 1) $ | ||
| by simpa only [coe_clique_finset, edge_disjoint_triangles, finset.card_le_one, ←coe_inter] |
There was a problem hiding this comment.
This might be worth extracting as a lemma.
|
|
||
| /-- The underlying relation of the tripartite-from-triangles graph. Two vertices are related iff | ||
| there exists a triangle index containing them both. -/ | ||
| @[mk_iff] inductive rel (t : finset (α × β × γ)) : α ⊕ β ⊕ γ → α ⊕ β ⊕ γ → Prop |
There was a problem hiding this comment.
α × β × γ feels like a rather strange representation of a triangle, as it isn't order-invariant. Would it be correct to use "ordered triangles" in the docstring; and do you actually end up needing this ordering?
There was a problem hiding this comment.
Those are not the triangles but the triangle indices. The triangle index (a, b, c) corresponds to the triangle {in₀ a, in₁ b, in₂ c} (which is unordered, even though the in₀, in₁, in₂ make it morally ordered). I definitely need the order in my applications, since α, β, γ won't even be the same.
| @[simp] lemma in₀₁_iff : (graph t).adj (in₀ a) (in₁ b) ↔ ∃ c, (a, b, c) ∈ t := | ||
| ⟨by { rintro ⟨⟩, exact ⟨_, ‹_›⟩ }, λ ⟨_, h⟩, in₀₁ h⟩ | ||
| @[simp] lemma in₁₀_iff : (graph t).adj (in₁ b) (in₀ a) ↔ ∃ c, (a, b, c) ∈ t := | ||
| ⟨by { rintro ⟨⟩, exact ⟨_, ‹_›⟩ }, λ ⟨_, h⟩, in₁₀ h⟩ | ||
| @[simp] lemma in₀₂_iff : (graph t).adj (in₀ a) (in₂ c) ↔ ∃ b, (a, b, c) ∈ t := | ||
| ⟨by { rintro ⟨⟩, exact ⟨_, ‹_›⟩ }, λ ⟨_, h⟩, in₀₂ h⟩ | ||
| @[simp] lemma in₂₀_iff : (graph t).adj (in₂ c) (in₀ a) ↔ ∃ b, (a, b, c) ∈ t := | ||
| ⟨by { rintro ⟨⟩, exact ⟨_, ‹_›⟩ }, λ ⟨_, h⟩, in₂₀ h⟩ | ||
| @[simp] lemma in₁₂_iff : (graph t).adj (in₁ b) (in₂ c) ↔ ∃ a, (a, b, c) ∈ t := | ||
| ⟨by { rintro ⟨⟩, exact ⟨_, ‹_›⟩ }, λ ⟨_, h⟩, in₁₂ h⟩ | ||
| @[simp] lemma in₂₁_iff : (graph t).adj (in₂ c) (in₁ b) ↔ ∃ a, (a, b, c) ∈ t := | ||
| ⟨by { rintro ⟨⟩, exact ⟨_, ‹_›⟩ }, λ ⟨_, h⟩, in₂₁ h⟩ |
There was a problem hiding this comment.
Is it definitely not worth generalizing to n-cliques (and sigma) so that you don't need to repeat things 3 times?
There was a problem hiding this comment.
I have exactly three applications in mind for this API, and they all use triangles (hell, even locally linear graphs are only about triangles). The point of this API is to repeat things 3 times only once (understand, not in the applications). In contrast, using sigma will result in an overhead in the applications.
mathlib-dependent-issues-bot
removed
the
blocked-by-other-PR
|
This PR/issue depends on:
|
|
Ported to LeanCamCombi |
Both the lower bound of the Ruzsa-Szemerédi problem and the proof of the corners theorem define an auxiliary tripartite graph by specifying its triangles and showing that there are no more.
This PR provides the boilerplate for this construction. It greatly simplifies both proofs.
Co-authored-by: Bhavik Mehta [email protected]