Definition and Surjectivity of Laplacian

In this file we define the Laplacian of a simple graph X and the notion of harmonic functions. We show that if X is a tree, with the property that each vertex has at least two and only finitely many neighbours, then the Laplacian is surjective.

noncomputable def SimpleGraph.incidenceEquiv {V : Type u_3} {X : SimpleGraph V} (v : V) : ↑{e : ↑X.edgeSet | v ∈ ↑e} ≃ ↑(X.incidenceSet v)

Edges containing v are equivalent to the incidence set at v.

Equations

• SimpleGraph.incidenceEquiv v = { toFun := fun (e : ↑{e : ↑X.edgeSet | v ∈ ↑e}) => ⟨↑↑e, ⋯⟩, invFun := fun (e : ↑(X.incidenceSet v)) => ⟨⟨↑e, ⋯⟩, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

instance SimpleGraph.instFiniteElemSym2EdgeSetSetOfMemValSetOfIncidenceSet_leanPool {V : Type u_3} {X : SimpleGraph V} (v : V) [Finite ↑(X.incidenceSet v)] : Finite ↑{e : ↑X.edgeSet | v ∈ ↑e}

noncomputable def SimpleGraph.incidenceFinset' {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} (v : V) [Fintype ↑(X.neighborSet v)] : Finset ↑X.edgeSet

The finset of the edges of X consisting of all edges connected to v.

Equations

• SimpleGraph.incidenceFinset' v = ⋯.toFinset

theorem SimpleGraph.mem_incidenceFinset' {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} (v : V) [Fintype ↑(X.neighborSet v)] (e : ↑X.edgeSet) : e ∈ incidenceFinset' v ↔ v ∈ ↑e

noncomputable def SimpleGraph.laplace {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : ↑X.edgeSet → M) (v : V) : M

The Laplacian of an M-valued function on the set of edges of X as an M-valued function on the vertices of X.

Equations

• SimpleGraph.laplace w f v = w v • ∑ e ∈ SimpleGraph.incidenceFinset' v, f e

noncomputable def SimpleGraph.IsHarmonic {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : ↑X.edgeSet → M) : Prop

A function on the edges of X is called harmonic, if the Laplacian of it is zero.

Equations

• SimpleGraph.IsHarmonic w f = (SimpleGraph.laplace w f = 0)

structure SimpleGraph.Tree (V : Type u_4) extends SimpleGraph V : Type u_4

A simple graph equipped with a proof that it is a tree.

• Adj : V → V → Prop
• symm : Std.Symm self.Adj
• loopless : Std.Irrefl self.Adj
• isTree : self.IsTree

theorem SimpleGraph.Tree.exists_path_eq_append_of_isPath_of_mem_support {V : Type u_3} {X : Tree V} {v w x : V} (p : X.Walk v w) (hp : p.IsPath) (hx : x ∈ p.support) : ∃ (r : X.Walk v x) (s : X.Walk x w), r.IsPath ∧ s.IsPath ∧ p = r.append s

theorem SimpleGraph.Tree.exists_path_eq_cons_of_isPath_of_mem_support {V : Type u_3} {X : Tree V} (v₀ : V) {v w : V} (h : X.Adj w v) (p : X.Walk w v₀) (hv : v ∈ p.support) (hpath : p.IsPath) : ∃ (r : X.Walk v v₀), r.IsPath ∧ p = Walk.cons h r

theorem SimpleGraph.Tree.dist_ne_of_of_adj {V : Type u_3} {X : Tree V} (v₀ : V) {v w : V} (h : X.Adj v w) : X.dist v₀ v ≠ X.dist v₀ w

theorem SimpleGraph.Tree.exists_ordered {V : Type u_3} {X : Tree V} (v₀ : V) (e : ↑X.edgeSet) : ∃ (p : V × V), X.dist v₀ p.1 < X.dist v₀ p.2 ∧ s(p.1, p.2) = ↑e

noncomputable def SimpleGraph.Tree.source {V : Type u_3} {X : Tree V} (v₀ : V) (e : ↑X.edgeSet) : V

Given an edge e of X, the source is the vertex of e closer to v₀.

Equations

• SimpleGraph.Tree.source v₀ e = ⋯.choose.1

noncomputable def SimpleGraph.Tree.target {V : Type u_3} {X : Tree V} (v₀ : V) (e : ↑X.edgeSet) : V

Given an edge e of X, the target is the vertex of e farther from v₀.

Equations

• SimpleGraph.Tree.target v₀ e = ⋯.choose.2

theorem SimpleGraph.Tree.norm_source_lt_norm_target {V : Type u_3} {X : Tree V} (v₀ : V) (e : ↑X.edgeSet) : X.dist v₀ (source v₀ e) < X.dist v₀ (target v₀ e)

theorem SimpleGraph.Tree.edge_eq_mk_source_target {V : Type u_3} {X : Tree V} (v₀ : V) (e : ↑X.edgeSet) : ↑e = s(source v₀ e, target v₀ e)

@[simp]

theorem SimpleGraph.Tree.source_mem {V : Type u_3} {X : Tree V} (v₀ : V) (e : ↑X.edgeSet) : source v₀ e ∈ ↑e

@[simp]

theorem SimpleGraph.Tree.target_mem {V : Type u_3} {X : Tree V} (v₀ : V) (e : ↑X.edgeSet) : target v₀ e ∈ ↑e

theorem SimpleGraph.Tree.source_adj_target {V : Type u_3} {X : Tree V} (v₀ : V) (e : ↑X.edgeSet) : X.Adj (source v₀ e) (target v₀ e)

theorem SimpleGraph.Tree.norm_target_eq_norm_source_add_one {V : Type u_3} {X : Tree V} (v₀ : V) (e : ↑X.edgeSet) : X.dist v₀ (target v₀ e) = X.dist v₀ (source v₀ e) + 1

theorem SimpleGraph.Tree.eq_source_or_eq_target_of_mem {V : Type u_3} {X : Tree V} (v₀ : V) (e : ↑X.edgeSet) (v : V) (hv : v ∈ ↑e) : source v₀ e = v ∨ target v₀ e = v

theorem SimpleGraph.Tree.zero_lt_norm_target {V : Type u_3} {X : Tree V} (v₀ : V) (e : ↑X.edgeSet) : 0 < X.dist v₀ (target v₀ e)

@[simp]

theorem SimpleGraph.Tree.source_eq_origin_of_mem {V : Type u_3} {X : Tree V} (v₀ : V) (e : ↑X.edgeSet) (h : v₀ ∈ ↑e) : source v₀ e = v₀

noncomputable def SimpleGraph.Tree.outwardCone {V : Type u_3} {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ w : V) : Finset V

The outward cone of a vertex w wrt. v₀ is the finset of neighbors that has a bigger distance to v₀ than w.

Equations

• SimpleGraph.Tree.outwardCone v₀ w = ⋯.toFinset

theorem SimpleGraph.Tree.mem_outwardCone_iff {V : Type u_3} {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ w a : V) : a ∈ outwardCone v₀ w ↔ X.Adj w a ∧ X.dist v₀ w < X.dist v₀ a

A vertex a is in the outward cone of a vertex w, iff a is a neighbour and has bigger distance to v₀ than w.

theorem SimpleGraph.Tree.not_mem_outwardCone {V : Type u_3} {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ w : V) : w ∉ outwardCone v₀ w

noncomputable def SimpleGraph.Tree.outwardEdgeCone {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ w : V) : Finset ↑X.edgeSet

The outward edge cone of a vertex w wrt. v₀ is the finset of neighboring edges where w is the source vertex wrt. to v₀.

Equations

• SimpleGraph.Tree.outwardEdgeCone v₀ w = ⋯.toFinset

theorem SimpleGraph.Tree.mem_outwardEdgeCone_iff {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ w : V) (e : ↑X.edgeSet) : e ∈ outwardEdgeCone v₀ w ↔ w ∈ ↑e ∧ source v₀ e = w

theorem SimpleGraph.Tree.outwardEdgeCone_nonempty_of_source {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ : V) (e : ↑X.edgeSet) : (outwardEdgeCone v₀ (source v₀ e)).Nonempty

theorem SimpleGraph.Tree.outwardEdgeCone_origin_eq {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ : V) : outwardEdgeCone v₀ v₀ = incidenceFinset' v₀

The outward edge cone of the origin v₀ is the finset of all neighboring edges.

noncomputable def SimpleGraph.Tree.distinguishedEdge {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ w : V) (hw : (outwardEdgeCone v₀ w).Nonempty) : ↑X.edgeSet

An arbitrary choice of a distinguished edge pointing away from v₀.

Equations

• SimpleGraph.Tree.distinguishedEdge v₀ w hw = Exists.choose hw

theorem SimpleGraph.Tree.distinguishedEdge_mem {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ w : V) (hw : (outwardEdgeCone v₀ w).Nonempty) : distinguishedEdge v₀ w hw ∈ outwardEdgeCone v₀ w

@[simp]

theorem SimpleGraph.Tree.source_distinguishedEdge {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ v : V) (hnonempty : (outwardEdgeCone v₀ v).Nonempty) : source v₀ (distinguishedEdge v₀ v hnonempty) = v

theorem SimpleGraph.Tree.outwardEdgeCone_eq_union {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ w : V) (hw : (outwardEdgeCone v₀ w).Nonempty) : ↑(outwardEdgeCone v₀ w) = {distinguishedEdge v₀ w hw} ∪ {e : ↑X.edgeSet | e ∈ outwardEdgeCone v₀ w ∧ distinguishedEdge v₀ w hw ≠ e}

theorem SimpleGraph.Tree.exists_edge_dist_source_lt {V : Type u_3} {X : Tree V} (v₀ w : V) (hw : 0 < X.dist v₀ w) : ∃ (e : ↑X.edgeSet), target v₀ e = w

For every vertex w different from the root vertex v₀ there exists an edge e, whose target is w.

noncomputable def SimpleGraph.Tree.edgeTowardsOrigin {V : Type u_3} {X : Tree V} (v₀ w : V) (hw : 0 < X.dist v₀ w) : ↑X.edgeSet

If w is not the origin, then this is the unique edge pointing towards the origin. For uniqueness, see eq_edgeTowardsOrigin_iff_of_mem.

Equations

• SimpleGraph.Tree.edgeTowardsOrigin v₀ w hw = ⋯.choose

@[simp]

theorem SimpleGraph.Tree.edgeTowardsOrigin_target_eq {V : Type u_3} {X : Tree V} (v₀ w : V) (hw : 0 < X.dist v₀ w) : target v₀ (edgeTowardsOrigin v₀ w hw) = w

theorem SimpleGraph.Tree.eq_of_isPath {V : Type u_3} {X : Tree V} {x y : V} {p q : X.Walk x y} (hp : p.IsPath) (hq : q.IsPath) : p = q

theorem SimpleGraph.Tree.dist_eq_of_isPath {V : Type u_3} {X : Tree V} {x y : V} (p : X.Walk x y) (hp : p.IsPath) : X.dist x y = p.length

theorem SimpleGraph.Tree.source_eq_of_target_eq {V : Type u_3} {X : Tree V} (v₀ : V) (e f : ↑X.edgeSet) (h : target v₀ e = target v₀ f) : source v₀ e = source v₀ f

theorem SimpleGraph.Tree.eq_of_target_eq {V : Type u_3} {X : Tree V} (v₀ : V) (e f : ↑X.edgeSet) (h : target v₀ e = target v₀ f) : e = f

theorem SimpleGraph.Tree.eq_edgeTowardsOrigin_iff_of_mem {V : Type u_3} {X : Tree V} (v₀ w : V) (hw : 0 < X.dist v₀ w) (e : ↑X.edgeSet) (hmem : w ∈ ↑e) : e = edgeTowardsOrigin v₀ w hw ↔ target v₀ e = w

theorem SimpleGraph.Tree.vertex_mem_edgeTowardsOrigin {V : Type u_3} {X : Tree V} (v₀ w : V) (hw : 0 < X.dist v₀ w) : w ∈ ↑(edgeTowardsOrigin v₀ w hw)

theorem SimpleGraph.Tree.edgeTowardsOrigin_not_mem_outwardEdgeCone {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ v : V) (hdist : 0 < X.dist v₀ v) : edgeTowardsOrigin v₀ v hdist ∉ outwardEdgeCone v₀ v

theorem SimpleGraph.Tree.outwardEdgeCone_nonempty_of_two_le_degree {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ : V) {v : V} (hv : 2 ≤ X.degree v) : (outwardEdgeCone v₀ v).Nonempty

noncomputable def SimpleGraph.Tree.auxBorder {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : V → M) (v₀ : V) (n : ℕ) (g : ↑X.edgeSet → M) (e : ↑X.edgeSet) (he : X.dist v₀ (target v₀ e) = n + 1) : M

Boundary value used in the recursive construction of a preimage of the Laplacian.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SimpleGraph.Tree.aux {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : V → M) (v₀ : V) (n : ℕ) : ↑X.edgeSet → M

Recursive auxiliary function assigning values to edges at bounded distance from the root.

Equations

• One or more equations did not get rendered due to their size.
• SimpleGraph.Tree.aux w f v₀ 0 = fun (x : ↑X.edgeSet) => 0

theorem SimpleGraph.Tree.aux_zero_of_gt {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : V → M) (v₀ : V) (n : ℕ) (e : ↑X.edgeSet) (h : n + 1 < X.dist v₀ (target v₀ e)) : aux w f v₀ n e = 0

theorem SimpleGraph.Tree.aux_extends {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : V → M) (v₀ : V) (n : ℕ) (e : ↑X.edgeSet) (he : X.dist v₀ (target v₀ e) ≤ n) : aux w f v₀ (n + 1) e = aux w f v₀ n e

theorem SimpleGraph.Tree.aux_extends' {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : V → M) (v₀ : V) (n : ℕ) (e : ↑X.edgeSet) (he : X.dist v₀ (target v₀ e) ≤ n) : aux w f v₀ (X.dist v₀ (target v₀ e)) e = aux w f v₀ n e

theorem SimpleGraph.Tree.incidenceFinset_eq_union {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (v₀ v : V) (hv : 0 < X.dist v₀ v) : incidenceFinset' v = {edgeTowardsOrigin v₀ v hv} ∪ outwardEdgeCone v₀ v

theorem SimpleGraph.Tree.aux_spec_origin_distinguishedEdge {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : V → M) (v₀ : V) (hnonempty : (outwardEdgeCone v₀ v₀).Nonempty) : aux w f v₀ 1 (distinguishedEdge v₀ v₀ hnonempty) = (w v₀)⁻¹ • f v₀

theorem SimpleGraph.Tree.aux_spec₀ {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : V → M) (v₀ : V) (e : ↑X.edgeSet) (n : ℕ) (he : X.dist v₀ (target v₀ e) ≤ n) (hnotdist : distinguishedEdge v₀ (source v₀ e) ⋯ ≠ e) : aux w f v₀ n e = 0

theorem SimpleGraph.Tree.aux_spec_outwardEdgeCone_erase {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : V → M) (v₀ : V) (n : ℕ) (v : V) (hv : X.dist v₀ v + 1 = n) (hnonempty : (outwardEdgeCone v₀ v).Nonempty) : ∑ x ∈ (outwardEdgeCone v₀ v).erase (distinguishedEdge v₀ v hnonempty), aux w f v₀ n x = 0

theorem SimpleGraph.Tree.aux_spec_distinguishedEdge {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : V → M) (v₀ : V) (n : ℕ) (v : V) (hv : X.dist v₀ v + 1 = n) (hlt : 0 < X.dist v₀ v) (hnonempty : (outwardEdgeCone v₀ v).Nonempty) : aux w f v₀ n (distinguishedEdge v₀ v hnonempty) = (w v)⁻¹ • f v - aux w f v₀ n (edgeTowardsOrigin v₀ v hlt)

theorem SimpleGraph.Tree.aux_spec {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : V → M) (v₀ : V) (n : ℕ) (v : V) (hv : X.dist v₀ v + 1 = n) (hnonempty : (outwardEdgeCone v₀ v).Nonempty) : w v • ∑ e ∈ incidenceFinset' v, aux w f v₀ n e = f v

noncomputable def SimpleGraph.Tree.preimage {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : V → M) (v₀ : V) (e : ↑X.edgeSet) : M

The constructed preimage of a vertex function under the Laplacian.

Equations

• SimpleGraph.Tree.preimage w f v₀ e = SimpleGraph.Tree.aux w f v₀ (X.dist v₀ (SimpleGraph.Tree.target v₀ e)) e

theorem SimpleGraph.Tree.laplace_preimage {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : Tree V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : V → M) (v₀ : V) (hinfinite : ∀ (v : V), (outwardEdgeCone v₀ v).Nonempty) : laplace w (preimage w f v₀) = f

The constructed preimage is indeed a preimage of the Laplacian.

theorem SimpleGraph.laplace_surjective {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} (htree : X.IsTree) [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (hmindeg : ∀ (v : V), 2 ≤ X.degree v) : Function.Surjective (laplace w)

If X is a tree, the Laplacian on X is surjective.

theorem SimpleGraph.laplace_apply {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : ↑X.edgeSet → M) (v : V) : laplace w f v = w v • ∑ e ∈ incidenceFinset' v, f e

@[simp]

theorem SimpleGraph.laplace_zero {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) : laplace w 0 = 0

@[simp]

theorem SimpleGraph.laplace_add {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f g : ↑X.edgeSet → M) : laplace w (f + g) = laplace w f + laplace w g

noncomputable def SimpleGraph.laplaceHom {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) : (↑X.edgeSet → M) →+ V → M

The Laplacian of X as a group homomorphism.

Equations

• SimpleGraph.laplaceHom w = { toFun := SimpleGraph.laplace w, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem SimpleGraph.laplaceHom_apply {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (f : ↑X.edgeSet → M) (v : V) : (laplaceHom w) f v = laplace w f v

theorem SimpleGraph.laplaceHom_surjective {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (htree : X.IsTree) (hdeg : ∀ (v : V), 2 ≤ X.degree v) : Function.Surjective ⇑(laplaceHom w)

@[simp]

theorem SimpleGraph.laplace_ASmul {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) (a : A) (f : ↑X.edgeSet → M) : laplace w (a • f) = a • laplace w f

theorem SimpleGraph.isLinearMap_laplace {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) : IsLinearMap A (laplace w)

noncomputable def SimpleGraph.laplaceLinearMap {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) : (↑X.edgeSet → M) →ₗ[A] V → M

The Laplacian of X as an A-linear map.

Equations

• SimpleGraph.laplaceLinearMap w = IsLinearMap.mk' (SimpleGraph.laplace w) ⋯

@[simp]

theorem SimpleGraph.coe_laplaceLinearMap {A : Type u_1} [CommRing A] {M : Type u_2} [AddCommGroup M] [Module A M] {V : Type u_3} [DecidableEq V] {X : SimpleGraph V} [(v : V) → Fintype ↑(X.neighborSet v)] (w : V → Aˣ) : ⇑(laplaceLinearMap w) = laplace w

@[simp]

theorem SimpleGraph.arrowAction_apply {G : Type u_8} {A : Type u_9} {B : Type u_10} [DivisionMonoid G] [MulAction G A] (g : G) (f : A → B) (a : A) : (g • f) a = f (g⁻¹ • a)

@[implicit_reducible]

noncomputable instance SimpleGraph.arrowDistribMulAction {G : Type u_8} {A : Type u_9} {B : Type u_10} [DivisionMonoid G] [MulAction G A] [AddMonoid B] : DistribMulAction G (A → B)

Equations

• SimpleGraph.arrowDistribMulAction = { toMulAction := arrowAction, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

noncomputable instance SimpleGraph.instSMulUnitsLeanPool {R : Type u_4} [CommRing R] (G : Type u_7) : SMul G Rˣ

Equations

• SimpleGraph.instSMulUnitsLeanPool G = { smul := fun (x : G) (x_1 : Rˣ) => x_1 }

@[simp]

theorem SimpleGraph.smul_units {R : Type u_4} [CommRing R] (G : Type u_7) (g : G) (x : Rˣ) : g • x = x

@[simp]

theorem SimpleGraph.laplace_smul {R : Type u_4} [CommRing R] {M : Type u_5} [AddCommGroup M] [Module R M] {V : Type u_6} [DecidableEq V] {G : Type u_7} [Group G] [MulAction G V] {X : SimpleGraph V} [GraphAction G X] [(v : V) → Fintype ↑(X.neighborSet v)] (w : V →ₑ[id] Rˣ) (g : G) (f : ↑X.edgeSet → M) : laplace (⇑w) (g • f) = g • laplace (⇑w) f

noncomputable def SimpleGraph.laplaceSMulHom {R : Type u_4} [CommRing R] {M : Type u_5} [AddCommGroup M] [Module R M] {V : Type u_6} [DecidableEq V] {G : Type u_7} [Group G] [MulAction G V] {X : SimpleGraph V} [GraphAction G X] [(v : V) → Fintype ↑(X.neighborSet v)] (w : V →ₑ[id] Rˣ) : (↑X.edgeSet → M) →+[G] V → M

The Laplacian of X as a G-module homomorphism.

Equations

• SimpleGraph.laplaceSMulHom w = { toFun := SimpleGraph.laplace ⇑w, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem SimpleGraph.laplaceSMulHom_surjective {R : Type u_4} [CommRing R] {M : Type u_5} [AddCommGroup M] [Module R M] {V : Type u_6} [DecidableEq V] {G : Type u_7} [Group G] [MulAction G V] {X : SimpleGraph V} [GraphAction G X] [(v : V) → Fintype ↑(X.neighborSet v)] (w : V →ₑ[id] Rˣ) (htree : X.IsTree) (hdeg : ∀ (v : V), 2 ≤ X.degree v) : Function.Surjective ⇑(laplaceSMulHom w)