Isogeny volcanoes

StructureMultigraph#✓fully proved

A multigraph on a vertex set \(V\) is given by an edge multiplicity function \(m\) that assigns to every two vertices \(v, w \in V\) a natural number \(m(v, w)\) and is symmetric: \(m(v, w) = m(w, v)\) for all \(v, w \in V\). Loops are permitted: \(m(v, v)\) may be positive.

structure Multigraph (V : Type*) where
  /-- The multiplicity of edges between two vertices. -/
  edgeMult : V → V → ℕ
  /-- Edge multiplicity is symmetric. -/
  symm : ∀ v w, edgeMult v w = edgeMult w v

Used by 17

Used byAdjacency in a multigraph · Symmetry of adjacency in a multigraph · Reversing an ascending edge gives a descending edge · Connectivity of vertices in a multigraph · Every vertex is connected to itself · Degree of a vertex in a multigraph · Degree restricted to a predicate · Degree splits over a predicate and its complement · Restricted degree depends only on the neighbours · Reversing a descending edge gives an ascending edge · Every edge of an isogeny volcano is horizontal, descending or ascending · Ascending edge · Connected multigraph · Descending edge · Horizontal edge · Isogeny volcano · Surface regularity of an isogeny volcano

DefinitionAdjacency in a multigraph#✓fully proved

Two vertices \(v\) and \(w\) of a multigraph \(G\) are adjacent when the edge multiplicity between \(v\) and \(w\) is positive.

def Adj (G : Multigraph V) (v w : V) : Prop :=
  0 < G.edgeMult v w

Uses 1 · Used by 3

Statement usesMultigraph

Used bySymmetry of adjacency in a multigraph · Connectivity of vertices in a multigraph · Every vertex is connected to itself

DefinitionDegree of a vertex in a multigraph#✓fully proved

For a multigraph \(G\) on a finite vertex set \(V\) with edge multiplicity \(m\), the degree of a vertex \(v\) is \(\sum_{w \in V} m(v, w)\). A loop at \(v\) contributes its multiplicity once, matching the outgoing-isogeny convention.

def degree (G : Multigraph V) [Fintype V] (v : V) : ℕ :=
  ∑ w : V, G.edgeMult v w

Uses 1 · Used by 2

Statement usesMultigraph

Used byDegree splits over a predicate and its complement · Isogeny volcano

DefinitionDegree restricted to a predicate#✓fully proved

Let \(G\) be a multigraph on a finite vertex set \(V\) with edge multiplicity \(m\), let \(v \in V\) and let \(P\) be a decidable predicate on \(V\). The degree of \(v\) restricted to \(P\) is \(\sum_{w \in V,\, P(w)} m(v, w)\).

def degreeOn (G : Multigraph V) [Fintype V] (v : V)
    (P : V → Prop) [DecidablePred P] : ℕ :=
  ∑ w ∈ Finset.univ.filter P, G.edgeMult v w

Uses 1 · Used by 4

Statement usesMultigraph

Used byDegree splits over a predicate and its complement · Restricted degree depends only on the neighbours · Isogeny volcano · Surface regularity of an isogeny volcano

DefinitionConnectivity of vertices in a multigraph#✓fully proved

Two vertices \(v\) and \(w\) of a multigraph \(G\) are connected when they are related by the reflexive-transitive closure of adjacency, that is, when there is a finite sequence of vertices \(v = u_0, u_1, \dots, u_k = w\) with \(k \ge 0\) and \(u_i\) adjacent to \(u_{i+1}\) for each \(i < k\).

def Connected (G : Multigraph V) (v w : V) : Prop :=
  Relation.ReflTransGen G.Adj v w

Uses 2 · Used by 2

Statement usesMultigraph · Adjacency in a multigraph

Used byEvery vertex is connected to itself · Connected multigraph

DefinitionConnected multigraph#✓fully proved

A multigraph \(G\) is connected when every two vertices \(v\) and \(w\) of \(G\) are joined by a walk, that is, \(w\) is reachable from \(v\) by a finite (possibly empty) sequence of steps along edges of positive multiplicity.

def IsConnected (G : Multigraph V) : Prop :=
  ∀ v w, G.Connected v w

Uses 2 · Used by 1

Statement usesMultigraph · Connectivity of vertices in a multigraph

Used byIsogeny volcano

TheoremSymmetry of adjacency in a multigraph#✓fully proved

In a multigraph \(G\), a vertex \(v\) is adjacent to a vertex \(w\) if and only if \(w\) is adjacent to \(v\).

theorem adj_comm (G : Multigraph V) (v w : V) :
    G.Adj v w ↔ G.Adj w v

