[Merged by Bors] - feat(Topology/CWComplex): 1-skeleton Graph of CWComplex

[Jun2M]

This PR introduces CWComplex.OneSkeletonGraph, a graph with 0-dim cells as vertices and 1-dim cells as edges.

---

[github-actions]

PR summary ade87df682

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Topology.CWComplex.Classical.Graph (new file)	1408

---

Declarations diff

+ CWComplex.OneSkeletonGraph
+ CWComplex.exists_cellFrontier_one_eq
+ RelCWComplex.cellFrontier_one_eq
+ RelCWComplex.closedCell_zero_injective
+ RelCWComplex.injective_map_zero
+ RelCWComplex.map_zero_eq_self_iff
+ RelCWComplex.nonempty_cellFrontier
+ RelCWComplex.openCell_zero_injective
+ adj_iff
+ exists_isLoopAt_iff
+ exists_isLoopAt_iff_subsingleton
+ isLink_iff_pair
+ not_exists_isLoopAt_iff_nontrivial

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[scholzhannah]

Thank you for your PR! This looks fun. Purely out of interest: are you planning to use this for anything?

[scholzhannah]

Do you maybe want this to be a simp lemma?

[Jun2M]

There is a simps tag to the def of OneSkeletonGraph which auto-creates (OneSkeletonGraph C).IsLink e x y = (cellFrontier 1 e = closedCell 0 x ∪ closedCell 0 y) as a simp lemma. Do you think this lemma is preferable as simp lemma than the other?

[scholzhannah]

Ah, I see. Then I guess whichever you think will be more useful. I cannot really judge that.

[Jun2M]

Thank you for your review, @scholzhannah!

This looks fun. Purely out of interest: are you planning to use this for anything?

I am currently working with Graph planarity. One way to define that is to say R^2 is a CW-complex with the given graph as 1-skeleton. Also, topological minor of a graph come from existence of one graph embedding to another, it would be good to formalize that. The big milestone for me is to prove Kuratowski's theorem.

[jcommelin]

Nice work. Regarding planar graphs, are you aware of the notion of combinatorial hypermap? It seems that was a very useful concept in the formalization of the four colour theorem. See https://www.ams.org/notices/200811/tx081101382p.pdf

[Jun2M]

Thank you, @jcommelin! I am aware of combinatorial hypermap. However, Peter and I think that the planarity of a graph should "be" about ability to draw a graph on a plane, that is either defined as that property or explicitly shown equivalence to it, rather than contending with just the combinatorial side. I believe this should not be too difficult. Combinatorial hypermap will probably act as a steping stone/ an interface between the combinatorial description and analytical description of planarity.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job