Documentation

LeanPool.BrillNoetherGraphs.Utilities.Subdivision.LeafExtension

Divisor rank under adjoining a leaf #

This module isolates the pendant-tree reduction needed before a finite stable core classification. The graph addLeaf H root adjoins one new vertex and a single edge from it to root. Divisors extend by zero to the new leaf, while divisors on the extension retract by moving the leaf coefficient to root. These operations preserve degree, linear equivalence, winnability, and rank.

The resulting rank-one interface shows that adjoining or pruning a leaf does not change divisorial gonality.

source
def Utilities.Certificate.LeafExtension.liftEdge (H : CFGraph) (edge : H.V × H.V) :
Option H.V × Option H.V

Lift both endpoints of an old edge into the graph with an added leaf.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev Utilities.Certificate.LeafExtension.addLeaf (H : CFGraph) (root : H.V) :
    CFGraph

    Adjoin a new leaf none to the old vertex some root.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem Utilities.Certificate.LeafExtension.addLeaf_edges (H : CFGraph) (root : H.V) :
      (addLeaf H root).edges = (none, some root) ::ₘ Multiset.map (liftEdge H) H.edges
      source
      @[simp]
      theorem Utilities.Certificate.LeafExtension.num_edges_some_some (H : CFGraph) (root x y : H.V) :
      numEdges (addLeaf H root) (some x) (some y) = numEdges H x y

      Old-old edge multiplicities are unchanged.

      source
      @[simp]
      theorem Utilities.Certificate.LeafExtension.num_edges_none_some (H : CFGraph) (root x : H.V) :
      numEdges (addLeaf H root) none (some x) = if x = root then 1 else 0

      The new leaf has one edge to root and none to another old vertex.

      source
      @[simp]
      theorem Utilities.Certificate.LeafExtension.num_edges_some_none (H : CFGraph) (root x : H.V) :
      numEdges (addLeaf H root) (some x) none = if x = root then 1 else 0
      source
      @[simp]
      theorem Utilities.Certificate.LeafExtension.genus_addLeaf (H : CFGraph) (root : H.V) :
      (addLeaf H root).genus = H.genus

      Adjoining one vertex and one edge preserves genus.

      source
      theorem Utilities.Certificate.LeafExtension.graph_connected_addLeaf (H : CFGraph) (root : H.V) (hH : graphConnected H) :
      graphConnected (addLeaf H root)

      A connected graph remains connected after adjoining a leaf.

      source
      def Utilities.Certificate.LeafExtension.extendDiv (H : CFGraph) (root : H.V) (D : CFDiv H) :
      CFDiv (addLeaf H root)

      Extend an old divisor by zero at the new leaf.

      Equations
      Instances For
        source
        def Utilities.Certificate.LeafExtension.extendScript (H : CFGraph) (root : H.V) (script : firingScript H) :
        firingScript (addLeaf H root)

        Extend a firing script constantly across the new leaf edge.

        Equations
        Instances For
          source
          @[simp]
          theorem Utilities.Certificate.LeafExtension.extendDiv_none (H : CFGraph) (root : H.V) (D : CFDiv H) :
          extendDiv H root D none = 0
          source
          @[simp]
          theorem Utilities.Certificate.LeafExtension.extendDiv_some (H : CFGraph) (root : H.V) (D : CFDiv H) (x : H.V) :
          extendDiv H root D (some x) = D x
          source
          @[simp]
          theorem Utilities.Certificate.LeafExtension.extendScript_none (H : CFGraph) (root : H.V) (script : firingScript H) :
          extendScript H root script none = script root
          source
          @[simp]
          theorem Utilities.Certificate.LeafExtension.extendScript_some (H : CFGraph) (root : H.V) (script : firingScript H) (x : H.V) :
          extendScript H root script (some x) = script x
          source
          @[simp]
          theorem Utilities.Certificate.LeafExtension.extendDiv_zero (H : CFGraph) (root : H.V) :
          extendDiv H root 0 = 0
          source
          @[simp]
          theorem Utilities.Certificate.LeafExtension.extendDiv_add (H : CFGraph) (root : H.V) (D E : CFDiv H) :
          extendDiv H root (D + E) = extendDiv H root D + extendDiv H root E
          source
          @[simp]
          theorem Utilities.Certificate.LeafExtension.extendDiv_sub (H : CFGraph) (root : H.V) (D E : CFDiv H) :
          extendDiv H root (D - E) = extendDiv H root D - extendDiv H root E
          source
          @[simp]
          theorem Utilities.Certificate.LeafExtension.extendDiv_one_chip (H : CFGraph) (root x : H.V) :
          extendDiv H root (oneChip x) = oneChip (some x)
          source
          theorem Utilities.Certificate.LeafExtension.effective_extendDiv (H : CFGraph) (root : H.V) {D : CFDiv H} (hD : effective D) :
          effective (extendDiv H root D)

          Extending by zero preserves effectivity.

          source
          @[simp]
          theorem Utilities.Certificate.LeafExtension.deg_extendDiv (H : CFGraph) (root : H.V) (D : CFDiv H) :
          CFDiv.degree (extendDiv H root D) = CFDiv.degree D

          Extending by zero preserves divisor degree.

          source
          theorem Utilities.Certificate.LeafExtension.extendDiv_prin (H : CFGraph) (root : H.V) (script : firingScript H) :
          extendDiv H root ((prin H) script) = (prin (addLeaf H root)) (extendScript H root script)

          Constant extension of a firing script has zero Laplacian at the leaf and the old Laplacian at every old vertex.

          source
          theorem Utilities.Certificate.LeafExtension.linearEquiv_extendDiv (H : CFGraph) (root : H.V) {D E : CFDiv H} (hEquiv : linearEquiv H D E) :
          linearEquiv (addLeaf H root) (extendDiv H root D) (extendDiv H root E)

          Linear equivalence transports from the old graph to its leaf extension.

          source
          theorem Utilities.Certificate.LeafExtension.winnable_extendDiv (H : CFGraph) (root : H.V) {D : CFDiv H} (hWin : winnable H D) :
          winnable (addLeaf H root) (extendDiv H root D)

          A winnable old divisor stays winnable after extension by zero.

          source
          def Utilities.Certificate.LeafExtension.leafMoveScript (H : CFGraph) (root : H.V) :
          firingScript (addLeaf H root)

          Script which moves one removed-chip test from root to the new leaf.

          Equations
          Instances For
            source
            theorem Utilities.Certificate.LeafExtension.prin_leafMoveScript (H : CFGraph) (root : H.V) :
            (prin (addLeaf H root)) (leafMoveScript H root) = oneChip (some root) - oneChip none
            source
            theorem Utilities.Certificate.LeafExtension.sub_root_linearEquiv_sub_leaf (H : CFGraph) (root : H.V) (D : CFDiv H) :
            linearEquiv (addLeaf H root) (extendDiv H root D - oneChip (some root)) (extendDiv H root D - oneChip none)

            Removing a chip at the old root or at the new leaf gives linearly equivalent divisors on the leaf extension.

            source
            theorem Utilities.Certificate.LeafExtension.rank_ge_one_addLeaf (H : CFGraph) (root : H.V) {D : CFDiv H} (hRank : rank H D ≥ 1) :
            rank (addLeaf H root) (extendDiv H root D) ≥ 1

            Rank-one lower bounds survive adjoining a leaf.

            source
            theorem Utilities.Certificate.LeafExtension.bnExists_rank_one_addLeaf (H : CFGraph) (root : H.V) {d : ℤ} :
            BNExists H 1 d → BNExists (addLeaf H root) 1 d

            A degree-d, rank-one divisor remains such after adjoining a leaf.

            Retracting the added leaf #

            source
            def Utilities.Certificate.LeafExtension.retractDiv (H : CFGraph) (root : H.V) (E : CFDiv (addLeaf H root)) :
            CFDiv H

            Move the coefficient at the new leaf into its old neighbour.

            Equations
            Instances For
              source
              @[simp]
              theorem Utilities.Certificate.LeafExtension.retractDiv_apply (H : CFGraph) (root : H.V) (E : CFDiv (addLeaf H root)) (x : H.V) :
              retractDiv H root E x = E (some x) + if x = root then E none else 0
              source
              def Utilities.Certificate.LeafExtension.retractScript (H : CFGraph) (root : H.V) (script : firingScript (addLeaf H root)) :
              firingScript H

              Restrict a firing script from a leaf extension to the old vertices.

              Equations
              Instances For
                source
                @[simp]
                theorem Utilities.Certificate.LeafExtension.retractDiv_extendDiv (H : CFGraph) (root : H.V) (D : CFDiv H) :
                retractDiv H root (extendDiv H root D) = D
                source
                @[simp]
                theorem Utilities.Certificate.LeafExtension.retractDiv_add (H : CFGraph) (root : H.V) (E F : CFDiv (addLeaf H root)) :
                retractDiv H root (E + F) = retractDiv H root E + retractDiv H root F
                source
                @[simp]
                theorem Utilities.Certificate.LeafExtension.retractDiv_sub (H : CFGraph) (root : H.V) (E F : CFDiv (addLeaf H root)) :
                retractDiv H root (E - F) = retractDiv H root E - retractDiv H root F
                source
                theorem Utilities.Certificate.LeafExtension.retractDiv_prin (H : CFGraph) (root : H.V) (script : firingScript (addLeaf H root)) :
                retractDiv H root ((prin (addLeaf H root)) script) = (prin H) (retractScript H root script)

                Retraction commutes with principal divisors. The leaf-edge contribution cancels between the root and the leaf.

                source
                theorem Utilities.Certificate.LeafExtension.linearEquiv_retractDiv (H : CFGraph) (root : H.V) {E F : CFDiv (addLeaf H root)} (hEquiv : linearEquiv (addLeaf H root) E F) :
                linearEquiv H (retractDiv H root E) (retractDiv H root F)

                Linear equivalence on a leaf extension retracts to linear equivalence on the original graph.

                source
                theorem Utilities.Certificate.LeafExtension.effective_retractDiv (H : CFGraph) (root : H.V) {E : CFDiv (addLeaf H root)} (hE : effective E) :
                effective (retractDiv H root E)

                Retraction of an effective divisor across the leaf is effective.

                source
                theorem Utilities.Certificate.LeafExtension.winnable_retractDiv (H : CFGraph) (root : H.V) {E : CFDiv (addLeaf H root)} (hWin : winnable (addLeaf H root) E) :
                winnable H (retractDiv H root E)

                Winnability on a leaf extension retracts to the original graph.

                source
                @[simp]
                theorem Utilities.Certificate.LeafExtension.deg_retractDiv (H : CFGraph) (root : H.V) (E : CFDiv (addLeaf H root)) :
                CFDiv.degree (retractDiv H root E) = CFDiv.degree E

                Moving all leaf chips to the root preserves divisor degree.

                source
                theorem Utilities.Certificate.LeafExtension.linearEquiv_retractDiv_extendDiv (H : CFGraph) (root : H.V) (E : CFDiv (addLeaf H root)) :
                linearEquiv (addLeaf H root) E (extendDiv H root (retractDiv H root E))

                The leaf transfer identifies every divisor with the zero extension of its retraction, up to linear equivalence.

                source
                theorem Utilities.Certificate.LeafExtension.rank_geq_addLeaf (H : CFGraph) (root : H.V) {D : CFDiv H} {k : ℤ} (hRank : rankGeq H D k) :
                rankGeq (addLeaf H root) (extendDiv H root D) k

                Zero extension preserves every rank lower bound.

                source
                theorem Utilities.Certificate.LeafExtension.rank_geq_of_addLeaf (H : CFGraph) (root : H.V) {D : CFDiv H} {k : ℤ} (hRank : rankGeq (addLeaf H root) (extendDiv H root D) k) :
                rankGeq H D k

                Every rank lower bound of a zero-extended divisor is already witnessed on the original graph.

                source
                theorem Utilities.Certificate.LeafExtension.rank_geq_addLeaf_iff (H : CFGraph) (root : H.V) (D : CFDiv H) (k : ℤ) :
                rankGeq (addLeaf H root) (extendDiv H root D) k ↔ rankGeq H D k

                Zero extension preserves and reflects every rank lower bound.

                source
                theorem Utilities.Certificate.LeafExtension.rank_addLeaf (H : CFGraph) (root : H.V) (D : CFDiv H) :
                rank (addLeaf H root) (extendDiv H root D) = rank H D

                Zero extension preserves divisor rank.

                source
                theorem Utilities.Certificate.LeafExtension.rank_retractDiv (H : CFGraph) (root : H.V) (E : CFDiv (addLeaf H root)) :
                rank H (retractDiv H root E) = rank (addLeaf H root) E

                Retraction across the added leaf preserves divisor rank.

                source
                theorem Utilities.Certificate.LeafExtension.bnExists_addLeaf_iff (H : CFGraph) (root : H.V) (r d : ℤ) :
                BNExists (addLeaf H root) r d ↔ BNExists H r d

                Brill--Noether existence in every rank and degree is invariant under adjoining a leaf.

                The public collapse interface #

                source
                def Utilities.Certificate.LeafExtension.collapseDiv (H : CFGraph) (root : H.V) (D : CFDiv (addLeaf H root)) :
                CFDiv H

                Collapse the added leaf onto its root.

                Equations
                Instances For
                  source
                  theorem Utilities.Certificate.LeafExtension.rank_collapseDiv (H : CFGraph) (root : H.V) (D : CFDiv (addLeaf H root)) :
                  rank H (collapseDiv H root D) = rank (addLeaf H root) D

                  Collapsing the leaf preserves divisor rank exactly.

                  source
                  theorem Utilities.Certificate.LeafExtension.prin_collapse (H : CFGraph) (root : H.V) (script : firingScript (addLeaf H root)) :
                  collapseDiv H root ((prin (addLeaf H root)) script) = (prin H) fun (w : H.V) => script (some w)

                  Collapsing a principal divisor restricts its firing script to the old vertices.

                  source
                  theorem Utilities.Certificate.LeafExtension.effective_collapseDiv (H : CFGraph) (root : H.V) {D : CFDiv (addLeaf H root)} (hD : effective D) :
                  effective (collapseDiv H root D)

                  Collapsing an effective divisor preserves effectivity.

                  source
                  theorem Utilities.Certificate.LeafExtension.rank_ge_one_collapseDiv (H : CFGraph) (root : H.V) {D : CFDiv (addLeaf H root)} (hRank : rank (addLeaf H root) D ≥ 1) :
                  rank H (collapseDiv H root D) ≥ 1

                  Rank one descends when the added leaf is collapsed.

                  source
                  theorem Utilities.Certificate.LeafExtension.bnExists_rank_one_of_addLeaf (H : CFGraph) (root : H.V) {d : ℤ} :
                  BNExists (addLeaf H root) 1 d → BNExists H 1 d

                  Rank-one Brill--Noether existence descends when the added leaf is collapsed.

                  source
                  theorem Utilities.Certificate.LeafExtension.divisorialGonality_addLeaf (H : CFGraph) (root : H.V) (hconn : graphConnected H) :
                  Gonality.divisorialGonality (addLeaf H root) = Gonality.divisorialGonality H

                  Adjoining one leaf does not change divisorial gonality.