mathlib

mathlib copied to clipboard

and graph orientations.

---

The intention of this file is to create the oriented incidence matrix, together with some useful (I assume) lemmas and theorems for later use in other areas.

so sorry your PR has been basically left open forever, here are some comments. I'll look at N(o) later, but I think it's better you get to see some of these first

Hello! There is no worries about that, I am sure there are a lot of PRs in similar situations and there's a lot of workload. I wanted to say that, if this is fine for you, I will take a look into the PR after the 18th of June, since then I finish the exam session. Thanks for the feedback! 😄

No worries, best of luck! I'll try finish the review by then :)

@gabrielmoise Good luck with your exams. When you've updated your PR, please ping us on zulip so that we can review again. (For now I've labelled it WIP and awaiting-author.)

Thank you so much for waiting! And also thanks for the support towards my exams! They went fine :smile:!

Wow it took me long to catch the obvious! You're not defining the incidence matrix but the adjacency matrix. Here ya go for a round of renaming 😅 EDIT: This is wrong. I got completely confused.

isn't the adj matrix V × V? I think this is V × E

Wow it took me long to catch the obvious! You're not defining the incidence matrix but the adjacency matrix. Here ya go for a round of renaming

No, I am defining the incidence matrix. The adjacency matrix is already in the standard library as adj_matrix.

ping? @gabrielmoise - should we take over from you?

ping? @gabrielmoise - should we take over from you?

Hello!

Sorry for my inactivity! I was very busy lately with applications for internships and with university work. Yes, I would be very happy if you would take over from me. :)

Thanks a lot for the help!

Does anyone active on this PR see an easy way forward here? It was a part of @gabrielmoise 's project I supervised (and thus I feel like it should not be let to bitrot), but I'm not really familiar with most details here.

I have already many pans on the stove, but I could take that one too. For having reviewed this PR quite thoroughly, I know what"s to be fixed and can probably make it mergeable rather quickly. Any help remains welcome!

I think it would be good to split off a new PR of just the stuff about unoriented incidence matrices. Things about orientations and oriented incidence matrices can wait in this PR until then. (These still need some thought for how they'll interact with the rest of the library.)

I remember there were some theorems in this gist that would be good to include (the gist has the gist of unoriented incidence matrices, originally based on this PR). The combinatorics.simple_graph.adj_matrix module could probably be used as a model.

just the stuff about unoriented incidence matrices

The main reason for oriented incidence matrices to appear here is that it's the most direct way to get the Laplacian matrix of the graph. The latter didn't make it to this PR, though.

@dimpase I get that (and I very much want that factorization of the Laplacian matrix) -- what I've been thinking is that orientations should probably come from simple_digraph, which doesn't exist yet. There's a map simple_digraph V -> simple_graph V from forgetting orientations, or rather from symmetrizing the adj relation.

It might also be OK for orientations to be their own thing. I'd suggest changing the definition, though, to something that is closer to the definition of simple_graph. Here's a possibility, along with a reimplementation of the old projections in terms of it:

structure orientation (G : simple_graph V) :=
(fwd : V → V → Prop)
(fwd_adj : ∀ v w, fwd v w → G.adj v w)
(neg_fwd_iff_fwd : ∀ v w, ¬fwd v w ↔ fwd w v)

namespace orientation
variables {G} (o : G.orientation)
variables [decidable_eq V] [decidable_rel o.fwd]

def orient (e : G.edge_set) : V × V :=
sym2.lift ⟨λ v w, if o.fwd v w then (v, w) else (w, v),
λ v w, by { rw ←ite_not, simp [o.neg_fwd_iff_fwd] }⟩ e.val

@[simp] lemma orient_prop (e : G.edge_set) : ⟦o.orient e⟧ = e :=
begin
  cases e with e h,
  induction e using quotient.ind,
  cases e with v w,
  by_cases hf : o.fwd v w;
  simp [orient, hf, -quotient.eq, sym2.eq_swap],
end

def head (e : G.edge_set) : V := (o.orient e).1

def tail (e : G.edge_set) : V := (o.orient e).2

@[simp] lemma consistent (e : G.edge_set) : ⟦(o.head e, o.tail e)⟧ = e :=
begin
  cases e with e h,
  induction e using quotient.ind,
  simp [head, tail, orient_prop],
end

end orientation

@RaduEu