structure Graph.orientation {α : Type u_1} {β : Type u_2} (G : Graph α β) : Type (max u_1 u_2)

• dInc : ↑G.edgeSet → α × α
• isLink_of_dInc (e : ↑G.edgeSet) : G.IsLink (↑e) (self.dInc e).1 (self.dInc e).2

theorem Graph.orientation_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} : Nonempty G.orientation

def Graph.orientation.anti {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hGH : G ≤ H) (D : H.orientation) : G.orientation

Equations

• Graph.orientation.anti hGH D = { dInc := fun (e : ↑G.edgeSet) => D.dInc ⟨↑e, ⋯⟩, isLink_of_dInc := ⋯ }

@[simp]

theorem Graph.orientation.anti_apply {α : Type u_1} {β : Type u_2} {G H : Graph α β} (hGH : G ≤ H) (D : H.orientation) (e : ↑G.edgeSet) : (anti hGH D).dInc e = D.dInc ⟨↑e, ⋯⟩

def Graph.orientation.signedIncMatrix {α : Type u_1} {β : Type u_2} {G : Graph α β} [DecidablePred fun (x : β) => x ∈ G.edgeSet] [DecidableEq α] (D : G.orientation) (𝔽 : Type u_4) [Ring 𝔽] : Matrix β α 𝔽

Equations

• D.signedIncMatrix 𝔽 = Matrix.of fun (e : β) => if he : e ∈ G.edgeSet then Function.update 0 (D.dInc ⟨e, he⟩).2 1 - Function.update 0 (D.dInc ⟨e, he⟩).1 1 else 0

theorem Graph.orientation.signedIncMatrix_apply_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {𝔽 : Type u_3} [CommRing 𝔽] [DecidablePred fun (x : β) => x ∈ G.edgeSet] [DecidableEq α] (he : e ∈ G.edgeSet) (D : G.orientation) : D.signedIncMatrix 𝔽 e = Function.update 0 (D.dInc ⟨e, he⟩).2 1 - Function.update 0 (D.dInc ⟨e, he⟩).1 1

theorem Graph.orientation.signedIncMatrix_apply_of_not_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {𝔽 : Type u_3} [CommRing 𝔽] [DecidablePred fun (x : β) => x ∈ G.edgeSet] [DecidableEq α] (he : e ∉ G.edgeSet) (D : G.orientation) : D.signedIncMatrix 𝔽 e = 0

theorem Graph.orientation.signedIncMatrix_anti_submatrix {α : Type u_1} {β : Type u_2} {G H : Graph α β} {e : β} {𝔽 : Type u_3} [CommRing 𝔽] [DecidablePred fun (x : β) => x ∈ G.edgeSet] [DecidableEq α] (hGH : G ≤ H) (he : e ∈ G.edgeSet) (D : H.orientation) : (anti hGH D).signedIncMatrix 𝔽 e = D.signedIncMatrix 𝔽 e

theorem Graph.orientation.signedIncMatrix_ne_zero_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {e : β} {𝔽 : Type u_3} [CommRing 𝔽] [DecidablePred fun (x : β) => x ∈ G.edgeSet] [DecidableEq α] [Nontrivial 𝔽] (D : G.orientation) : D.signedIncMatrix 𝔽 e x ≠ 0 ↔ G.IsNonloopAt e x

theorem Graph.orientation.signedIncMatrix_pendent_col_support {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {e : β} {𝔽 : Type u_3} [CommRing 𝔽] [DecidablePred fun (x : β) => x ∈ G.edgeSet] [DecidableEq α] [Nontrivial 𝔽] (hx : G.IsPendant e x) (D : G.orientation) : Function.support ((D.signedIncMatrix 𝔽).col x) = {e}

def Graph.orientation.coeff_walk {α : Type u_1} {β : Type u_2} {G : Graph α β} [DecidableEq α] {w : WList α β} [DecidableEq β] (hw : G.IsWalk w) (𝔽 : Type u_4) [Ring 𝔽] (D : G.orientation) : β → 𝔽

Equations

• Graph.orientation.coeff_walk hw 𝔽 D e = if he : e ∈ w.edge then if (w.dIncLast he).1 = (D.dInc ⟨e, ⋯⟩).1 then 1 else -1 else 0

theorem Graph.orientation.coeff_isCycleWalk_not_zero {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} [DecidableEq α] {w : WList α β} [DecidableEq β] (hw : G.IsCyclicWalk w) (he : e ∈ w.edge) (𝔽 : Type u_4) [Ring 𝔽] [Nontrivial 𝔽] (D : G.orientation) : coeff_walk ⋯ 𝔽 D e ≠ 0

theorem Graph.orientation.coeff_signedIncMatrix {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {𝔽 : Type u_3} [CommRing 𝔽] [DecidablePred fun (x : β) => x ∈ G.edgeSet] [DecidableEq α] {w : WList α β} [DecidableEq β] (hw : G.IsWalk w) (he : e ∈ w.edge) (D : G.orientation) : coeff_walk hw 𝔽 D e • D.signedIncMatrix 𝔽 e = Function.update 0 (w.dIncLast he).2 1 - Function.update 0 (w.dIncLast he).1 1

theorem Graph.orientation.coeff_walk_cons_stable {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {e f : β} {𝔽 : Type u_3} [CommRing 𝔽] [DecidableEq α] {w : WList α β} [DecidableEq β] (hw : G.IsWalk (WList.cons x e w)) (hf : f ∈ w.edge) (D : G.orientation) : coeff_walk hw 𝔽 D f = coeff_walk ⋯ 𝔽 D f

theorem Graph.orientation.signedIncMatrix_isTrail {α : Type u_1} {β : Type u_2} {G : Graph α β} {𝔽 : Type u_3} [CommRing 𝔽] [DecidablePred fun (x : β) => x ∈ G.edgeSet] [DecidableEq α] {w : WList α β} [DecidableEq β] (hw : G.IsTrail w) (hne : w.Nonempty) (D : G.orientation) : ∑ e ∈ w.edge.toFinset, coeff_walk ⋯ 𝔽 D e • D.signedIncMatrix 𝔽 e = Function.update 0 w.last 1 - Function.update 0 w.first 1

theorem Graph.orientation.signedIncMatrix_isCyclicWalk {α : Type u_1} {β : Type u_2} {G : Graph α β} {𝔽 : Type u_3} [CommRing 𝔽] [DecidablePred fun (x : β) => x ∈ G.edgeSet] [DecidableEq α] {w : WList α β} [DecidableEq β] (hw : G.IsCyclicWalk w) (D : G.orientation) : ∑ e ∈ w.edge.toFinset, coeff_walk ⋯ 𝔽 D e • D.signedIncMatrix 𝔽 e = 0