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:

source
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
    source
    theorem SimpleGraph.TripartiteFromTriangles.rel_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) (a✝ a✝¹ : α ⊕ β ⊕ γ) :
    Rel t a✝ a✝¹ ↔ (∃ (a : α) (b : β) (c : γ), (a, b, c) ∈ t ∧ a✝ = Sum3.in₀ a ∧ a✝¹ = Sum3.in₁ b) ∨ (∃ (a : α) (b : β) (c : γ), (a, b, c) ∈ t ∧ a✝ = Sum3.in₁ b ∧ a✝¹ = Sum3.in₀ a) ∨ (∃ (a : α) (b : β) (c : γ), (a, b, c) ∈ t ∧ a✝ = Sum3.in₀ a ∧ a✝¹ = Sum3.in₂ c) ∨ (∃ (a : α) (b : β) (c : γ), (a, b, c) ∈ t ∧ a✝ = Sum3.in₂ c ∧ a✝¹ = Sum3.in₀ a) ∨ (∃ (a : α) (b : β) (c : γ), (a, b, c) ∈ t ∧ a✝ = Sum3.in₁ b ∧ a✝¹ = Sum3.in₂ c) ∨ ∃ (a : α) (b : β) (c : γ), (a, b, c) ∈ t ∧ a✝ = Sum3.in₂ c ∧ a✝¹ = Sum3.in₁ b
    source
    instance SimpleGraph.TripartiteFromTriangles.rel_irrefl {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} :
    Std.Irrefl (Rel t)
    source
    instance SimpleGraph.TripartiteFromTriangles.rel_symm {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} :
    Std.Symm (Rel t)
    source
    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
      source
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.not_in₀₀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a a' : α} :
      ¬(graph t).Adj (Sum3.in₀ a) (Sum3.in₀ a')
      source
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.not_in₁₁ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b b' : β} :
      ¬(graph t).Adj (Sum3.in₁ b) (Sum3.in₁ b')
      source
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.not_in₂₂ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {c c' : γ} :
      ¬(graph t).Adj (Sum3.in₂ c) (Sum3.in₂ c')
      source
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β} :
      (graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ↔ ∃ (c : γ), (a, b, c) ∈ t
      source
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β} :
      (graph t).Adj (Sum3.in₁ b) (Sum3.in₀ a) ↔ ∃ (c : γ), (a, b, c) ∈ t
      source
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ} :
      (graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ↔ ∃ (b : β), (a, b, c) ∈ t
      source
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ} :
      (graph t).Adj (Sum3.in₂ c) (Sum3.in₀ a) ↔ ∃ (b : β), (a, b, c) ∈ t
      source
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ} :
      (graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c) ↔ ∃ (a : α), (a, b, c) ∈ t
      source
      @[simp]
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ} :
      (graph t).Adj (Sum3.in₂ c) (Sum3.in₁ b) ↔ ∃ (a : α), (a, b, c) ∈ t
      source
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₀₁_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β} :
      (graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ↔ ∃ x ∈ t, x.1 = a ∧ x.2.1 = b
      source
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₁₀_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {b : β} :
      (graph t).Adj (Sum3.in₁ b) (Sum3.in₀ a) ↔ ∃ x ∈ t, x.2.1 = b ∧ x.1 = a
      source
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₀₂_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ} :
      (graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ↔ ∃ x ∈ t, x.1 = a ∧ x.2.2 = c
      source
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₂₀_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {a : α} {c : γ} :
      (graph t).Adj (Sum3.in₂ c) (Sum3.in₀ a) ↔ ∃ x ∈ t, x.2.2 = c ∧ x.1 = a
      source
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₁₂_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ} :
      (graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c) ↔ ∃ x ∈ t, x.2.1 = b ∧ x.2.2 = c
      source
      theorem SimpleGraph.TripartiteFromTriangles.Graph.in₂₁_iff' {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {b : β} {c : γ} :
      (graph t).Adj (Sum3.in₂ c) (Sum3.in₁ b) ↔ ∃ x ∈ t, x.2.2 = c ∧ x.2.1 = b
      source
      class SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) :
      Prop

      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) ∈ t → a = a'
      • inj₁ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ ⦃b' : β⦄ : (a, b, c) ∈ t → (a, b', c) ∈ t → b = b'
      • inj₂ ⦃a : α⦄ ⦃b : β⦄ ⦃c c' : γ⦄ : (a, b, c) ∈ t → (a, b, c') ∈ t → c = c'
      Instances
        source
        class SimpleGraph.TripartiteFromTriangles.NoAccidental {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) :
        Prop

        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') ∈ t → a = a' ∨ b = b' ∨ c = c'
        Instances
          source
          @[instance_reducible]
          instance SimpleGraph.TripartiteFromTriangles.graph.instDecidableRelAdj {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] :
          DecidableRel (graph t).Adj
          Equations
          source
          theorem SimpleGraph.TripartiteFromTriangles.graph_triple {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] ⦃x y z : α ⊕ β ⊕ γ⦄ :
          (graph t).Adj x y → (graph t).Adj x z → (graph t).Adj y z → ∃ (a : α) (b : β) (c : γ), {Sum3.in₀ a, Sum3.in₁ b, Sum3.in₂ c} = {x, y, z} ∧ (graph t).Adj (Sum3.in₀ a) (Sum3.in₁ b) ∧ (graph t).Adj (Sum3.in₀ a) (Sum3.in₂ c) ∧ (graph t).Adj (Sum3.in₁ b) (Sum3.in₂ c)

          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 : γ.

          source
          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
            source
            @[simp]
            theorem SimpleGraph.TripartiteFromTriangles.toTriangle_apply {α : Type u_1} {β : Type u_2} {γ : Type u_3} [DecidableEq α] [DecidableEq β] [DecidableEq γ] (x : α × β × γ) :
            toTriangle x = {Sum3.in₀ x.1, Sum3.in₁ x.2.1, Sum3.in₂ x.2.2}
            source
            theorem SimpleGraph.TripartiteFromTriangles.toTriangle_is3Clique {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} {x : α × β × γ} [DecidableEq α] [DecidableEq β] [DecidableEq γ] (hx : x ∈ t) :
            (graph t).IsNClique 3 (toTriangle x)
            source
            theorem SimpleGraph.TripartiteFromTriangles.exists_mem_toTriangle {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] {x y : α ⊕ β ⊕ γ} (hxy : (graph t).Adj x y) :
            ∃ z ∈ t, x ∈ toTriangle z ∧ y ∈ toTriangle z
            source
            theorem SimpleGraph.TripartiteFromTriangles.is3Clique_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] [NoAccidental t] {s : Finset (α ⊕ β ⊕ γ)} :
            (graph t).IsNClique 3 s ↔ ∃ x ∈ t, toTriangle x = s
            source
            theorem SimpleGraph.TripartiteFromTriangles.toTriangle_surjOn {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} [DecidableEq α] [DecidableEq β] [DecidableEq γ] [NoAccidental t] :
            Set.SurjOn (⇑toTriangle) (↑t) ((graph t).cliqueSet 3)
            source
            theorem SimpleGraph.TripartiteFromTriangles.map_toTriangle_disjoint {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [ExplicitDisjoint t] :
            (↑(Finset.map toTriangle t)).Pairwise fun (x y : Finset (α ⊕ β ⊕ γ)) => (↑x ∩ ↑y).Subsingleton
            source
            theorem SimpleGraph.TripartiteFromTriangles.cliqueSet_eq_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [NoAccidental t] :
            (graph t).cliqueSet 3 = ⇑toTriangle '' ↑t
            source
            theorem SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_image {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [Fintype α] [Fintype β] [Fintype γ] [NoAccidental t] :
            (graph t).cliqueFinset 3 = Finset.image (⇑toTriangle) t
            source
            theorem SimpleGraph.TripartiteFromTriangles.cliqueFinset_eq_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [Fintype α] [Fintype β] [Fintype γ] [NoAccidental t] :
            (graph t).cliqueFinset 3 = Finset.map toTriangle t
            source
            @[simp]
            theorem SimpleGraph.TripartiteFromTriangles.card_triangles {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [Fintype α] [Fintype β] [Fintype γ] [NoAccidental t] :
            ((graph t).cliqueFinset 3).card = t.card
            source
            theorem SimpleGraph.TripartiteFromTriangles.farFromTriangleFree {α : Type u_1} {β : Type u_2} {γ : Type u_3} {𝕜 : Type u_4} [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (t : Finset (α × β × γ)) [DecidableEq α] [DecidableEq β] [DecidableEq γ] [Fintype α] [Fintype β] [Fintype γ] [ExplicitDisjoint t] {ε : 𝕜} (ht : ε * ↑((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) ≤ ↑t.card) :
            (graph t).FarFromTriangleFree ε
            source
            theorem SimpleGraph.TripartiteFromTriangles.locallyLinear {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ)) [ExplicitDisjoint t] [NoAccidental t] :
            (graph t).LocallyLinear