Bridge Chain Transport

@[reducible, inline]

abbrev Utilities.MarkedGraph.bridge (M N : MarkedGraph) : MarkedGraph

Join the right mark of the first graph to the left mark of the second by a bridge, retaining the outer marks.

Equations

• M.bridge N = { graph := Utilities.bridgeGraph M.graph N.graph M.right N.left, left := Sum.inl M.left, right := Sum.inr N.right }

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

Attach each graph in the list by a bridge, starting from the given marked graph.

Equations

• M.bridgeChain [] = M
• M.bridgeChain (N :: rest) = (M.bridge N).bridgeChain rest

noncomputable def Bananas.bridgeWedgeAssocIso (M N K : Utilities.MarkedGraph) : Utilities.CFGraphIso ((M.bridge N).wedge K).graph (M.bridge (N.wedge K)).graph

Reassociate a bridge followed by a vertex wedge without changing the graph.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Bananas.bridgeWedgeAssocIso_apply_left (M N K : Utilities.MarkedGraph) : (bridgeWedgeAssocIso M N K).vertexEquiv ((M.bridge N).wedge K).left = (M.bridge (N.wedge K)).left

@[simp]

theorem Bananas.bridgeWedgeAssocIso_apply_right (M N K : Utilities.MarkedGraph) : (bridgeWedgeAssocIso M N K).vertexEquiv ((M.bridge N).wedge K).right = (M.bridge (N.wedge K)).right

Rank-preserving transport with a distinguished left mark

structure Bananas.LeftMarkedIso (M N : Utilities.MarkedGraph) : Type u

A graph isomorphism which also carries the displayed left mark.

• iso : Utilities.CFGraphIso M.graph N.graph

  The underlying graph isomorphism that carries the left mark.

• map_left : self.iso.vertexEquiv M.left = N.left

noncomputable def Bananas.LeftMarkedIso.refl (M : Utilities.MarkedGraph) : LeftMarkedIso M M

The identity graph isomorphism with its left mark fixed.

Equations

• Bananas.LeftMarkedIso.refl M = { iso := Utilities.CFGraphIso.refl M.graph, map_left := ⋯ }

noncomputable def Bananas.LeftMarkedIso.symm {M N : Utilities.MarkedGraph} (phi : LeftMarkedIso M N) : LeftMarkedIso N M

Invert a graph isomorphism that preserves the left mark.

Equations

• phi.symm = { iso := phi.iso.symm, map_left := ⋯ }

noncomputable def Bananas.LeftMarkedIso.trans {M N K : Utilities.MarkedGraph} (phi : LeftMarkedIso M N) (psi : LeftMarkedIso N K) : LeftMarkedIso M K

Compose two graph isomorphisms that preserve the left mark.

Equations

• phi.trans psi = { iso := phi.iso.trans psi.iso, map_left := ⋯ }

def Bananas.rightChain (M : Utilities.MarkedGraph) : List Utilities.MarkedGraph → Utilities.MarkedGraph

The fully right-associated vertex-wedge chain.

Equations

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

noncomputable def Bananas.rightChainIso (M : Utilities.MarkedGraph) (rest : List Utilities.MarkedGraph) : LeftMarkedIso (M.chain rest) (rightChain M rest)

Reassociate the library's left-associated chain all the way to the right, retaining its outside left mark.

Equations

• One or more equations did not get rendered due to their size.
• Bananas.rightChainIso M [] = Bananas.LeftMarkedIso.refl M

noncomputable def Bananas.bridgeWedgeAssocLeftIso (M N K : Utilities.MarkedGraph) : LeftMarkedIso ((M.bridge N).wedge K) (M.bridge (N.wedge K))

The bridge/wedge reassociation as an isomorphism preserving the outside left mark.

Equations

• Bananas.bridgeWedgeAssocLeftIso M N K = { iso := Bananas.bridgeWedgeAssocIso M N K, map_left := ⋯ }

structure Bananas.LeftRankTransport (M N : Utilities.MarkedGraph) : Type u

A divisor map preserving degree, rank, genus, and the distinguished one-chip divisor. This is exactly the interface needed to transport both ordinary and once-marked Brill--Noether statements.

• mapDiv : CFDiv M.graph → CFDiv N.graph

  Transport divisors while preserving subtraction, integer scaling, degree, rank, and the chip at the left mark.

• map_sub (D E : CFDiv M.graph) : self.mapDiv (D - E) = self.mapDiv D - self.mapDiv E
• map_zsmul (n : ℤ) (D : CFDiv M.graph) : self.mapDiv (n • D) = n • self.mapDiv D
• map_one_chip : self.mapDiv (oneChip M.left) = oneChip N.left
• deg_map (D : CFDiv M.graph) : CFDiv.degree (self.mapDiv D) = CFDiv.degree D
• rank_map (D : CFDiv M.graph) : rank N.graph (self.mapDiv D) = rank M.graph D
• genus_eq : N.graph.genus = M.graph.genus

noncomputable def Bananas.LeftRankTransport.ofIso {M N : Utilities.MarkedGraph} (phi : LeftMarkedIso M N) : LeftRankTransport M N

Transport divisors along a graph isomorphism preserving the left mark.

Equations

• Bananas.LeftRankTransport.ofIso phi = { mapDiv := ⇑phi.iso.mapDiv, map_sub := ⋯, map_zsmul := ⋯, map_one_chip := ⋯, deg_map := ⋯, rank_map := ⋯, genus_eq := ⋯ }

noncomputable def Bananas.LeftRankTransport.trans {M N K : Utilities.MarkedGraph} (first : LeftRankTransport M N) (second : LeftRankTransport N K) : LeftRankTransport M K

Compose two transports of divisor rank and left-marked chips.

Equations

• first.trans second = { mapDiv := fun (D : CFDiv M.graph) => second.mapDiv (first.mapDiv D), map_sub := ⋯, map_zsmul := ⋯, map_one_chip := ⋯, deg_map := ⋯, rank_map := ⋯, genus_eq := ⋯ }

noncomputable def Bananas.contractBridgeTransport (M N : Utilities.MarkedGraph) : LeftRankTransport (M.bridge N) (M.wedge N)

Contract the bridge between two marked factors.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Bananas.contractInitialBridge (M N : Utilities.MarkedGraph) (rest : List Utilities.MarkedGraph) : LeftRankTransport ((M.bridge N).chain rest) ((M.wedge N).chain rest)

Move the initial bridge of a wedge-chain to the outside and contract it.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Bananas.contractBridgeChain (M : Utilities.MarkedGraph) (rest : List Utilities.MarkedGraph) : LeftRankTransport (M.bridgeChain rest) (M.chain rest)

Contract every separating edge in the displayed bridge chain.

Equations

• Bananas.contractBridgeChain M [] = Bananas.LeftRankTransport.ofIso (Bananas.LeftMarkedIso.refl M)
• Bananas.contractBridgeChain M (N :: rest) = (Bananas.contractBridgeChain (M.bridge N) rest).trans (Bananas.contractInitialBridge M N rest)