Uses 2

Statement usesMultigraph · Adjacency in a multigraph

TheoremEvery vertex is connected to itself#✓fully proved

In a multigraph \(G\), every vertex \(v\) is connected to \(v\).

theorem connected_refl (G : Multigraph V) (v : V) :
    G.Connected v v

Uses 3

Statement usesMultigraph · Connectivity of vertices in a multigraph

Proof usesAdjacency in a multigraph

TheoremDegree splits over a predicate and its complement#✓fully proved

Let \(G\) be a multigraph on a finite vertex set \(V\), let \(v \in V\) and let \(P\) be a decidable predicate on \(V\). Then the degree of \(v\) equals the degree of \(v\) restricted to \(P\) plus the degree of \(v\) restricted to \(\neg P\).

theorem degreeOn_compl (G : Multigraph V) [Fintype V]
    (v : V) (P : V → Prop) [DecidablePred P] :
    G.degree v = G.degreeOn v P + G.degreeOn v (fun w => ¬ P w)

Uses 3

Statement usesMultigraph · Degree of a vertex in a multigraph · Degree restricted to a predicate

TheoremRestricted degree depends only on the neighbours#✓fully proved

Let \(G\) be a multigraph on a finite vertex set \(V\), let \(v \in V\) and let \(P\) and \(Q\) be decidable predicates on \(V\). If \(P(w) \iff Q(w)\) for every vertex \(w\) whose edge multiplicity with \(v\) is positive, then the degree of \(v\) restricted to \(P\) equals the degree of \(v\) restricted to \(Q\).

theorem degreeOn_congr (G : Multigraph V) [Fintype V]
    (v : V) {P Q : V → Prop}
    [DecidablePred P] [DecidablePred Q]
    (h : ∀ w, G.edgeMult v w > 0 → (P w ↔ Q w)) :
    G.degreeOn v P = G.degreeOn v Q

Uses 2 · Used by 1

Statement usesMultigraph · Degree restricted to a predicate

Used bySurface regularity of an isogeny volcano

StructureIsogeny volcano#✓fully proved

Let \(\ell\) be a prime. An \(\ell\)-isogeny volcano consists of a finite vertex set \(V\), a multigraph on \(V\) with edge multiplicities \(m(v, w)\), a depth \(d \in \mathbb{N}\), a surjective level map \(\mathrm{lev} : V \to \{0, 1, \dots, d\}\) and a surface degree \(s \in \mathbb{N}\) with \(s \le 2\), subject to the following conditions, where the surface is the set of vertices of level \(0\). Every surface vertex \(v\) satisfies \(\sum_{w \in V,\ \mathrm{lev}(w) = 0} m(v, w) = s\). Every vertex \(v\) of positive level has a unique parent: \(\sum_{w \in V,\ \mathrm{lev}(w) + 1 = \mathrm{lev}(v)} m(v, w) = 1\). Whenever \(m(v, w) > 0\), either \(v\) and \(w\) both lie on the surface or their levels differ by exactly one. Every vertex \(v\) with \(\mathrm{lev}(v) < d\) has degree \(\sum_{w \in V} m(v, w) = \ell + 1\), where a loop at \(v\) contributes its multiplicity once. Finally, the multigraph is connected: any two vertices are joined by a path along which consecutive vertices have positive edge multiplicity.

IsogenyVolcano · 41 lines

structure IsogenyVolcano (ℓ : ℕ) where
  /-- The isogeny degree is prime. -/
  prime : Nat.Prime ℓ
  /-- Vertex type. -/
  V : Type*
  /-- Finite vertices. -/
  instFintype : Fintype V
  /-- Decidable equality on vertices. -/
  instDecEq : DecidableEq V
  /-- Underlying multigraph. -/
  graph : Multigraph V
  /-- Depth of the volcano. -/
  depth : ℕ
  /-- Level of each vertex. -/
  level : V → Fin (depth + 1)
  /-- Every level is inhabited. -/
  level_surj : Function.Surjective level
  /-- Surface degree. -/
  surfaceDegree : ℕ
  /-- Surface degree is at most two. -/
  surfaceDegree_le : surfaceDegree ≤ 2
  /-- Surface regularity. -/
  surface_regular : ∀ v,
    level v = ⟨0, Nat.zero_lt_succ _⟩ →
      graph.degreeOn v
        (fun w => level w = ⟨0, Nat.zero_lt_succ _⟩) =
        surfaceDegree
  /-- Every nonsurface vertex has a unique parent. -/
  unique_parent : ∀ v, (level v : ℕ) > 0 →
    graph.degreeOn v
      (fun w => (level w : ℕ) + 1 = (level v : ℕ)) = 1
  /-- Positive edges stay within or across adjacent levels. -/
  edges_between_levels : ∀ v w, graph.edgeMult v w > 0 →
    ((level v : ℕ) = 0 ∧ (level w : ℕ) = 0) ∨
      (level w : ℕ) + 1 = (level v : ℕ) ∨
        (level v : ℕ) + 1 = (level w : ℕ)
  /-- Regularity below the floor. -/
  degree_eq : ∀ v, (level v : ℕ) < depth →
    graph.degree v = ℓ + 1
  /-- The graph is connected. -/
  connected : graph.IsConnected

