feat(Combinatorics/SimpleGraph): conversions between SimpleGraph and Digraphs
#16954
+147
−0
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
PR summary b446b25eeeImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
vbeffara
reviewed
Sep 20, 2024
vbeffara
reviewed
Sep 20, 2024
YaelDillies
reviewed
Oct 31, 2024
Comment on lines
+91
to
+143
| section IsOriented | ||
|
|
||
| /-! ### Oriented graphs -/ | ||
|
|
||
| /-- | ||
| Oriented graphs are `Digraph`s that have no self-loops and no pair of vertices with edges in both | ||
| directions. | ||
| -/ | ||
| def IsOriented (G : Digraph V) : Prop := | ||
| Asymmetric G.Adj | ||
|
|
||
| lemma isOriented_def {G : Digraph V} (h : G.IsOriented) (v w : V) : ¬(G.Adj v w ∧ G.Adj w v) := | ||
| fun ⟨a, b⟩ ↦ h a b | ||
|
|
||
| lemma isOriented_loopless {G : Digraph V} (h : G.IsOriented) : Irreflexive G.Adj := | ||
| fun _ a ↦ h a a | ||
|
|
||
| lemma isOriented_toSimpleGraphAnd_eq_bot {G : Digraph V} (h : G.IsOriented) : | ||
| G.toSimpleGraphAnd = ⊥ := by | ||
| ext; exact ⟨fun ⟨_, a, b⟩ ↦ h a b, False.elim⟩ | ||
|
|
||
| lemma toSimpleGraphAnd_eq_bot_iff_isOriented_and_loopless {G : Digraph V} : | ||
| G.IsOriented ↔ G.toSimpleGraphAnd = ⊥ ∧ ∀ v, ¬G.Adj v v:= by | ||
| refine ⟨fun h ↦ ⟨isOriented_toSimpleGraphAnd_eq_bot h, isOriented_loopless h⟩, | ||
| fun ⟨h₁, h₂⟩ v w ↦ ?_⟩ | ||
| by_cases h : v = w | ||
| · exact h ▸ fun _ ↦ h₂ v | ||
| · exact fun a b ↦ (SimpleGraph.bot_adj v w).mp <| h₁ ▸ ⟨h, a, b⟩ | ||
|
|
||
| end IsOriented | ||
|
|
||
| end Digraph | ||
|
|
||
| namespace SimpleGraph | ||
|
|
||
| /-! ### Digraphs constructed from simple graphs -/ | ||
|
|
||
| /-- | ||
| Orienting map that gives a `Digraph` from a `SimpleGraph` by giving two edges in opposite directions | ||
| to each adjacent vertices in the `SimpleGraph`. | ||
| -/ | ||
| def toDigraph (G : SimpleGraph V) : Digraph V where | ||
| Adj v w := G.Adj v w | ||
|
|
||
| @[mono] | ||
| lemma toDigraph_mono : Monotone (toDigraph : _ → Digraph V) := | ||
| fun _ _ h₁ _ _ h₂ ↦ h₁ h₂ | ||
|
|
||
| lemma gc_toDigraph_toSimpleGraphAnd : | ||
| GaloisConnection toDigraph (Digraph.toSimpleGraphAnd : _ → SimpleGraph V) := | ||
| fun _ _ ↦ ⟨fun h₁ _ _ h₂ ↦ ⟨h₂.ne, h₁ h₂, h₁ h₂.symm⟩, fun h₁ _ _ h₂ ↦ (h₁ h₂).2.1⟩ | ||
|
|
||
| end SimpleGraph |
There was a problem hiding this comment.
I'm not really convinced by the usefulness of this section. G.Adj already does everything we want. Do you think you could split this half off to a later PR?
Comment on lines
+46
to
+56
| /-- | ||
| Orientation-forgetting map from `Digraph` to `SimpleGraph` that gives an unoriented edge if | ||
| either orientation is present. | ||
| -/ | ||
| def toSimpleGraphOr (G : Digraph V) : SimpleGraph V := SimpleGraph.fromRel G.Adj | ||
|
|
||
| /-- | ||
| Orientation-forgetting map from `Digraph` to `SimpleGraph` that gives an unoriented edge if | ||
| both orientations are present. | ||
| -/ | ||
| def toSimpleGraphAnd (G : Digraph V) : SimpleGraph V where |
There was a problem hiding this comment.
Do you think you could find more semantic names for these two operations?
YaelDillies
added
the
awaiting-author
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
And proves some lemmas about them. Also defines the related oriented graphs. This is a first step to start porting the material of the
SimpleGraphpart of the library intoDigraphs.