Basis.mk

Stream: new members

[Adrian Wüthrich]

Hi all,
I'am trying to implement the graph Laplacian in lean and proving some theorems about it. I want to build a basis for the kernel of the laplacian by taking for each connected component a function that is constant on it and zero elsewhere. Consider the following familiy of functions indexed by the connected components of a SimpleGraph G.

def myBasis : G.ConnectedComponent → (V → ℝ) :=
  fun c ↦ fun i ↦ if G.connectedComponentMk i = c then 1 else 0

Now I'am trying to get a basis using Basis.mk by providing proofs that myBasis is spanning and linearly inependent

lemma myBasis_linearIndependent :
  LinearIndependent ℝ (myBasis G) := by
  sorry

lemma myBasis_spanning :
  LinearMap.ker (Matrix.toLinearMap₂' (G.lapMatrix ℝ)) ≤ Submodule.span ℝ (Set.range (myBasis G)) := by
  sorry

#check Basis.mk {G.ConnectedComponent} myBasis_linearIndependent myBasis_spanning

In the last line this results in the following error message

application type mismatch
  ↑(Basis.mk ?m.143919 ?m.143953) _
argument
  myBasis_spanning
has type
  ∀ (G : SimpleGraph ?m.144491) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq (ConnectedComponent G)],
    LinearMap.ker (↑toLinearMap₂' (lapMatrix G ℝ)) ≤ Submodule.span ℝ (Set.range (myBasis G)) : Prop
but is expected to have type
  ?m.143866 : Type ?u.143863

I have checked the types of all the involved objects and couldn't figure out the issue.
In case it matters here are the preceding definitions

variable {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq G.ConnectedComponent]

def SimpleGraph.degMatrix (R : Type*) [Ring R] : Matrix V V R :=
  of fun a b ↦ if a = b then (G.degree a : R) else 0

def SimpleGraph.lapMatrix (R : Type*) [Ring R] : Matrix V V R := G.degMatrix R - G.adjMatrix R

Any help would be much appreciated.

[Eric Wieser]

That error message is telling you that myBasis_spanning was expecting a G argument

[Eric Wieser]

(docs#Basis.mk)

[Eric Wieser]

You're also passing Basis.mk three arguments, but it expects two

[Adrian Wüthrich]

Thanks a lot. I now ran into a second problem. It looks like Basis.mk is infering the module that the basis spans from the codomain of myBasis, hence myBasis should look something like the following

def myBasis : G.ConnectedComponent → LinearMap.ker (Matrix.toLinearMap₂' (G.lapMatrix ℝ)) :=
  fun c ↦ (fun i ↦ if G.connectedComponentMk i = c then 1 else 0)

lemma myBasis_spanning :
  ⊤ ≤ Submodule.span ℝ (Set.range (myBasis G)) := by
  sorry

#check Basis.mk (myBasis_linearIndependent G) (myBasis_spanning G)

I guess that in the definition of myBasis I have to provide a proof that the given map is indeed in the kernel. What would be the syntax for that?

[Richard Copley]

Will you make a #mwe (with all required imports), please?

[Adrian Wüthrich]

Of course

import Mathlib.Combinatorics.SimpleGraph.Basic
import Mathlib.Combinatorics.SimpleGraph.Connectivity
import Mathlib.Combinatorics.SimpleGraph.AdjMatrix
import Mathlib.Data.Matrix.Basic
import Mathlib.Data.Fintype.Basic
import Mathlib.Data.Real.Basic
import Mathlib.LinearAlgebra.Basic
import Mathlib.LinearAlgebra.Matrix.BilinearForm

open Matrix SimpleGraph

variable {V : Type*} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] [DecidableEq G.ConnectedComponent]

def SimpleGraph.degMatrix (R : Type*) [Ring R] : Matrix V V R :=
  of fun a b ↦ if a = b then (G.degree a : R) else 0

def SimpleGraph.lapMatrix (R : Type*) [Ring R] : Matrix V V R := G.degMatrix R - G.adjMatrix R

def myBasis : G.ConnectedComponent → LinearMap.ker (Matrix.toLinearMap₂' (G.lapMatrix ℝ)) :=
  fun c ↦ (fun i ↦ if G.connectedComponentMk i = c then 1 else 0)

lemma myBasis_linearIndependent :
  LinearIndependent ℝ (myBasis G) := by
  sorry

lemma myBasis_spanning :
  ⊤ ≤ Submodule.span ℝ (Set.range (myBasis G)) := by
  sorry

#check Basis.mk (myBasis_linearIndependent G) (myBasis_spanning G)

[Eric Wieser]

This should get you started:

def myBasis (c : G.ConnectedComponent) : LinearMap.ker (Matrix.toLinearMap₂' (G.lapMatrix ℝ)) :=
  ⟨fun i ↦ if G.connectedComponentMk i = c then 1 else 0, sorry⟩

[Eric Wieser]

You can also simplify your first definition slightly to

def SimpleGraph.degMatrix (R : Type*) [Ring R] : Matrix V V R := Matrix.diagonal (G.degree ·)

[Adrian Wüthrich]

Now it fits all together. Many thanks!