Documentation

LeanPool.BrillNoetherGraphs.Utilities.Subdivision.SubdivisionCoreSupport

Core-supported rank-one divisors on subdivisions #

The embedded core vertices of a positive subdivision are a strong separator. Thus a particularly small uniform rank-one witness is available whenever one can put a positive number of chips at every core vertex. This module records that observation without referring to a genus, a trivalence hypothesis, or a certificate search.

The first theorem is deliberately graph-theoretic: an effective divisor with at least one chip at every member of a certified strong separator has rank at least one. The subdivision theorems specialize it to the transparent divisor which is zero on every edge-interior vertex.

source
theorem Utilities.Subdivision.SubdivisionCoreSupport.rank_ge_one_of_effective_positive_on_strongSeparator {G : CFGraph} (hConnected : graphConnected G) {S : Finset G.V} (hSNonempty : S.Nonempty) (hSeparator : Certificate.StrongSeparator.StrongSeparatorCertificate G S) {D : CFDiv G} (hEffective : effective D) (hPositive : ∀ s ∈ S, 1 ≤ D s) :
rank G D ≥ 1

A positive effective representative already reaches each vertex at which it carries a chip. Consequently positivity on a strong separator proves rank at least one.

source
def Utilities.Subdivision.SubdivisionCoreSupport.coreDivisor {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (weight : Fin n → ℤ) :
CFDiv spec.graph

The divisor which places weight vertex chips at each embedded core vertex and no chips at subdivision-interior vertices.

Equations
Instances For
    source
    @[simp]
    theorem Utilities.Subdivision.SubdivisionCoreSupport.coreDivisor_coreVertex {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (weight : Fin n → ℤ) (vertex : Fin n) :
    coreDivisor spec weight (spec.coreVertex vertex) = weight vertex
    source
    @[simp]
    theorem Utilities.Subdivision.SubdivisionCoreSupport.coreDivisor_interiorVertex {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (weight : Fin n → ℤ) (edge : Fin p) (offset : Fin (spec.length edge - 1)) :
    coreDivisor spec weight (spec.interiorVertex edge offset) = 0
    source
    theorem Utilities.Subdivision.SubdivisionCoreSupport.coreDivisor_effective {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (weight : Fin n → ℤ) (hNonnegative : ∀ (vertex : Fin n), 0 ≤ weight vertex) :
    effective (coreDivisor spec weight)

    Nonnegative core weights make the core-supported divisor effective.

    source
    @[simp]
    theorem Utilities.Subdivision.SubdivisionCoreSupport.deg_coreDivisor {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (weight : Fin n → ℤ) :
    CFDiv.degree (coreDivisor spec weight) = ∑ vertex : Fin n, weight vertex

    The degree of the core-supported divisor is exactly the sum of its core weights; subdivision-interior vertices contribute zero.

    source
    theorem Utilities.Subdivision.SubdivisionCoreSupport.rank_ge_one_coreDivisor {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (weight : Fin n → ℤ) (hConnected : graphConnected spec.graph) (hPositive : ∀ (vertex : Fin n), 1 ≤ weight vertex) :
    rank spec.graph (coreDivisor spec weight) ≥ 1

    Positive core weights on a connected positive subdivision give a rank-one divisor, uniformly over all edge lengths.

    source
    theorem Utilities.Subdivision.SubdivisionCoreSupport.bnExists_coreDivisor {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (weight : Fin n → ℤ) (degree : ℤ) (hDegree : ∑ vertex : Fin n, weight vertex = degree) (hConnected : graphConnected spec.graph) (hPositive : ∀ (vertex : Fin n), 1 ≤ weight vertex) :
    BNExists spec.graph 1 degree

    Advertise the core-supported rank-one witness at its exact total degree. This is useful for uniform families: only connectedness and positivity of the core weights remain as hypotheses.

    source
    def Utilities.Subdivision.SubdivisionCoreSupport.degreeWeight {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (degree : ℤ) :
    Fin n → ℤ

    Put one chip at every core vertex and place all remaining degree at the first core vertex. The core is nonempty by definition of a subdivision specification.

    Equations
    Instances For
      source
      @[simp]
      theorem Utilities.Subdivision.SubdivisionCoreSupport.sum_degreeWeight {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (degree : ℤ) :
      ∑ vertex : Fin n, degreeWeight spec degree vertex = degree
      source
      theorem Utilities.Subdivision.SubdivisionCoreSupport.degreeWeight_positive {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (degree : ℤ) (hDegree : ↑n ≤ degree) (vertex : Fin n) :
      1 ≤ degreeWeight spec degree vertex
      source
      theorem Utilities.Subdivision.SubdivisionCoreSupport.bnExists_of_coreVertexCount_le_degree {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (degree : ℤ) (hConnected : graphConnected spec.graph) (hDegree : ↑n ≤ degree) :
      BNExists spec.graph 1 degree

      Core-cardinality criterion. A connected subdivision with at most degree embedded core vertices has a rank-one divisor of that degree. This is the certificate-free form of the all-supported sparse-potential pattern.

      source
      theorem Utilities.Subdivision.SubdivisionCoreSupport.bnExists_of_coreVertexCount_le_degree_of_coreConnected {n p : ℕ} (spec : Certificate.SubdivisionGraph.Spec n p) (degree : ℤ) (hCoreConnected : spec.core.Connected) (hDegree : ↑n ≤ degree) :
      BNExists spec.graph 1 degree

      Finite-core-facing form of the core-cardinality criterion.