Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(Combinatorics/SimpleGraph): conversions between SimpleGraph and Digraphs #16954

Open
wants to merge 5 commits into
base: master
Choose a base branch
from

Conversation

Rida-Hamadani
Copy link
Collaborator

And proves some lemmas about them. Also defines the related oriented graphs. This is a first step to start porting the material of the SimpleGraph part of the library into Digraphs.


Open in Gitpod

Copy link

github-actions bot commented Sep 19, 2024

PR summary b446b25eee

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Combinatorics.Digraph.Orientation 498

Declarations diff

+ Asymmetric
+ IsOriented
+ gc_toDigraph_toSimpleGraphAnd
+ isOriented_def
+ isOriented_loopless
+ isOriented_toSimpleGraphAnd_eq_bot
+ toDigraph
+ toDigraph_mono
+ toSimpleGraphAnd
+ toSimpleGraphAnd_bot
+ toSimpleGraphAnd_eq_bot_iff_isOriented_and_loopless
+ toSimpleGraphAnd_mono
+ toSimpleGraphAnd_subgraph_toSimpleGraphOr
+ toSimpleGraphAnd_top
+ toSimpleGraphOr
+ toSimpleGraphOr_bot
+ toSimpleGraphOr_mono
+ toSimpleGraphOr_top

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

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

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

@Rida-Hamadani Rida-Hamadani added the t-combinatorics Combinatorics label Sep 20, 2024
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sorry, I'm as of yet unconvinced that Digraph deserves to be a thing as opposed to just using V → V → Prop😅

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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do you think you could find more semantic names for these two operations?

@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Oct 31, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
awaiting-author A reviewer has asked the author a question or requested changes t-combinatorics Combinatorics
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants