Results on maximal acyclic subgraphs

Stream: PR reviews

[Thomas Waring]

Two PRs proving results on maximal acyclic subgraphs (cf discussion here):

• #32041 proves that every acyclic subgraph H ≤ G can be extended to a maximal acyclic subgraph of G, using that the directed supremum of acyclic graphs is acyclic.
• #32043 characterises maximal acyclic subgraphs F of G as those for which F.Reachable = G.Reachable.

This is my first (hopefully!) contribution, so I am very grateful for any feedback.

I notice that the results of #32043 overlap with @Snir Broshi 's results in #30640, which proves the forward direction for subgraphs of the complete graph. I have no intention of scooping anyone, please let me know if it would be more appropriate for me to close my version. (In particular, my helping lemma IsAcyclic.add_edge_acyclic is proved in a better form in his PR, so at very least that ought to be incorporated.)

With these two PRs, it is straightforward to add the result that any graph contains a spanning forest, where we take that to mean a forest with the same reachability relation. Also, the converse of my characterisation of maximal acyclic subgraphs makes it relatively straightforward to define graphic matroids. If that's interesting I have it in an external repo.

[Snir Broshi]

Hello :wave:
Commented on the linked thread, it looks like we're working on very similar things :)
Very cool theorems, I think proving G.IsTree ↔ Nonempty V ∧ Maximal IsAcyclic G as a special case of your maximal_acyclic_iff_reachable_eq is a good idea, we need to save the best parts of both PRs.
Though I do think working with reachabilitySet (#30570) is the best, which isn't merged yet unfortunately.

[Snir Broshi]

A PR that uses docs#SimpleGraph.Connected.exists_isTree_le was merged #29309, I wonder if after you remove the Finite assumption we can remove it from the new statements as well (docs#SimpleGraph.Connected.exists_connected_induce_compl_singleton_of_finite_nontrivial and docs#SimpleGraph.Connected.exists_preconnected_induce_compl_singleton_of_finite).

[Yaël Dillies]

No that is impossible: consider the standard Cayley graph of $\Z$, no vertex can be removed without disconnecting the graph

[Thomas Waring]

Updates:

• #32043 is open, characterising maximal acyclic subgraphs by their reachability relation.
• Since #32041 was merged, I opened #33118 which shows that every graph has a spanning forest (tree).
  CC @Oliver Nash who reviewed the zorn-y PR, and @Bhavik Mehta who was looking at some similar results — if either of you are interested & have capacity :-)

[Snir Broshi]

Nice! Do you happen to know which lemmas from #30640 are already covered by your PRs?

[Thomas Waring]

Yep, I have in #32043

• your IsAcyclic.isAcyclic_sup_fromEdgeSet_of_not_reachable is my IsAcyclic.add_edge_acyclic (possibly your name is better), and
• your isTree_iff_maximal_isAcyclic is my maximal_isAcyclic_iff_isTree, derived as a special case of

theorem Connected.maximal_le_isAcyclic_iff_isTree {T : SimpleGraph V}
  (hG : G.Connected) (hT : T ≤ G) :
  Maximal (fun H => H ≤ G ∧ H.IsAcyclic) T ↔ T.IsTree

which in turn follows easily from my main result

theorem maximal_isAcyclic_iff_reachable_eq {F : SimpleGraph V}
  (hF : F ≤ G ∧ F.IsAcyclic) :
  Maximal (fun H => H ≤ G ∧ H.IsAcyclic) F ↔ F.Reachable = G.Reachable