Documentation

Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Construct a tripartite graph from its triangles #

This file contains the construction of a simple graph on α ⊕ β ⊕ γ from a list of triangles (a, b, c) (with a in the first component, b in the second, c in the third).

We call

The two important properties of this construction are:

This construction shows up unrelatedly twice in the theory of Roth numbers:

theorem SimpleGraph.TripartiteFromTriangles.rel_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) :
∀ (a a_1 : α β γ), SimpleGraph.TripartiteFromTriangles.Rel t a a_1 (∃ (a_2 : α) (b : β) (c : γ), (a_2, b, c) t a = Sum3.in₀ a_2 a_1 = Sum3.in₁ b) (∃ (a_2 : α) (b : β) (c : γ), (a_2, b, c) t a = Sum3.in₁ b a_1 = Sum3.in₀ a_2) (∃ (a_2 : α) (b : β) (c : γ), (a_2, b, c) t a = Sum3.in₀ a_2 a_1 = Sum3.in₂ c) (∃ (a_2 : α) (b : β) (c : γ), (a_2, b, c) t a = Sum3.in₂ c a_1 = Sum3.in₀ a_2) (∃ (a_2 : α) (b : β) (c : γ), (a_2, b, c) t a = Sum3.in₁ b a_1 = Sum3.in₂ c) ∃ (a_2 : α) (b : β) (c : γ), (a_2, b, c) t a = Sum3.in₂ c a_1 = Sum3.in₁ b
inductive SimpleGraph.TripartiteFromTriangles.Rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) :
α β γα β γProp

The underlying relation of the tripartite-from-triangles graph.

Two vertices are related iff there exists a triangle index containing them both.

