Documentation

LeanPool.BrillNoetherGraphs.Bananas.Theta.ThetaNegativeDivisorClassesTerminal

Terminal-endpoint negative divisor classes on theta graphs #

This is the reflected boundary family complementary to thetaPairDivisorClass_bijOn_negative_zero_left: the second mark is the raw terminal endpoint and the first is an interior point at least two steps from the initial endpoint.

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

Every exceptional position gives a negative divisor when the second mark is the raw terminal endpoint.

source
theorem Bananas.negative_path_pair_has_exceptional_representative_terminal_right (B : Banana 2) (alpha : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hi : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B alpha i) (hiFar : 1 < ↑i) (D : CFDiv (Utilities.Certificate.SubdivisionGraph.Spec.graph B)) (hNeg : rankDelta (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha i) (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha ⟨B.length alpha, ⋯⟩)) D < 0) :
∃ k ∈ thetaExceptionalPositions B alpha i ⟨B.length alpha, ⋯⟩, 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 i))

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

source
theorem Bananas.thetaPairDivisorClass_bijOn_negative_terminal_right (B : Banana 2) (alpha : Fin 3) (i : Utilities.Certificate.SubdivisionGraph.Spec.PathPosition B alpha) (hi : Utilities.Certificate.SubdivisionGraph.Spec.IsInteriorPosition B alpha i) (hiFar : 1 < ↑i) :
Set.BijOn (thetaPairDivisorClass B alpha i) (thetaExceptionalPositions B alpha i ⟨B.length alpha, ⋯⟩) (negativeRankDeltaClasses (mark (Utilities.Certificate.SubdivisionGraph.Spec.graph B) (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha i) (Utilities.Certificate.SubdivisionGraph.Spec.pathVertex B alpha ⟨B.length alpha, ⋯⟩)))

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