Uses 4 · Used by 13

Statement usesMultigraph · Connected multigraph · Degree of a vertex in a multigraph · Degree restricted to a predicate

Used byReversing an ascending edge gives a descending edge · Reversing a descending edge gives an ascending edge · Every edge of an isogeny volcano is horizontal, descending or ascending · Ascending edge · Descending edge · Floor of a volcano · Floor vertices are those whose level equals the depth · Horizontal edge · Surface of a volcano · Surface vertices are those of level zero · Vertical edge · Surface regularity of an isogeny volcano · Depth of an isogeny volcano

DefinitionSurface of a volcano#✓fully proved

A vertex \(v\) of an \(\ell\)-isogeny volcano \(C\) lies on the surface of \(C\) when its level is \(0\).

def isSurface (C : IsogenyVolcano ℓ) (v : C.V) : Prop :=
  C.level v = 0

Uses 1 · Used by 2

Statement usesIsogeny volcano

Used bySurface vertices are those of level zero · Surface regularity of an isogeny volcano

DefinitionFloor of a volcano#✓fully proved

A vertex \(v\) of an \(\ell\)-isogeny volcano \(C\) of depth \(d\) lies on the floor of \(C\) when its level is \(d\), the last of the levels \(0, 1, \dots, d\).

def isFloor (C : IsogenyVolcano ℓ) (v : C.V) : Prop :=
  C.level v = Fin.last C.depth

Uses 1 · Used by 1

Statement usesIsogeny volcano

Used byFloor vertices are those whose level equals the depth

DefinitionDepth of an isogeny volcano#✓fully proved

The depth of an \(\ell\)-isogeny volcano \(C\) is the natural number \(d\) recorded in \(C\): the levels of the vertices of \(C\) are exactly \(0, 1, \dots, d\), with level \(0\) the surface and level \(d\) the floor.

def volcanoDepth (C : IsogenyVolcano ℓ) : ℕ :=
  C.depth

Uses 1

Statement usesIsogeny volcano

DefinitionHorizontal edge#✓fully proved

In an \(\ell\)-isogeny volcano \(C\), the pair \((v, w)\) of vertices is a horizontal edge when the edge multiplicity between \(v\) and \(w\) is positive and both \(v\) and \(w\) lie on the surface, that is, both have level \(0\).

def IsHorizontalEdge (C : IsogenyVolcano ℓ)
    (v w : C.V) : Prop :=
  C.graph.edgeMult v w > 0 ∧
    (C.level v : ℕ) = 0 ∧ (C.level w : ℕ) = 0

Uses 2 · Used by 1

Statement usesIsogeny volcano · Multigraph

Used byEvery edge of an isogeny volcano is horizontal, descending or ascending

DefinitionDescending edge#✓fully proved

In an \(\ell\)-isogeny volcano \(C\), the pair \((v, w)\) of vertices is a descending edge when the edge multiplicity between \(v\) and \(w\) is positive and \(w\) lies one level below \(v\), that is, the level of \(v\) plus one equals the level of \(w\) (level \(0\) being the surface).

def IsDescendingEdge (C : IsogenyVolcano ℓ)
    (v w : C.V) : Prop :=
  C.graph.edgeMult v w > 0 ∧
    (C.level v : ℕ) + 1 = (C.level w : ℕ)

Uses 2 · Used by 4

Statement usesIsogeny volcano · Multigraph

Used byReversing an ascending edge gives a descending edge · Reversing a descending edge gives an ascending edge · Every edge of an isogeny volcano is horizontal, descending or ascending · Vertical edge

DefinitionAscending edge#✓fully proved

In an \(\ell\)-isogeny volcano \(C\), the pair \((v, w)\) of vertices is an ascending edge when the edge multiplicity between \(v\) and \(w\) is positive and \(w\) lies one level above \(v\), that is, the level of \(w\) plus one equals the level of \(v\) (level \(0\) being the surface).

def IsAscendingEdge (C : IsogenyVolcano ℓ)
    (v w : C.V) : Prop :=
  C.graph.edgeMult v w > 0 ∧
    (C.level w : ℕ) + 1 = (C.level v : ℕ)

