Documentation

LeanPool.BrillNoetherGraphs.Bananas.Wedge.SameFactorWedgeKGeneral

The same-factor exceptional wedge marking #

When the marked genus-one wedge factor has two vertices, its two marked vertices have exact order two in the whole wedge. Consequently the general order-two criterion supplies general transmission as soon as submodularity is known.

source
theorem Bananas.same_leftFactor_wedge_isTorsionOrder_two (G H : CFGraph) (x u : G.V) (y : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hCut : Utilities.TwoEdgeCutCondition G) (hCard : Fintype.card G.V = 2) (hxu : x ≠ u) :
IsTorsionOrder (mark (Utilities.vertexWedge G H x y) (Sum.inl x) (Sum.inl u)) 2

The two vertices of a two-vertex bridgeless genus-one left factor have exact marked torsion order two after attaching any pointed-rigid genus-one right factor.

source
theorem Bananas.same_leftFactor_wedge_twoGeneral (G H : CFGraph) (x u : G.V) (y : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hCut : Utilities.TwoEdgeCutCondition G) (hCard : Fintype.card G.V = 2) (hxu : x ≠ u) (hSub : AllSubmodular (mark (Utilities.vertexWedge G H x y) (Sum.inl x) (Sum.inl u))) :
KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Sum.inl x) (Sum.inl u)) 2

The same-factor two-vertex exception has two-general transmission.

source
theorem Bananas.same_leftFactor_wedge_twoGeneral_of_card_eq_two (G H : CFGraph) (x u : G.V) (y : H.V) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hCut : Utilities.TwoEdgeCutCondition G) (hCard : Fintype.card G.V = 2) (hxu : x ≠ u) :
KGeneralTransmission (mark (Utilities.vertexWedge G H x y) (Sum.inl x) (Sum.inl u)) 2

The same-factor two-vertex exception needs no additional submodularity hypothesis: genus-one Riemann--Roch and the wedge rank formula prove it automatically.