Iterated vertex gluing and the chain transmission theorem

This is the assembly layer for Section 6 of the twice-marked banana paper: the iterated vertex gluing of a chain of twice-marked graphs, and the transport of TransmissionExistence along it.

What is here and what it rests on

TransmissionWedgeDemazure already proves the two-factor step: opposite-side wedge addition composes two transmission witnesses by the Demazure product (satisfiesTransmission_wedgeAddDivisor_star, the paper's eq:tauGlued), and the existential form of the same (transmissionExistence_vertexWedge_opposite_of_factorizations) is conditional on one named input, HasBoundedDemazureFactorizations: every finite ASP permutation whose inversion length fits inside gG + gH splits as a Demazure product of two factors of lengths at most gG and gH.

This file iterates that step along a chain, so the chain theorem is reduced to exactly the same single input and nothing else. chainTransmissionExistence below is the ℓ-fold statement; the two-factor case is the existing theorem.

The bounded factorization property is an explicit hypothesis of this module's general gluing theorem. Demazure.Avoiding321.dprod_eq_iff supplies the factorization criterion used by its consumers.

Universes

vertexWedge lands in CFGraph.{max u v}, so iterating it in full universe generality would raise the level at every step. Everything here therefore works with all factors in a single fixed universe, where the wedge is closed.

structure Utilities.MarkedGraph : Type (u + 1)

A twice-marked graph, bundled so that an iterated wedge can change the vertex type at every step.

• graph : CFGraph

  The underlying graph of a chain factor with ordered attachment marks.

• left : self.graph.V

  The outside left mark retained when the factor is glued to another on its right.

• right : self.graph.V

  The outside right mark used to attach the next chain factor.

def Utilities.MarkedGraph.wedge (M N : MarkedGraph) : MarkedGraph

Glue the right mark of M to the left mark of N. The result keeps the left mark of M and the right mark of N, which is the marking the Demazure composition theorem produces.

Equations

• M.wedge N = { graph := Utilities.vertexWedge M.graph N.graph M.right N.left, left := Sum.inl M.left, right := Utilities.wedgeRightVertex M.graph N.graph M.right N.left N.right }

@[simp]

theorem Utilities.MarkedGraph.genus_wedge (M N : MarkedGraph) : (M.wedge N).graph.genus = M.graph.genus + N.graph.genus

def Utilities.MarkedGraph.chain (M : MarkedGraph) : List MarkedGraph → MarkedGraph

The left-associated iterated vertex gluing of a chain, growing to the right. chain M [] is M, and each further factor is glued onto the accumulated right mark.

Equations

• M.chain [] = M
• M.chain (N :: rest) = (M.wedge N).chain rest

@[simp]

theorem Utilities.MarkedGraph.chain_nil (M : MarkedGraph) : M.chain [] = M

@[simp]

theorem Utilities.MarkedGraph.chain_cons (M N : MarkedGraph) (rest : List MarkedGraph) : M.chain (N :: rest) = (M.wedge N).chain rest

theorem Utilities.MarkedGraph.genus_chain (M : MarkedGraph) (L : List MarkedGraph) : (M.chain L).graph.genus = M.graph.genus + (List.map (fun (N : MarkedGraph) => N.graph.genus) L).sum

Genera add along a chain: vertex identification creates no cycle.

def Utilities.HasAllBoundedDemazureFactorizations : Prop

The bounded Demazure factorization input, at every pair of budgets.

HasBoundedDemazureFactorizations is stated for one pair (gG, gH); the chain induction meets a new pair at every step, so it needs the uniform version.

Equations

• Utilities.HasAllBoundedDemazureFactorizations = ∀ (gG gH : ℤ), Utilities.HasBoundedDemazureFactorizations gG gH

theorem Utilities.chainTransmissionExistence (hFactor : HasAllBoundedDemazureFactorizations) (M : MarkedGraph) (L : List MarkedGraph) (hM : TransmissionExistence M.graph M.left M.right) (hL : ∀ N ∈ L, TransmissionExistence N.graph N.left N.right) : TransmissionExistence (M.chain L).graph (M.chain L).left (M.chain L).right

Chain gluing for transmission existence.

If every factor of a chain has transmission existence at its own two marks, then so does the whole chain at the two outer marks. This is the ℓ-fold form of transmissionExistence_vertexWedge_opposite_of_factorizations, and rests on the same single input.

This is the transmission half of thm:bngChain (Theorem 1.13).

theorem Utilities.onceMarkedBNExists_chain (hFactor : HasAllBoundedDemazureFactorizations) (M : MarkedGraph) (L : List MarkedGraph) (hM : TransmissionExistence M.graph M.left M.right) (hL : ∀ N ∈ L, TransmissionExistence N.graph N.left N.right) (hconn : graphConnected (M.chain L).graph) (tau : AspPerm) (lambda : YoungDiagram) (hProfile : GrassmannianPartitionProfile tau lambda) (hFinite : FiniteTransmissionPerm tau) (hLength : ↑(invSet tau.func).ncard ≤ (M.chain L).graph.genus) : OnceMarkedBNExists (M.chain L).graph (M.chain L).left lambda

Chain gluing for once-marked Brill--Noether existence.

The once-marked corollary of the chain theorem: if the chain's transmission existence holds and the ASP permutation attached to a partition has the Grassmannian profile, then the glued graph realizes that partition at its left mark.

This is the shape in which thm:bngChain is used downstream — the partition side is supplied by transmissionExists_iff_onceMarkedBNExists, the chain side by chainTransmissionExistence.