Documentation

LeanPool.BrillNoetherGraphs.Bananas.Wedge.WedgeKGeneralClassification

Mark-placement classification on a rigid genus-two wedge #

This is the wedge half of Theorem 4.13. It is deliberately intrinsic: the two genus-one factors are not presented as chosen cycles.

source
def Bananas.WedgeKGeneralPlacement (G H : CFGraph) (x : G.V) (y : H.V) (u v : (Utilities.vertexWedge G H x y).V) (k : ℕ) :
Prop

The six ordered placements that can survive general transmission on a rigid wedge of two genus-one factors. The first four are the order-two two-vertex same-factor exceptions; the last two are the distinct-factor equal-order branch.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem Bananas.wedge_kGeneral_placement (G H : CFGraph) (x : G.V) (y : H.V) (u v : (Utilities.vertexWedge G H x y).V) (k : ℕ) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hGCut : Utilities.TwoEdgeCutCondition G) (hHCut : Utilities.TwoEdgeCutCondition H) (hWCut : Utilities.TwoEdgeCutCondition (Utilities.vertexWedge G H x y)) (huv : u ≠ v) (hK : KGeneralTransmission (mark (Utilities.vertexWedge G H x y) u v) k) :
    WedgeKGeneralPlacement G H x y u v k

    Necessity half of the wedge branch of Theorem 4.13.

    source
    theorem Bananas.kGeneral_of_wedge_placement (G H : CFGraph) (x : G.V) (y : H.V) (u v : (Utilities.vertexWedge G H x y).V) (k : ℕ) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hGCut : Utilities.TwoEdgeCutCondition G) (hHCut : Utilities.TwoEdgeCutCondition H) (hPlace : WedgeKGeneralPlacement G H x y u v k) :
    KGeneralTransmission (mark (Utilities.vertexWedge G H x y) u v) k

    Sufficiency half of the intrinsic wedge classification. Each placement is either the automatic order-two two-vertex exception or an opposite-factor pair with equal exact factor orders.

    source
    theorem Bananas.kGeneral_iff_wedge_placement (G H : CFGraph) (x : G.V) (y : H.V) (u v : (Utilities.vertexWedge G H x y).V) (k : ℕ) (hG : Utilities.PointedGenusOneRigid G x) (hH : Utilities.PointedGenusOneRigid H y) (hGCut : Utilities.TwoEdgeCutCondition G) (hHCut : Utilities.TwoEdgeCutCondition H) (hWCut : Utilities.TwoEdgeCutCondition (Utilities.vertexWedge G H x y)) (huv : u ≠ v) :
    KGeneralTransmission (mark (Utilities.vertexWedge G H x y) u v) k ↔ WedgeKGeneralPlacement G H x y u v k

    Exact intrinsic wedge form of the general-transmission branch of Theorem 4.13, for distinct marked vertices.