Instances For
    theorem SimpleGraph.TripartiteFromTriangles.rel_irrefl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} (x : α β γ) :
    def SimpleGraph.TripartiteFromTriangles.graph {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) :
    SimpleGraph (α β γ)

    The tripartite-from-triangles graph. Two vertices are related iff there exists a triangle index containing them both.

    Equations
    Instances For
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.not_in₀₀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {a' : α} :
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.not_in₁₁ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {b' : β} :
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.not_in₂₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {c : γ} {c' : γ} :
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β} :
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ∃ (c : γ), (a, b, c) t
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β} :
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₀ a) ∃ (c : γ), (a, b, c) t
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ} :
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ∃ (b : β), (a, b, c) t
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ} :
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₀ a) ∃ (b : β), (a, b, c) t
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ} :
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c) ∃ (a : α), (a, b, c) t
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ} :
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₁ b) ∃ (a : α), (a, b, c) t
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β} :
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) xt, x.1 = a x.2.1 = b
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β} :
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₀ a) xt, x.2.1 = b x.1 = a
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ} :
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) xt, x.1 = a x.2.2 = c
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ} :
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₀ a) xt, x.2.2 = c x.1 = a
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ} :
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c) xt, x.2.1 = b x.2.2 = c
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ} :
      (SimpleGraph.TripartiteFromTriangles.graph t).Adj (Sum3.in₂ c) (Sum3.in₁ b) xt, x.2.2 = c x.2.1 = b
      class SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) :

      Predicate on the triangle indices for the explicit triangles to be edge-disjoint.

      • inj₀ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ ⦃a' : α⦄, (a, b, c) t(a', b, c) ta = a'
      • inj₁ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ ⦃b' : β⦄, (a, b, c) t(a, b', c) tb = b'
      • inj₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c c' : γ⦄, (a, b, c) t(a, b, c') tc = c'
      Instances
        theorem SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [self : SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] ⦃a : α ⦃b : β ⦃c : γ ⦃a' : α :
        (a, b, c) t(a', b, c) ta = a'
        theorem SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₁ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [self : SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] ⦃a : α ⦃b : β ⦃c : γ ⦃b' : β :
        (a, b, c) t(a, b', c) tb = b'
        theorem SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [self : SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] ⦃a : α ⦃b : β ⦃c : γ ⦃c' : γ :
        (a, b, c) t(a, b, c') tc = c'
        class SimpleGraph.TripartiteFromTriangles.NoAccidental {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) :

        Predicate on the triangle indices for there to be no accidental triangle.

        Note that we cheat a bit, since the exact translation of this informal description would have (a', b', c') ∈ t as a conclusion rather than a = a' ∨ b = b' ∨ c = c'. Those conditions are equivalent when the explicit triangles are edge-disjoint (which is the case we care about).

        • eq_or_eq_or_eq : ∀ ⦃a a' : α⦄ ⦃b b' : β⦄ ⦃c c' : γ⦄, (a', b, c) t(a, b', c) t(a, b, c') ta = a' b = b' c = c'
        Instances
          theorem SimpleGraph.TripartiteFromTriangles.NoAccidental.eq_or_eq_or_eq {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [self : SimpleGraph.TripartiteFromTriangles.NoAccidental t] ⦃a : α ⦃a' : α ⦃b : β ⦃b' : β ⦃c : γ ⦃c' : γ :
          (a', b, c) t(a, b', c) t(a, b, c') ta = a' b = b' c = c'
          Equations
          theorem SimpleGraph.TripartiteFromTriangles.graph_triple {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] ⦃x : α β γ ⦃y : α β γ ⦃z : α β γ :

          This lemma reorders the elements of a triangle in the tripartite graph. It turns a triangle {x, y, z} into a triangle {a, b, c} where a : α , b : β, c : γ.

          @[simp]
          theorem SimpleGraph.TripartiteFromTriangles.toTriangle_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [DecidableEq γ] (x : α × β × γ) :
          SimpleGraph.TripartiteFromTriangles.toTriangle x = {Sum3.in₀ x.1, Sum3.in₁ x.2.1, Sum3.in₂ x.2.2}
          def SimpleGraph.TripartiteFromTriangles.toTriangle {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [DecidableEq γ] :
          α × β × γ Finset (α β γ)

          The map that turns a triangle index into an explicit triangle.

          Equations
          Instances For
            theorem SimpleGraph.TripartiteFromTriangles.toTriangle_is3Clique {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {x : α × β × γ} [DecidableEq α] [DecidableEq β] [DecidableEq γ] (hx : x t) :
            (SimpleGraph.TripartiteFromTriangles.graph t).IsNClique 3 (SimpleGraph.TripartiteFromTriangles.toTriangle x)
            theorem SimpleGraph.TripartiteFromTriangles.exists_mem_toTriangle {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] {x : α β γ} {y : α β γ} (hxy : (SimpleGraph.TripartiteFromTriangles.graph t).Adj x y) :
            zt, x SimpleGraph.TripartiteFromTriangles.toTriangle z y SimpleGraph.TripartiteFromTriangles.toTriangle z
            theorem SimpleGraph.TripartiteFromTriangles.is3Clique_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] {s : Finset (α β γ)} :
            (SimpleGraph.TripartiteFromTriangles.graph t).IsNClique 3 s xt, SimpleGraph.TripartiteFromTriangles.toTriangle x = s
            theorem SimpleGraph.TripartiteFromTriangles.toTriangle_surjOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] :
            Set.SurjOn (⇑SimpleGraph.TripartiteFromTriangles.toTriangle) (↑t) ((SimpleGraph.TripartiteFromTriangles.graph t).cliqueSet 3)
            theorem SimpleGraph.TripartiteFromTriangles.map_toTriangle_disjoint {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] :
            (↑(Finset.map SimpleGraph.TripartiteFromTriangles.toTriangle t)).Pairwise fun (x y : Finset (α β γ)) => (x y).Subsingleton
            theorem SimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] :
            (SimpleGraph.TripartiteFromTriangles.graph t).cliqueSet 3 = SimpleGraph.TripartiteFromTriangles.toTriangle '' t
            theorem SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [Fintype α] [Fintype β] [Fintype γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] :
            (SimpleGraph.TripartiteFromTriangles.graph t).cliqueFinset 3 = Finset.image (⇑SimpleGraph.TripartiteFromTriangles.toTriangle) t
            theorem SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [Fintype α] [Fintype β] [Fintype γ] [SimpleGraph.TripartiteFromTriangles.NoAccidental t] :
            (SimpleGraph.TripartiteFromTriangles.graph t).cliqueFinset 3 = Finset.map SimpleGraph.TripartiteFromTriangles.toTriangle t
            @[simp]
            theorem SimpleGraph.TripartiteFromTriangles.farFromTriangleFree {α : Type u_1} {β : Type u_2} {γ : Type u_3} {𝕜 : Type u_4} [LinearOrderedField 𝕜] (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [Fintype α] [Fintype β] [Fintype γ] [SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] {ε : 𝕜} (ht : ε * ((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) t.card) :