feat: Colors alternate in a bicolored path

[IvanRenison]

Add the theorem pathGraph_G_Hom_coloring saying that if a graph has a homorphism from a pathGraph then the colors alternate in the path. Specifically, the theorem ask for the first element of the path to be colored by true, and in the pathGraph_G_Hom_coloring' it ask for the first element to be colored by false.

---

• [x] depends on: #11192
• [ ] depends on: #11787

[IvanRenison]

I plan to use this theorems for (first) defining a cyclic graph and then proving it's chromatic number (in particular I will use this theorems for the odd case of the cyclic graph)

[IvanRenison]

Very good suggestions, thank you very much, I will apply them. Are you going to add more comments or did you forgot to change the label to awaiting-author?

[YaelDillies]

The labels are loosely used (they are mostly there for when the PR has been without activity for some time), but yes I can mark it awaiting-author.

[kmill]

@YaelDillies These seem to be all the variants we could consider, and we'd want an equivalence between each pair in each variant. Many of these have versions where you construct a walk or homomorphism from the other without the sigma type, since you can figure out the correct endpoints, but notice that there are a bunch of annoying dependent type issues. I'm not sure what the "right" implementation is for anything but the first, and maybe the fourth, but maybe we should define a type for each possibility?

-- Walk between two specific vertices:
G.Walk u v
Σ n, {φ : pathGraph (n + 1) →g G // φ 0 = u ∧ φ n = v}

-- Walk between two unspecified vertices:
Σ u v, G.Walk u v
Σ n, pathGraph (n + 1) →g G

-- Walk of a particular length between two specific vertices
{p : G.Walk u v // p.length = n}
{φ : pathGraph (n + 1) →g G // φ 0 = u ∧ φ n = v}

-- Walk of a particular length between two unspecified vertices
Σ u v, {p : G.Walk u v // p.length = n}
pathGraph (n + 1) →g G

[IvanRenison]

I will try As you sed the "obvious" way to state it gives the error that pathGraph (length (ofPathGraphHom α G hom) + 1) →g G is not the same that pathGraph (n + 1) →g G. I was able to state it like this:

theorem Walk.of_to_PathGraphHom (G : SimpleGraph α) {n : ℕ} (hom : pathGraph (n + 1) →g G) :
    ∀ (i : Fin (n + 1)), hom i = (ofPathGraphHom α G hom).toPathGraphHom i := sorry

With two implicit casts in the second i And like this:

theorem Walk.ofPathGraphHom_lenght (G : SimpleGraph α) {n : ℕ} (hom : pathGraph (n + 1) →g G) :
    (ofPathGraphHom α G hom).length = n := sorry

theorem Walk.of_to_PathGraphHom' (G : SimpleGraph α) {n : ℕ} (hom : pathGraph (n + 1) →g G) :
    ∀ (i : Fin (n + 1)),
      hom i =
        (ofPathGraphHom α G hom).toPathGraphHom ⟨i.val, by rw [ofPathGraphHom_lenght]; exact i.prop⟩
  := sorry

With a explicit cast Witch one you think is better? (Or maybe you have a better one?)

[YaelDillies]

I think your second way is better (at least until we acquire SimpleGraph.Iso.ofEq. Note that for the equality the other way around you should use Walk.copy.

[Parcly-Taxel]

I think your second way is better (at least until we acquire SimpleGraph.Iso.ofEq).

What is the statement of SimpleGraph.Iso.ofEq?

[IvanRenison]

Now I added the theorem for a walk using the one for a pathGraph homorphism

[YaelDillies]

Sorry, I don't have time to review this anymore. Maybe @kmill or @b-mehta will?

[IvanRenison]

Hi @kmill, as this pull request has become big, and I guess that difficult to review because of that, maybe it will be better if I split it in smaller pull requests? So that it is easier to review

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#11192~~
• ~~leanprover-community/mathlib4#11787~~ By Dependent Issues (🤖). Happy coding!