Documentation

LeanPool.BrillNoetherGraphs.Bananas.Theta.ThetaNegativeDivisorClassesBoundary

Boundary negative divisor classes on theta graphs #

This extends the class-valued bijection in Theorem 3.4 to the first genuine boundary family: the first mark is the raw initial endpoint and the second is an interior point at least two steps before the terminal endpoint. The two excluded terminal-near positions are precisely the all-submodular cases of Corollary 3.6.

source
theorem Bananas.rankDelta_path_pair_neg_of_mem_thetaExceptionalPositions_zero_left (B : Banana 2) (alpha : Fin 3) (j k : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B alpha j) (hjFar : ↑j + 1 < B.length alpha) (hkExceptional : k ∈ thetaExceptionalPositions B alpha ⟨0, ⋯⟩ j) :
rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha ⟨0, ⋯⟩) (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha j)) (oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha k) + oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha ⟨0, ⋯⟩)) < 0

Every exceptional position gives a negative divisor when the first mark is the raw initial endpoint.

source
theorem Bananas.negative_path_pair_has_exceptional_representative_zero_left (B : Banana 2) (alpha : Fin 3) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B alpha j) (_hjFar : ↑j + 1 < B.length alpha) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (hNeg : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha ⟨0, ⋯⟩) (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha j)) D < 0) :
∃ k ∈ thetaExceptionalPositions B alpha ⟨0, ⋯⟩ j, linearEquiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B) D (oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha k) + oneChip (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha ⟨0, ⋯⟩))

Every negative divisor for the raw-initial/interior boundary marking has the exceptional representative asserted in Theorem 3.4.

source
theorem Bananas.thetaPairDivisorClass_bijOn_negative_zero_left (B : Banana 2) (alpha : Fin 3) (j : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hj : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B alpha j) (hjFar : ↑j + 1 < B.length alpha) :
Set.BijOn (thetaPairDivisorClass B alpha ⟨0, ⋯⟩) (thetaExceptionalPositions B alpha ⟨0, ⋯⟩ j) (negativeRankDeltaClasses (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha ⟨0, ⋯⟩) (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha j)))

Theorem 3.4, class-valued bijection, raw initial-endpoint branch.