Degree-one classes on a bridgeless graph

This formalizes Lemma 2.3 of the paper using TwoEdgeCutCondition as the precise no-bridge hypothesis. A nontriviality hypothesis is stated explicitly: for the one-vertex edgeless graph the cut condition is vacuous, but its unique degree-one class has rank one rather than rank zero.

theorem Bananas.vertex_eq_iff_one_chip_linear_equiv_of_twoEdgeCutCondition (G : CFGraph) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (u v : G.V) : u = v ↔ linearEquiv G (oneChip u) (oneChip v)

Lemma 2.3(1): on a connected graph with no one-edge cut, two vertices are equal exactly when their degree-one divisors are linearly equivalent.

theorem Bananas.rank_one_chip_eq_zero_of_twoEdgeCutCondition (G : CFGraph) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) (x : G.V) : rank G (oneChip x) = 0

On a nontrivial connected graph with no one-edge cut, every one-chip divisor has rank exactly zero.

def Bananas.RankZeroDegreeOneClass (G : CFGraph) : Type u_1

The rank-zero part of the degree-one Picard component, represented in the additive quotient model used throughout the formalization.

Equations

• Bananas.RankZeroDegreeOneClass G = { c : CFDiv G ⧸ principalDivisors G // ∃ (D : CFDiv G), (QuotientAddGroup.mk' (principalDivisors G)) D = c ∧ rank G D = 0 ∧ CFDiv.degree D = 1 }

def Bananas.bridgelessDegreeOneClassMap (G : CFGraph) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) : G.V → RankZeroDegreeOneClass G

The Abel--Jacobi vertex map, with codomain restricted to rank-zero degree-one divisor classes.

Equations

• Bananas.bridgelessDegreeOneClassMap G hConnected hCut hNontrivial x = ⟨(QuotientAddGroup.mk' (principalDivisors G)) (oneChip x), ⋯⟩

theorem Bananas.bridgelessDegreeOneClassMap_bijective (G : CFGraph) (hConnected : _root_.graphConnected G) (hCut : Utilities.TwoEdgeCutCondition G) (hNontrivial : ∃ (p : G.V) (q : G.V), p ≠ q) : Function.Bijective (bridgelessDegreeOneClassMap G hConnected hCut hNontrivial)

Lemma 2.3(2): vertices are in bijection with rank-zero divisor classes of degree one.