Uses 2 · Used by 4

Statement usesIsogeny volcano · Multigraph

Used byReversing an ascending edge gives a descending edge · Reversing a descending edge gives an ascending edge · Every edge of an isogeny volcano is horizontal, descending or ascending · Vertical edge

DefinitionVertical edge#✓fully proved

In an \(\ell\)-isogeny volcano \(C\), the pair \((v, w)\) of vertices is a vertical edge when it is a descending edge or an ascending edge, that is, when the edge multiplicity between \(v\) and \(w\) is positive and the levels of \(v\) and \(w\) differ by exactly one.

def IsVerticalEdge (C : IsogenyVolcano ℓ)
    (v w : C.V) : Prop :=
  C.IsDescendingEdge v w ∨ C.IsAscendingEdge v w

Uses 3

Statement usesIsogeny volcano · Ascending edge · Descending edge

TheoremReversing a descending edge gives an ascending edge#✓fully proved

In an \(\ell\)-isogeny volcano, for vertices \(v\) and \(w\), \((v, w)\) is a descending edge if and only if \((w, v)\) is an ascending edge.

theorem descending_iff_ascending_symm (v w : C.V) :
    C.IsDescendingEdge v w ↔ C.IsAscendingEdge w v

Uses 4

Statement usesIsogeny volcano · Ascending edge · Descending edge

Proof usesMultigraph

TheoremReversing an ascending edge gives a descending edge#✓fully proved

In an \(\ell\)-isogeny volcano, for vertices \(v\) and \(w\), \((v, w)\) is an ascending edge if and only if \((w, v)\) is a descending edge.

theorem ascending_iff_descending_symm (v w : C.V) :
    C.IsAscendingEdge v w ↔ C.IsDescendingEdge w v

Uses 4

Statement usesIsogeny volcano · Ascending edge · Descending edge

Proof usesMultigraph

TheoremEvery edge of an isogeny volcano is horizontal, descending or ascending#✓fully proved

Let \(C\) be an \(\ell\)-isogeny volcano, with levels numbered from \(0\) at the surface, and let \(v, w\) be vertices of \(C\) whose edge multiplicity is positive. Then \((v, w)\) is a horizontal edge (both \(v\) and \(w\) have level \(0\)), a descending edge (the level of \(w\) is the level of \(v\) plus one) or an ascending edge (the level of \(v\) is the level of \(w\) plus one).

theorem edge_direction (v w : C.V)
    (h : C.graph.edgeMult v w > 0) :
    C.IsHorizontalEdge v w ∨ C.IsDescendingEdge v w ∨
      C.IsAscendingEdge v w

Uses 5

Statement usesIsogeny volcano · Ascending edge · Descending edge · Horizontal edge · Multigraph

TheoremSurface vertices are those of level zero#✓fully proved

A vertex \(v\) of an \(\ell\)-isogeny volcano \(C\) lies on the surface of \(C\) if and only if the level of \(v\), as a natural number, is \(0\).

@[simp] theorem isSurface_iff (v : C.V) :
    C.isSurface v ↔ (C.level v : ℕ) = 0

Uses 2 · Used by 1

Statement usesIsogeny volcano · Surface of a volcano

Used bySurface regularity of an isogeny volcano

TheoremFloor vertices are those whose level equals the depth#✓fully proved

A vertex \(v\) of an \(\ell\)-isogeny volcano \(C\) lies on the floor of \(C\) if and only if the level of \(v\), as a natural number, equals the depth of \(C\).

@[simp] theorem isFloor_iff (v : C.V) :
    C.isFloor v ↔ (C.level v : ℕ) = C.depth

Uses 2

Statement usesIsogeny volcano · Floor of a volcano

TheoremSurface regularity of an isogeny volcano#✓fully proved

Let \(C\) be an \(\ell\)-isogeny volcano with edge multiplicities \(m\) and surface degree \(s\). For every surface vertex \(v\) of \(C\), that is, every vertex of level \(0\), the sum of \(m(v, w)\) over all surface vertices \(w\) of \(C\) equals \(s\).

This restates the surface-regularity condition of an isogeny volcano in terms of the surface predicate.

@[simp] theorem surface_degreeOn (v : C.V) (hv : C.isSurface v) :
    C.graph.degreeOn v (fun w => C.isSurface w) = C.surfaceDegree

Uses 6

Statement usesIsogeny volcano · Surface of a volcano · Multigraph · Degree restricted to a predicate

Proof usesSurface vertices are those of level zero · Restricted degree depends only on the neighbours

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.